A Logical Framework for the spi-calculus

\spi\ \cite{ag98} 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.