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:

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:

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