Adversary Safety by Construction in a Language of Cryptographic Protocols

Timothy Braje, Alice Lee, Andrew Wagner, Benjamin Kaiser, Daniel Park, Martine Kalke, Robert Cunningham, Adam Chlipala. Adversary Safety by Construction in a Language of Cryptographic Protocols. Proceedings of the 35th IEEE Computer Security Foundations Symposium (CSF'22). August 2022. Lincoln Laboratory Best Paper Award.

Paper as PDF

Compared to ordinary concurrent and distributed systems, cryptographic protocols are distinguished by the need to reason about interference by adversaries. We suggest a new layered approach to tame that complexity, via an executable protocol language whose semantics does not reveal an adversary directly, instead enforcing a set of intuitive hygiene rules. By virtue of those rules, protocols written in this language provably behave identically with or without interference by active Dolev-Yao-style adversaries. As a result, formal reasoning about protocols can be simplified enough that even naive model checking can establish correctness of a multiparty protocol, through analysis of a state space with no adversary.

We present the design and implementation of SPICY, short for Secure Protocols Implemented CorrectlY, including the semantics of its input languages; the essential safety proofs, formalized in the Coq theorem prover; and the automation techniques. We provide a preliminary evaluation of the tool's performance and capabilities via a handful of case studies.

GitHub repository