Automatic verification of transparency protocols (extended version)
Vincent Cheval, José Moreira, Mark Ryan
备注：
23 pages, Extended version to the paper "Automatic verification of transparency protocols" to be published in the 8th IEEE European Symposium on Security and Privacy 2023 (EuroS&P'23)
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.
Improving the Security of Containerized Workloads using Transparency and Traceability Services
ExcID；Universitat Politècnica de València（瓦伦西亚理工大学）；Athens University of Economics and Business（雅典经济与商业大学）；Chinese University of Hong Kong, Shenzhen（香港中文大学（深圳））
