A formalisation of the spi calculus in Coq
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.