Events

29 November 2007

A formalisation of the spi calculus in Coq

Sébastien Briais
Plume Team, ENS Lyon

Thursday, 29 November 2007
10h30 - 11h30
MSR-INRIA Joint Centre

Firstly, I will recall the definition of the spi calculus (an extension of the pi calculus to reason about cryptographic protocols) and the notion of hedged bisimilarity. I will also give two alternative operationnal semantics that are useful for defining an open variant of hedged bisimilarity.

Secondly, I will sketch the formalisation in Coq of these notions, and discuss in particular of several abstractions that have been convenient for achieving this task.

Finally, I will discuss several proofs led in Coq and if time permits, demonstrate some small examples of bisimulation proofs using my formalisation.