Computability in Europe 2006
Logical Approaches to Computational Barriers

Regular Talk:
Implementing Spi Calculus using Nominal techniques

Author(s): Temesghen Kahsai and Marino Miculan
Slot: Array, 17:10-17:30, col. 4


The aim of this work is to obtain an interactive proof environment based on Isabelle/HOL for reasoning formally about cryptographic protocols, expressed as processes of the spi calculus (a Ï-calculus with cryptographic primitives). To this end, we formalize syntax, semantics, and both hedged and framed bisimulation, two environment-sensitive bisimulations which can be used for proving security properties of protocols. In order to deal smoothly with binding operators and reason up-to α-equivalence of bound names, we adopt the new Nominal datatype package. This simplifying both the encoding, and the formal proofs, which turn out to correspond closely to âmanual proofsâ.

websites: Arnold Beckmann 2008-05-19