Computing Publications

Publications Home » Cryptographic Protocol Synthesis ...

Cryptographic Protocol Synthesis and Verification for Multiparty Sessions

Pierre-Malo , Karthikeyan Bhargavan, Ricardo Corin, Fournet, James Leifer

Conference or Workshop Paper
Computer Security Foundations Symposium
July, 2009
IEEE Computer Security Foundations Symposium
Issue 2009
pp.124–140
IEEE Computer Society
ISBN 978-0-7695-3712-2
ISSN 1063-6900
DOI 10.1109/CSF.2009.26
Abstract

We present the design and implementation of a compiler that, given high-level multiparty session descriptions, generates custom cryptographic protocols. Our sessions specify pre-arranged patterns of message exchanges and data accesses between distributed participants. They provide each participant with strong security guarantees for all their messages. Our compiler generates code for sending and receiving these messages, with cryptographic operations and checks, in order to enforce these guarantees against any adversary that may control both the network and some session participants. We verify that the generated code is secure by relying on a recent type system for cryptography. Most of the proof is performed by mechanized type checking and does not rely on the correctness of our compiler. We obtain the strongest session security guarantees to date in a model that captures the executable details of protocol code. We illustrate and evaluate our approach on a series of protocols inspired by web services.

BibTEX file for the publication
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.