Alley Stoughton, Boston University

Abstract

We show how one can use the EasyCrypt proof assistant to mechanize proofs of security of cryptographic protocols within the universally composable (UC) security framework.  This allows, for the first time, the mechanization of the entire sequence of steps needed for proving simulation-based security in a modular way:

(*) specifying the real protocol and desired ideal functionality;

(*) constructing a simulator and demonstrating its validity, possibly via reduction to hard computational problems;

(*) invoking the universal composition operation and demonstrating that it indeed preserves security.

We work with a variant of UC security in which real protocols, ideal functionalities, adversaries, simulators and environments are represented by modules in the EasyCrypt programming language (as opposed to interactive Turing machines). We formalize a UC message routing system based on hierarchical addresses, and employ an interface module that firewalls the environment from a real protocol/ideal functionality and adversary/simulator.

We illustrate our approach on a recently completed case study involving one-time-pad encryption, where the key comes from Diffie-Hellman key-exchange. We conclude by surveying the lessons learned from our case study, and pointing the way toward future work.

Joint work with Ran Canetti and Mayank Varia.

Video