  Transparency protocols are protocols whose actions can be publicly monitored
by observers (such observers may include regulators, rights advocacy groups, or
the general public). The observed actions are typically usages of private keys
such as decryptions, and signings. Examples of transparency protocols include
certificate transparency, cryptocurrency, transparent decryption, and
electronic voting. These protocols usually pose a challenge for automatic
verification, because they involve sophisticated data types that have strong
properties, such as Merkle trees, that allow compact proofs of data presence
and tree extension.
  We address this challenge by introducing new features in ProVerif, 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. We illustrate the
methodology and features by providing the first formal verification of the
transparent decryption and certificate transparency protocols with a precise
modelling of the Merkle tree data structure.
