Computing That Serves

Deploying Cryptographic Protocols in the Real World


Thursday, January 24, 2008 - 11:00am


Jay McCarthy, PhD Candidate, Brown University

Cryptographic protocols are used to engineer trust in online transactions.  In real-world deployments, implementations must be
scalable and fault-tolerant.  We present two analyses that enable this.  The first determines when multiple sessions of protocols can
safely interact concurrently to achieve scalability.  The second determines the minimal backup of a running protocol, which enables
fault-tolerance and even has value as an analysis technique.

We also observe that typical protocol specification languages do not match the abstractions used by protocol designers.  We therefore
present a protocol specification language that matches design idioms. We offer a compiler that transforms these specifications into
executables that can be deployed.

We evaluate our work on a large repository of known protocols to demonstrate its utility.  Our work has been formalized, verified, and
implemented using the Coq proof assistant.


Jay McCarthy received an BS in Mathematics and Computer Science at the University of Massachusetts at Lowell with a minor in Economics. He received an ScM in Computer Science at Brown University, where he is a PhD candidate in Computer Science working with Shriram Krishnamurthi. He has been employed as a Research Scientist at the MITRE Corporation, a consultant at Exis Capital, and as an industrial researcher at EMC Corporation. He is a member of the multi-university research group, PLT, with affiliates at Northeastern University, University of Chicago, University of Utah, and Worcester Polytechnic Institute. He is the recipient of an NSF Graduate Research Fellowship. His research interests include cryptographic protocols, new low-level systems paradigms, computer-aided verification, and program analysis.