# Re: [isabelle] [moca] A formalisation of the spi calculus in Coq

On 02/nov/07, at 14:40, Sébastien Briais wrote:

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].

`I guess this is a good occasion for advertising also our
``formalization of the spi-calculus in Isabelle/Nominal, which we have
``done about one year ago.
`See at
http://www.cs.swan.ac.uk/~csteme/SpiInIsabelle/SpiInIsabelle.html
It contains
- the definition of the spi calculus
- the definitions of several LTS and their properties
- the definitions of frame and frame bisimulation
- the definitions and properties of hedges
- the definition of late hedged bisimulation
- the proof of a "perfect encryption" equation in frame bisimulation
- the proof of a "perfect encryption" equation in hedged bisimulation

`- the proof of "impossibility of certain inputs", both in framed and
``in hedged bisimulations
`

`Notably, the usage of Nominal package simplifies the handling of
``binders and names, without using de Bruijn indexes.
`
All the best
- Temesghen Kahsai and Marino Miculan
--
Marino Miculan - Dept Math Compu Sci, University of Udine
miculan at dimi.uniud.it http://www.dimi.uniud.it/miculan/

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*