Specifying and implementing privacy-preserving cryptographic protocols

Formal methods are an important tool for designing secure cryptographic protocols. However, the existing work on formal methods does not cover privacy-preserving protocols as much as other types of protocols. Furthermore, privacy-related properties, such as unlinkability, are not always easy or even possible to prove statically, but need to be checked dynamically during the protocol’s execution. In this paper, we demonstrate how, starting from an informal description of a privacy-preserving protocol in natural language, one may use a modified and extended version of the Typed MSR language to create a formal specification of this protocol, typed in a linkability-oriented type system, and then use this specification to reach an implementation of this protocol in Jif, in such a way that privacy vulnerabilities can be detected with a mixture of static and runtime checks.