The paper introduces the spi calculus, an extension of the pi calculus designed for describing and analyzing cryptographic protocols. The pi calculus is used for abstract protocol descriptions, while the spi calculus includes cryptographic primitives to handle more detailed security issues. The spi calculus represents protocols as processes and defines security properties in terms of coarse-grained notions of protocol equivalence. The paper covers the syntax and semantics of the spi calculus, including shared-key cryptography and public-key cryptography. Examples of cryptographic protocols are provided, demonstrating how the spi calculus can model authentication and key exchange protocols. The formal semantics of the spi calculus is also discussed, including the reaction relation and the equivalence relation used for expressing security properties.The paper introduces the spi calculus, an extension of the pi calculus designed for describing and analyzing cryptographic protocols. The pi calculus is used for abstract protocol descriptions, while the spi calculus includes cryptographic primitives to handle more detailed security issues. The spi calculus represents protocols as processes and defines security properties in terms of coarse-grained notions of protocol equivalence. The paper covers the syntax and semantics of the spi calculus, including shared-key cryptography and public-key cryptography. Examples of cryptographic protocols are provided, demonstrating how the spi calculus can model authentication and key exchange protocols. The formal semantics of the spi calculus is also discussed, including the reaction relation and the equivalence relation used for expressing security properties.