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. 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 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 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.

翻译：我们在安全协议自动化验证工具ProVerif中引入了新功能，并提出了一套对应的使用方法。该方法和功能针对涉及具有强特性的复杂数据类型（如Merkle树，可实现数据存在性与树扩展的紧凑证明）的协议。这类数据类型广泛用于分布式账本和/或区块链系统中的协议。通过我们的方法，可以借助ProVerif公理以相当抽象的方式描述数据类型，并基于这些公理假设证明协议的正确性。随后，可在独立步骤中定义该数据类型的一种或多种具体实现，并再次使用ProVerif证明这些实现满足先前编码为公理的假设。这种方法有助于实现组合式证明，将证明负担分解为多个可管理的部分。为实现该方法，我们扩展了ProVerif能够推理的引理与公理类别，引入了新功能。具体而言，我们允许用户自定义谓词、攻击者谓词以及消息谓词出现在引理和公理中。我们从语义角度证明了该实现的可靠性。通过首次对两种精确建模Merkle树数据结构的透明度协议进行形式化验证，我们展示了该方法和新功能的应用。这两种协议分别是透明解密与证书透明度。透明解密旨在确保解密操作能被受影响人员观察到，这可用于支持隐私保护：它意味着数据主体能获知其相关信息已被解密。证书透明度则是互联网安全标准，用于监控和审计数字证书的颁发。