Mobile values, new names, and secure communication
2001pp. 104–115
Citations Over TimeTop 1% of 2001 papers
Abstract
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.
Related Papers
- → Structural Operational Semantics(1999)226 cited
- → On collecting semantics for program analysis(2020)4 cited
- An operational semantics for Scheme(1992)
- An overview of semantics for the validation of numerical programs(2005)
- Semantics for the Asynchronous Communication in LIPS, a Language for Implementing Parallel/distributed Systems.(2009)