Mobile Values, New Names, and Secure Communications

Cedric Fournet and Martin Abadi.


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.