×

Formalising \(\varSigma\)-protocols and commitment schemes using CryptHOL. (English) Zbl 1524.94063

Summary: 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: \(\varSigma\)-protocols and Commitment Schemes. \( \varSigma\)-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 to formalise both primitives and prove secure multiple examples namely; the Schnorr, Chaum-Pedersen and Okamoto \(\varSigma\)-protocols as well as a construction that allows for compound (AND and OR) \( \varSigma\)-protocols and the Pedersen and Rivest commitment schemes. A highlight of the work is a formalisation of the construction of commitment schemes from \(\varSigma\)-protocols. 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.

MSC:

94A60 Cryptography
68V20 Formalization of mathematics in connection with theorem provers
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Barthe, G., Grégoire, B., Zanella Béguelin, S.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90-101. ACM (2009) · Zbl 1315.68081
[2] Barthe, G., Grégoire, B., Heraud, S., Zanella Béguelin, S.: Computer-aided security proofs for the working cryptographer. In: CRYPTO, Volume 6841 of Lecture Notes in Computer Science, pp. 71-90. Springer (2011) · Zbl 1287.94048
[3] Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: CRYPTO, Volume 6841 of Lecture Notes in Computer Science, pp. 71-90. Springer (2011) · Zbl 1287.94048
[4] Barthe, G., Grégoire, B., Zanella-Béguelin, S.: Formal certification of code-based cryptographic proofs. In: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 90-101. ACM (2009) · Zbl 1315.68081
[5] Barthe, G., Hedin, D., Béguelin, S.Z., Grégoire, B., Heraud, S.: A machine-checked formalization of sigma-protocols. In: CSF, pp. 246-260. IEEE Computer Society (2010)
[6] Basin, DA; Lochbihler, A.; Sefidgar, SR, CryptHOL: game-based proofs in higher-order logic, J. Cryptol., 33, 494-566 (2020) · Zbl 1455.94121 · doi:10.1007/s00145-019-09341-z
[7] 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-426. Springer (2006) · Zbl 1140.94321
[8] Blum, M.: Coin flipping by telephone. In: CRYPTO, pp. 11-15. U. C. Santa Barbara, Dept. of Elec. and Computer Eng., ECE Report No 82-04 (1981)
[9] Blum, M.: How to prove a theorem so no one else can claim it. In: International Congress of Mathematicians, pp. 1444-1451 (1986) · Zbl 0672.94005
[10] Blundo, C.; Masucci, B.; Stinson, DR; Wei, R., Constructions and bounds for unconditionally secure non-interactive commitment schemes, Des. Codes Cryptogr., 26, 1-3, 97-110 (2002) · Zbl 1004.94016 · doi:10.1023/A:1016501125022
[11] Butler, D., Aspinall, D.: Multi-party computation. In: Archive of Formal Proofs (2019)
[12] Butler, D., Aspinall, D., Gascón, 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-130. Springer (2017) · Zbl 1483.68486
[13] Butler, D., Aspinall, D., Gascón, A.: On the formalisation of \(\Sigma \)-protocols and commitment schemes. In: POST, Volume 11426 of Lecture Notes in Computer Science, pp. 175-196. Springer (2019)
[14] Butler, D., Aspinall, D., Gascón, A.: Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL. In: CPP, pp. 229-243. ACM (2020)
[15] Butler, D., Lochbihler, A.: Sigma protocols and commitment schemes. In: Archive of Formal Proofs (2019)
[16] Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: FOCS, pp. 136-145. IEEE Computer Society (2001)
[17] 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)
[18] Chaum, D., Pedersen, T.P.: Wallet databases with observers. In: CRYPTO, Volume 740 of Lecture Notes in Computer Science, pp. 89-105. Springer (1992)
[19] 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) · Zbl 1377.94044
[20] Ciampi, M.; Persiano, G.; Scafuro, A.; Siniscalchi, L.; Visconti, I.; Kushilevitz, E.; Malkin, T., Improved OR-composition of Sigma-protocols, Theory of Cryptography, 112-141 (2016), Berlin: Springer, Berlin · Zbl 1377.94044 · doi:10.1007/978-3-662-49099-0_5
[21] Cramer, R.: Modular design of secure, yet practical cryptographic protocols. Ph.D. Thesis University of Amsterdam (1996) · Zbl 0903.94025
[22] Cramer, R., Damgård, 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-187. Springer (1994) · Zbl 0939.94546
[23] Damgard, I.: On \(\Sigma \)-protocols. Lecture Notes, University of Aarhus, Department for Computer Science (2002)
[24] Damgård, I.: On the existence of bit commitment schemes and zero-knowledge proofs. In: CRYPTO, Volume 435 of Lecture Notes in Computer Science, pp. 17-27. Springer (1989) · Zbl 0724.68030
[25] Damgård, 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-73. Springer (1999) · Zbl 0932.68045
[26] Even, S.: Protocol for signing contracts. In: CRYPTO, pp. 148-153. U. C. Santa Barbara, Dept. of Elec. and Computer Eng., ECE Report No 82-04 (1981)
[27] 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-194. Springer (1986) · Zbl 0636.94012
[28] Goldreich, O., The Foundations of Cryptography—Volume 2: Basic Applications (2004), Cambridge: Cambridge University Press, Cambridge · Zbl 1179.94063 · doi:10.1017/CBO9780511721656
[29] Haagh, H., Karbyshev, A., Oechsner, S., Spitters, B., Strub, P.-Y.: Computer-aided proofs for multiparty computation with active security. In: CSF, pp. 119-131. IEEE Computer Society (2018)
[30] Halevi, S., A plausible approach to computer-aided cryptographic proofs, IACR Cryptol. ePrint Arch., 2005, 181 (2005)
[31] Hazay, C.; Lindell, Y., Efficient Secure Two-Party Protocols—Techniques and Constructions. Information Security and Cryptography (2010), Berlin: Springer, Berlin · Zbl 1208.68005
[32] Lochbihler, A.: CryptHOL. In: Archive of Formal Proofs (2017)
[33] Lochbihler, A., Sefidgar, S.R., Basin, D.A., Maurer, U.: Formalizing constructive cryptography using CryptHOL. In: Computer Security Foundations (CSF 2019), pp. 152-166. IEEE (2019)
[34] 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-287. Springer (2017)
[35] Nipkow, T.; Klein, G., Concrete Semantics—With Isabelle/HOL (2014), Berlin: Springer, Berlin · Zbl 1410.68004
[36] Petcher, A., Morrisett, G.: The foundational cryptography framework. In: POST, Volume 9036 of Lecture Notes in Computer Science, pp. 53-72. Springer (2015)
[37] Rivest, R.: Unconditionally secure commitment and oblivious transfer schemes using private channels and a trusted initializer. Unpublished manuscript (1999)
[38] Schnorr, C-P, Efficient signature generation by smart cards, J. Cryptol., 4, 3, 161-174 (1991) · Zbl 0743.68058 · doi:10.1007/BF00196725
[39] Shoup, V., Sequences of games: a tool for taming complexity in security proofs, IACR Cryptol. ePrint Arch., 2004, 332 (2004)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.