Mark Ryan, University of Birmingham with Vincent Cheval and José Moreira.
Transparency protocols are protocols whose actions can be publicly monitored by observers (observers may include regulators, rights advocacy groups, or the general public). The observed actions are typically usages of private keys: decryptions, and signings. Examples of transparency protocols include certificate transparency, cryptocurrency, transparent decryption, and electronic voting. Transparency protocols pose a challenge for automatic verification, because they involve sophisticated data types that have strong properties, such as Merkle trees, which allow compact proofs of data presence and tree extension.
We address this challenge by introducing new features in ProVerif (an automatic tool for verifying security protocols), and a methodology for using them. 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.