Talks

Abstract

Spi (Abadi, Gordon 1998) has been presented as a (formal) setting used to describe and analyze protocols. Here we will present a short description of the calculus, introduce a new LTS, proving its equivalence to the LTS defined by Abadi and Gordon, and give a representation of the spi in the Edimburg Logical Framework introduced by Haper, Honsell and Plotkin. This Logical Framework provides a setting used to define formal systems based on a general treatment of syntax, rules and proofs by means of a typed lambda-calculus with dependent types. Finally, we will prove that the LF-semantics and the LTS-semantics are equivalent.