Analysis of Cryptographic Protocols via Symbolic State Space Enumeration

Reference:

Antti Huima. Analysis of cryptographic protocols via symbolic state space enumeration. Master's thesis, Helsinki University of Technology, May 1999.

[This thesis was nominated the best Master's Thesis on the area of Computer Science by The Finnish Society for Computer Science in 1999.]

Abstract:

Cryptographic protocols are an important building block of information security solutions.

Many proposed security protocols have been found to have defects in their logical structures. Such defects can cause the protocol to be vulnerable to various kinds of attacks. In the worst case, a faulty protocol can cause large monetary and other losses. Therefore many methods for analyzing security protocols formally have appeared in the scientific literature.

In this thesis, a new formal analysis method for security protocols is presented. The analysis method is based on symbolic state space enumeration. Symbolic state space enumeration is a generic concept in the verification of concurrent systems. This work applies the concept to the domain of security protocols.

Symbolic state space enumeration makes it possible to search an infinite state space in finite time.

Cryptography is modeled using algebras and convergent rewrite systems. Typically, models involving rewrite systems are implemented by using variants of the narrowing algorithm. However, the presented method does not need to use narrowing because of a novel, alternative approach bound tightly to the whole search process.

In the case of formal verification of generic concurrent systems, much of the data flow can be abstracted away. However, for security protocols, data is of the essence. Most of the complexity of the symbolic method in this thesis stems from the need to be able to handle infinite sets of algebraic terms and their interactions under a rewrite system.

In addition to the basic symbolic method, a symmetry method for the symbolic states as well as a method for detecting symbolic state subsumption relations is developed.

An end-user tool based on the theory, implemented in Scheme, is described.

As a whole the work is divided into two parts. In the first part the theoretical aspects of the method are described. The second part focuses on the implementation; also, an example is presented there.

Suggested BibTeX entry:

@mastersthesis{Huima99,
    author = {Antti Huima},
    month = {May},
    school = {Helsinki University of Technology},
    title = {Analysis of Cryptographic Protocols via Symbolic State Space Enumeration},
    year = {1999},
}