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