{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T08:43:19Z","timestamp":1774946599145,"version":"3.50.1"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2020,9,9]],"date-time":"2020-09-09T00:00:00Z","timestamp":1599609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,9,9]],"date-time":"2020-09-09T00:00:00Z","timestamp":1599609600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100012338","name":"Alan Turing Institute","doi-asserted-by":"publisher","award":["EP\/N510129\/1"],"award-info":[{"award-number":["EP\/N510129\/1"]}],"id":[{"id":"10.13039\/100012338","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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:<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varSigma $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03a3<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-protocols and Commitment Schemes.<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varSigma $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03a3<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-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\u00a0(Lochbihler in Archive of formal proofs, 2017) to formalise both primitives and prove secure multiple examples namely; the Schnorr, Chaum-Pedersen and Okamoto<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varSigma $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03a3<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-protocols as well as a construction that allows for compound (AND and OR)<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varSigma $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03a3<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-protocols and the Pedersen and Rivest commitment schemes. A highlight of the work is a formalisation of the construction of commitment schemes from<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varSigma $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03a3<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-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.<\/jats:p>","DOI":"10.1007\/s10817-020-09581-w","type":"journal-article","created":{"date-parts":[[2020,9,10]],"date-time":"2020-09-10T12:53:09Z","timestamp":1599742389000},"page":"521-567","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Formalising $$\\varSigma $$-Protocols and Commitment Schemes Using CryptHOL"],"prefix":"10.1007","volume":"65","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2599-0736","authenticated-orcid":false,"given":"D.","family":"Butler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Lochbihler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Aspinall","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Gasc\u00f3n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,9,9]]},"reference":[{"key":"9581_CR1","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90\u2013101. ACM (2009)","DOI":"10.1145\/1594834.1480894"},{"key":"9581_CR2","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., Zanella B\u00e9guelin, S.: Computer-aided security proofs for the working cryptographer. In: CRYPTO, Volume 6841 of Lecture Notes in Computer Science, pp. 71\u201390. Springer (2011)","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"9581_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: CRYPTO, Volume 6841 of Lecture Notes in Computer Science, pp. 71\u201390. Springer (2011)","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"9581_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella-B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 90\u2013101. ACM (2009)","DOI":"10.1145\/1594834.1480894"},{"key":"9581_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., Hedin, D., B\u00e9guelin, S.Z., Gr\u00e9goire, B., Heraud, S.: A machine-checked formalization of sigma-protocols. In: CSF, pp. 246\u2013260. IEEE Computer Society (2010)","DOI":"10.1109\/CSF.2010.24"},{"key":"9581_CR6","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1007\/s00145-019-09341-z","volume":"33","author":"DA Basin","year":"2020","unstructured":"Basin, D.A., Lochbihler, A., Sefidgar, S.R.: CryptHOL: game-based proofs in higher-order logic. J. Cryptol. 33, 494\u2013566 (2020)","journal-title":"J. Cryptol."},{"key":"9581_CR7","doi-asserted-by":"crossref","unstructured":"Bellare, M., Rogaway, P.: The security of triple encryption and a framework for code-based game-playing proofs. In: EUROCRYPT, Volume 4004 of Lecture Notes in Computer Science, pp. 409\u2013426. Springer (2006)","DOI":"10.1007\/11761679_25"},{"key":"9581_CR8","unstructured":"Blum, M.: Coin flipping by telephone. In: CRYPTO, pp. 11\u201315. U. C. Santa Barbara, Dept. of Elec. and Computer Eng., ECE Report No 82-04 (1981)"},{"key":"9581_CR9","unstructured":"Blum, M.: How to prove a theorem so no one else can claim it. In: International Congress of Mathematicians, pp. 1444\u20131451 (1986)"},{"issue":"1\u20133","key":"9581_CR10","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1023\/A:1016501125022","volume":"26","author":"C Blundo","year":"2002","unstructured":"Blundo, C., Masucci, B., Stinson, D.R., Wei, R.: Constructions and bounds for unconditionally secure non-interactive commitment schemes. Des. Codes Cryptogr. 26(1\u20133), 97\u2013110 (2002)","journal-title":"Des. Codes Cryptogr."},{"key":"9581_CR11","unstructured":"Butler, D., Aspinall, D.: Multi-party computation. In: Archive of Formal Proofs (2019)"},{"key":"9581_CR12","doi-asserted-by":"crossref","unstructured":"Butler, D., Aspinall, D., Gasc\u00f3n, A.: How to simulate it in Isabelle: towards formal proof for secure multi-party computation. In: ITP, Volume 10499 of Lecture Notes in Computer Science, pp. 114\u2013130. Springer (2017)","DOI":"10.1007\/978-3-319-66107-0_8"},{"key":"9581_CR13","doi-asserted-by":"crossref","unstructured":"Butler, D., Aspinall, D., Gasc\u00f3n, A.: On the formalisation of $$\\Sigma $$-protocols and commitment schemes. In: POST, Volume 11426 of Lecture Notes in Computer Science, pp. 175\u2013196. Springer (2019)","DOI":"10.1007\/978-3-030-17138-4_8"},{"key":"9581_CR14","doi-asserted-by":"crossref","unstructured":"Butler, D., Aspinall, D., Gasc\u00f3n, A.: Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL. In: CPP, pp. 229\u2013243. ACM (2020)","DOI":"10.1145\/3372885.3373815"},{"key":"9581_CR15","unstructured":"Butler, D., Lochbihler, A.: Sigma protocols and commitment schemes. In: Archive of Formal Proofs (2019)"},{"key":"9581_CR16","doi-asserted-by":"crossref","unstructured":"Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: FOCS, pp. 136\u2013145. IEEE Computer Society (2001)","DOI":"10.1109\/SFCS.2001.959888"},{"key":"9581_CR17","doi-asserted-by":"crossref","unstructured":"Canetti, R., Stoughton, A., Varia, M.: EasyUC: using EasyCrypt to mechanize proofs of universally composable security. In: Proceedings of the 32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA. IEEE Computer Society (2019)","DOI":"10.1109\/CSF.2019.00019"},{"key":"9581_CR18","doi-asserted-by":"crossref","unstructured":"Chaum, D., Pedersen, T.P.: Wallet databases with observers. In: CRYPTO, Volume 740 of Lecture Notes in Computer Science, pp. 89\u2013105. Springer (1992)","DOI":"10.1007\/3-540-48071-4_7"},{"key":"9581_CR19","unstructured":"Ciampi, M., Persiano, G., Scafuro, A., Siniscalchi, L., Visconti, I.: Improved OR-composition of Sigma-protocols. Cryptology ePrint Archive, Report 2015\/810. https:\/\/eprint.iacr.org\/2015\/810 (2015)"},{"key":"9581_CR20","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-662-49099-0_5","volume-title":"Theory of Cryptography","author":"M Ciampi","year":"2016","unstructured":"Ciampi, M., Persiano, G., Scafuro, A., Siniscalchi, L., Visconti, I.: Improved OR-composition of Sigma-protocols. In: Kushilevitz, E., Malkin, T. (eds.) Theory of Cryptography, pp. 112\u2013141. Springer, Berlin (2016)"},{"key":"9581_CR21","unstructured":"Cramer, R.: Modular design of secure, yet practical cryptographic protocols. Ph.D. Thesis University of Amsterdam (1996)"},{"key":"9581_CR22","doi-asserted-by":"crossref","unstructured":"Cramer, R., Damg\u00e5rd, I., Schoenmakers, B.: Proofs of partial knowledge and simplified design of witness hiding protocols. In: CRYPTO, Volume 839 of Lecture Notes in Computer Science, pp. 174\u2013187. Springer (1994)","DOI":"10.1007\/3-540-48658-5_19"},{"key":"9581_CR23","unstructured":"Damgard, I.: On $$\\Sigma $$-protocols. Lecture Notes, University of Aarhus, Department for Computer Science (2002)"},{"key":"9581_CR24","doi-asserted-by":"crossref","unstructured":"Damg\u00e5rd, I.: On the existence of bit commitment schemes and zero-knowledge proofs. In: CRYPTO, Volume 435 of Lecture Notes in Computer Science, pp. 17\u201327. Springer (1989)","DOI":"10.1007\/0-387-34805-0_3"},{"key":"9581_CR25","doi-asserted-by":"crossref","unstructured":"Damg\u00e5rd, I., Kilian, J., Salvail, L.: On the (im)possibility of basing oblivious transfer and bit commitment on weakened security assumptions. In: EUROCRYPT, Volume 1592 of Lecture Notes in Computer Science, pp. 56\u201373. Springer (1999)","DOI":"10.1007\/3-540-48910-X_5"},{"key":"9581_CR26","unstructured":"Even, S.: Protocol for signing contracts. In: CRYPTO, pp. 148\u2013153. U. C. Santa Barbara, Dept. of Elec. and Computer Eng., ECE Report No 82-04 (1981)"},{"key":"9581_CR27","doi-asserted-by":"crossref","unstructured":"Fiat, A., Shamir, A.: How to prove yourself: practical solutions to identification and signature problems. In: CRYPTO, Volume 263 of Lecture Notes in Computer Science, pp. 186\u2013194. Springer (1986)","DOI":"10.1007\/3-540-47721-7_12"},{"key":"9581_CR28","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511721656","volume-title":"The Foundations of Cryptography\u2014Volume 2: Basic Applications","author":"O Goldreich","year":"2004","unstructured":"Goldreich, O.: The Foundations of Cryptography\u2014Volume 2: Basic Applications. Cambridge University Press, Cambridge (2004)"},{"key":"9581_CR29","doi-asserted-by":"crossref","unstructured":"Haagh, H., Karbyshev, A., Oechsner, S., Spitters, B., Strub, P.-Y.: Computer-aided proofs for multiparty computation with active security. In: CSF, pp. 119\u2013131. IEEE Computer Society (2018)","DOI":"10.1109\/CSF.2018.00016"},{"key":"9581_CR30","first-page":"181","volume":"2005","author":"S Halevi","year":"2005","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. IACR Cryptol. ePrint Arch. 2005, 181 (2005)","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"9581_CR31","volume-title":"Efficient Secure Two-Party Protocols\u2014Techniques and Constructions. Information Security and Cryptography","author":"C Hazay","year":"2010","unstructured":"Hazay, C., Lindell, Y.: Efficient Secure Two-Party Protocols\u2014Techniques and Constructions. Information Security and Cryptography. Springer, Berlin (2010)"},{"key":"9581_CR32","unstructured":"Lochbihler, A.: CryptHOL. In: Archive of Formal Proofs (2017)"},{"key":"9581_CR33","doi-asserted-by":"crossref","unstructured":"Lochbihler, A., Sefidgar, S.R., Basin, D.A., Maurer, U.: Formalizing constructive cryptography using CryptHOL. In: Computer Security Foundations (CSF 2019), pp. 152\u2013166. IEEE (2019)","DOI":"10.1109\/CSF.2019.00018"},{"key":"9581_CR34","doi-asserted-by":"crossref","unstructured":"Metere, R., Dong, C.: Automated cryptographic analysis of the pedersen commitment scheme. In: MMM-ACNS, Volume 10446 of Lecture Notes in Computer Science, pp. 275\u2013287. Springer (2017)","DOI":"10.1007\/978-3-319-65127-9_22"},{"key":"9581_CR35","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics\u2014With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics\u2014With Isabelle\/HOL. Springer, Berlin (2014)"},{"key":"9581_CR36","doi-asserted-by":"crossref","unstructured":"Petcher, A., Morrisett, G.: The foundational cryptography framework. In: POST, Volume 9036 of Lecture Notes in Computer Science, pp. 53\u201372. Springer (2015)","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"9581_CR37","unstructured":"Rivest, R.: Unconditionally secure commitment and oblivious transfer schemes using private channels and a trusted initializer. Unpublished manuscript (1999)"},{"issue":"3","key":"9581_CR38","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/BF00196725","volume":"4","author":"C-P Schnorr","year":"1991","unstructured":"Schnorr, C.-P.: Efficient signature generation by smart cards. J. Cryptol. 4(3), 161\u2013174 (1991)","journal-title":"J. Cryptol."},{"key":"9581_CR39","first-page":"332","volume":"2004","author":"V Shoup","year":"2004","unstructured":"Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. IACR Cryptol. ePrint Arch. 2004, 332 (2004)","journal-title":"IACR Cryptol. ePrint Arch."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09581-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09581-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09581-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,7]],"date-time":"2023-10-07T04:27:35Z","timestamp":1696652855000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09581-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,9]]},"references-count":39,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["9581"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09581-w","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,9,9]]},"assertion":[{"value":"11 October 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 August 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 September 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}