Mobile values, new names, and secure communication

We study the interaction of the "new" construct with a rich but common form of (first-order) communication. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts. Specifically, we introduce a simple, general extension of the pi calculus with value passing, primitive functions, and equations among terms. We develop semantics and proof techniques for this extended language and apply them in reasoning about some security protocols. 1 A case for impurity Purity often comes before convenience and even before faithfulness in the lambda calculus, the pi calculus, and other foundational programming languages. For example, in the standard pi calculus, the only messages are atomic names [32]. This simplicity is extremely appealing from a foundational viewpoint, and helps in developing the theory of the pi calculus. Furthermore, ingenious encodings demonstrate that it may not entail...

• Type: Conference
• Year: 2001
• Where: POPL
• Authors: Cédric Fournet, Martín Abadi
• Keywords: Main Motivating Examples, Pi Calculus, POPL 2001, Programming Languages, Standard Pi Calculus