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
Finally, we will prove that the LF-semantics and the
LTS-semantics are equivalent.