Cryptyc papers

[Alan Jeffrey <ajeffrey@xxxxxxxxxxxxx>]

We are pleased to announce the availability of the first two technical
reports from the Cryptyc project:

     * A.D. Gordon and A.S.A. Jeffrey: Authenticity by Typing for 
Security Protocols.

     * A.D. Gordon and A.S.A. Jeffrey: Typing Correspondence Assertions 
for Communication Protocols.

These papers use a type-and-effect system to statically verify 
authenticity properties of communication protocols expressed in the 
spi-calculus, and the pi-calculus respectively.

The papers are available from:

   http://cryptyc.cs.depaul.edu/papers.html

   http://research.microsoft.com/~adg/Publications/

A proof-of-concept implementation of the type system, together with its 
use on a number of cryptographic protocols, is available at:

   http://cryptyc.cs.depaul.edu/

The abstracts are attached.

Andrew D. Gordon and Alan Jeffrey

--

A.D. Gordon and A.S.A. Jeffrey: Authenticity by typing for security 
protocols.  Technical Report MSR-TR-2000-49, Microsoft Research, 
conference version to appear in Proc. IEEE Computer Security Foundations 
Workshop, 2001.

We propose a new method to check authenticity properties of 
cryptographic protocols. First, code up the protocol in the spi-calculus 
of Abadi and Gordon. Second, specify authenticity properties by 
annotating the code with correspondence assertions in the style of Woo 
and Lam. Third, figure out types for the keys, nonces, and messages of 
the protocol. Fourth, check that the spi-calculus code is well-typed 
according to a novel type and effect system presented in this paper. Our 
main theorem guarantees that any well-typed protocol is robustly safe, 
that is, its correspondence assertions are true in the presence of any 
opponent expressible in spi. It is feasible to apply this method by hand 
to several well-known cryptographic protocols. It requires little human 
effort per protocol, puts no bound on the size of the opponent, and 
requires no state space enumeration. Moreover, the types for protocol 
data provide some intuitive explanation of how the protocol works. This 
paper describes our method and gives some simple examples. Our method 
has led us to the independent rediscovery of flaws in existing protocols 
and to the design of improved protocols.

--

A.D. Gordon and A.S.A. Jeffrey: Typing correspondence assertions for 
communication protocols.  Technical Report MSR-TR-2000-48, Microsoft 
Research, conference version to appear in Proc. Mathematical Foundations 
of Programming Semantics, 2001.

Woo and Lam propose correspondence assertions for specifying 
authenticity properties of security protocols. The only prior work on 
checking correspondence assertions depends on model-checking and is 
limited to finite-state systems. We propose a dependent type and effect 
system for checking correspondence assertions. Since it is based on 
type-checking, our method is not limited to finite-state systems. This 
paper presents our system in the simple and general setting of the 
pi-calculus. We show how to type-check correctness properties of example 
communication protocols based on secure channels.



 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html