Secure protocol synthesis for multi-party sessions

James Leifer, INRIA Rocquencourt, France

We present the design and implementation of a compiler that, given high-level multiparty session de- scriptions, generates custom cryptographic protocols. Our sessions specify pre-arranged patterns of mes- sage 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 re- ceiving these messages, with cryptographic operations and checks to enforce these guarantees against any adversary that may control both the network and arbitrary coalitions of 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.