Cryptographically Sound Implementations for Communicating Processes (joint work with Cédric Fournet)
In M. Bugliesi, B. Preneel, V. Sassone, and I. Wegener, editors, 33rd International Colloquium on Automata, Languages and Programming (ICALP), volume 4052 of LNCS, pages 83-94, Venice, Italy, July 9-16 2006. © Springer.

Abstract: We design a core language of principals running distributed programs over a public network. Our language is a variant of the pi calculus, with secure communications, mobile names, and high-level certificates, but without any explicit cryptography. Within this language, security properties can be conveniently studied using trace properties and observational equivalences, even in the presence of an arbitrary (abstract) adversary. With some care, these security properties can be achieved in a concrete setting, relying on standard cryptographic primitives and computational assumptions, even in the presence of an adversary modelled as an arbitrary probabilistic polynomial-time algorithm. To this end, we develop a cryptographic implementation that preserves all properties for all safe programs. We give a series of soundness and completeness results that precisely relate the language to its implementation. We also illustrate our approach using a series of protocols and properties expressible in our language, and motivate some unusual design choices.

Publication Info. Extended abstract presented at ICALP'06.

Date: 10 February 2006.

Get a preprint: PDF | PS | BibTeX Citation.
Get it from the publisher's website.