13 June 2023 - Mark Ryan Speaker Mark Ryan, University of Birmingham. Joint work with Vincent Cheval and José Moreira. Title Automatic verification of transparency protocols Abstract 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. Jun 13 2023 11.00 - 12.00 13 June 2023 - Mark Ryan Security, Privacy & Trust, and LFCS joint Seminar by Mark Ryan The Bayes Centre, 4th floor Edinburgh Coffee House 47 Potterrow Edinburgh EH8 9BT --- Join Zoom Meeting https://ed-ac-uk.zoom.us/j/86477486145 Meeting ID: 864 7748 6145 Passcode: 13gTnbFD
13 June 2023 - Mark Ryan Speaker Mark Ryan, University of Birmingham. Joint work with Vincent Cheval and José Moreira. Title Automatic verification of transparency protocols Abstract 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. Jun 13 2023 11.00 - 12.00 13 June 2023 - Mark Ryan Security, Privacy & Trust, and LFCS joint Seminar by Mark Ryan The Bayes Centre, 4th floor Edinburgh Coffee House 47 Potterrow Edinburgh EH8 9BT --- Join Zoom Meeting https://ed-ac-uk.zoom.us/j/86477486145 Meeting ID: 864 7748 6145 Passcode: 13gTnbFD
Jun 13 2023 11.00 - 12.00 13 June 2023 - Mark Ryan Security, Privacy & Trust, and LFCS joint Seminar by Mark Ryan
