The Coq mailing list

[S�bastien Briais <sebastien.briais AT epfl.ch>]

Dear all,

I am happy to announce the first public release of
my formalisation of the spi calculus [3] in the Coq
proof assistant [1].

The archive is available here:
http://lamp.epfl.ch/~sbriais/download/Spi_071102.tar.gz

De Bruijn indices are used to represent terms;
in order to avoid duplication of work, I have developed
a library to handle de Bruijn indices and their properties.

This formalisation is composed of 41 modules and
uses the (excellent) CoLoR library [2]. It compiles with
the latest release of Coq (>= 8.1pl2)

It includes most of the results of papers in which
I have been involved. More precisely, it contains:
- the definition of the pi calculus
- the definition of the spi calculus
(messages may use shared-key cryptography,
public-key cryptography, pairing and hashing;
the keys can be arbitrary terms (not just names))
- the definitions of several LTS and their properties
- the definitions and properties of hedges: a structure that is used
to represent the attacker knowledge in hedged bisimulations
(multiset order provided by CoLoR library is useful there)
- the definition of late hedged bisimulation
- the proof of a "perfect encryption" equation, namely that
if P(M)=(^k)'c<enc_s(M,k)> then P(M) = P(N) for any M and N

Best wishes,

Sébastien

[1] http://coq.inria.fr/
[2] http://color.loria.fr/
[3] A. Gordon, M. Abadi. A Calculus for Cryptographic Protocols: The Spi 
Calculus