Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 18 2022 at 11:02):

From: Marino Miculan <miculan@dimi.uniud.it>
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

Last updated: May 03 2024 at 12:27 UTC