Overview

Protocols based on cryptographic mechanisms play a fundamental role to achieve security of distributed applications. They are used to provide secure communication services (e.g. Secure Socket Layer), authentication services for handling and distributing passwords (e.g. Kerberos), and so on. The design of cryptographic protocols is highly error-prone. Many formal approaches have been developed and applied to the certification (specification and verification) of cryptographic protocols. Some of these techniques are based on state space exploration (e.g. finite-state model checking). The main advantage of state-space exploration with respect to other approaches is that it provides counterexamples when a protocol does not satisfy some properties. A major issues is therefore the dimension of the state space. Due to the rich structure of the messages exchanged inside a protocol session and to the power of the adversary (the intruder), the state-space may explode thus making state-space exploration unfeasible.

The standard way of addressing this problem is to assume an upper bound on the size of messages synthesized by the intruder. Symbolic approaches have been developed to keep finite the state-space. The basic idea of symbolic approaches is to adopt constraint systems (e.g. variation of unification) to express the values variables may assume. Moreover, properties are specified by inserting logical assertions in the specification of the protocol. Our research is aimed at further developing verification methodologies based on the notion of symbolic state-space exploration.

Current verification methodologies are not satisfactory for several reasons:

they do not clearly separate the specification of protocol behaviour from the specification of its security properties. Usually, the specification of the properties is hard-written into the code of the protocol. We argue that the clear distinction among the two specification will avoid mis-interpretation of the protocol. Moreover, it will allow to analyze a cryptographic protocol by looking at different security properties.
the assumptions underlying the formal notion of correctness are often not sufficiently formalized. This may lead into difficulties in the verification phase. For instance, it can allow us to prove correctness of a flawed protocol.
the life-cycle of a cryptographic protocol depends on the adversary: The precise specification of the adversary knowledge becomes a powerful verification device. It allows one to check correctness of a cryptographic protocol under different assumptions about the power of the adversary.

We present ASPASyA (Automated tool for Security Protocols Analysis based on a Symbolic Approach), a tool for verifying cryptographic protocols that tackles the three issues discussed above.

ASPASyA permits the verification of cryptographic protocols by controlling three different coordinates:

the intruder's knowledge,
the property specification and
the specification of implicit assumptions.

Users can opportunely mix those three ingredients for testing the correctness of the protocol without modifying the protocol specification. Moreover, also the definition of the desired property let the verifier abstract away specification details, like, noticeably, the number of interleaved execution of the protocol for which the property has to be cheked.

The separation of concerns is the added value of our approach with respect to other approaches based on symbolic state-space exploration.

The front-end of ASPASyA permits specifying cryptographic protocols by a name passing process calculus (called cIP). Properties are given with a suitable fragment of first order logic.

Emilio Tuosto

Last modified: Tue Nov 18 17:06:04 CET 2003