Computability in Europe 2008
Logic and Theory of Algorithms

Print current page  Print this page

Regular Talk:
Implementing Spi Calculus using Nominal techniques

Edit abstract data

Author(s): Temesghen Kahsai and Marino Miculan
Slot: Wed, 17:10-17:30, Room 22 (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 Valid HTML 4.01! Valid CSS!