| Autor: |
Butler, D., Lochbihler, A., Aspinall, D., Gascón, A. |
| Jazyk: |
angličtina |
| Rok vydání: |
2021 |
| Předmět: |
|
| Zdroj: |
Butler, D, Lochbihler, A, Aspinall, D & Gascón, A 2021, ' Formalising Σ-Protocols and Commitment Schemes Using CryptHOL ', Journal of Automated Reasoning, vol. 65, pp. 521-567 . https://doi.org/10.1007/s10817-020-09581-w |
| DOI: |
10.1007/s10817-020-09581-w |
| Popis: |
Machine-checked proofs of security are important to increase the rigour of provable security. In this work we present a formalised theory of two fundamental two party cryptographic primitives: Σ-protocols and Commitment Schemes. Σ-protocols allow a prover to convince a verifier that they possess some knowledge without leaking information about the knowledge. Commitment schemes allow a committer to commit to a message and keep it secret until revealing it at a later time. We use CryptHOL (Lochbihler in Archive of formal proofs, 2017) to formalise both primitives and prove secure multiple examples namely; the Schnorr, Chaum-Pedersen and Okamoto Σ-protocols as well as a construction that allows for compound (AND and OR) Σ-protocols and the Pedersen and Rivest commitment schemes. A highlight of the work is a formalisation of the construction of commitment schemes from Σ-protocols (Damgard in Lecture notes, 2002). We formalise this proof at an abstract level using the modularity available in Isabelle/HOL and CryptHOL. This way, the proofs of the instantiations come for free. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
