Automatic verification of transparency protocols

Abstract

We introduce new features in ProVerif, an automatic tool for verifying security protocols, and a methodology for using them. This methodology and these features are aimed at protocols which involve sophisticated data types that have strong properties, such as Merkle trees, which allow compact proofs of data presence and tree extension. Such data types are widely used in protocols in systems that use distributed ledgers and/or blockchains.

With our methodology, it is possible to describe the data type quite abstractly, using ProVerif axioms, and prove the correctness of the protocol using those axioms as assumptions. Then, in separate steps, one can define one or more concrete implementations of the data type, and again use ProVerif to show that the implementations satisfy the assumptions that were coded as axioms. This helps make compositional proofs, splitting the proof burden into several manageable pieces.

To enable this methodology, we introduce new capabilities in ProVerif, by extending the class of lemmas and axioms that it can reason with. Specifically, we allow user-defined predicates, attacker predicates and message predicates to appear in lemmas and axioms, and define their semantics. We show the soundness of the implementation of this idea with respect to the semantics.

We illustrate the methodology and features by providing the first formal verification of two transparency protocols which precisely models the Merkle tree data structure. The two protocols are transparent decryption (sometimes called accountable decryption), and certificate transparency. Transparent decryption is a way of ensuring that decryption operations are visible by people who are affected by them. This can be used, for example, to support privacy: it can mean that a subject is alerted to the fact that information about them has been decrypted. Certificate transparency is an Internet security standard for monitoring and auditing the issuance of digital certificates.