Implementing spi calculus using nominal techniques

Abstract

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 formalise syntax, semantics, and hedged bisimulation, an environment-sensitive bisimulation 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 simplifies both the encoding, and the formal proofs, which turn out to correspond closely to "manual proofs". © 2008 Springer-Verlag Berlin Heidelberg.