CryptHOL: game-based proofs in higher-order logic. (English) Zbl 1455.94121
Summary: Game-based proofs are a well-established paradigm for structuring security arguments and simplifying their understanding. We present a novel framework, CryptHOL, for rigorous game-based proofs that is supported by mechanical theorem proving. CryptHOL is based on a new semantic domain with an associated functional programming language for expressing games. We embed our framework in the Isabelle/HOL theorem prover and, using the theory of relational parametricity, we tailor Isabelle’s existing proof automation to game-based proofs. By basing our framework on a conservative extension of higher-order logic and providing automation support, the resulting proofs are trustworthy and comprehensible, and the framework is extensible and widely applicable. We evaluate our framework by formalising different game-based proofs from the literature and comparing the results with existing formal-methods tools.
MSC:
| 94A60 | Cryptography |
| 94A62 | Authentication, digital signatures and secret sharing |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 91A99 | Game theory |
Software:
Isabelle/HOL; HOL; ML; Autoref; Zoo Probabilistic Systems; F*; miz3; AmiCo; Nuprl; MFMC_Countable; Probabilistic_While; Game_Based_Crypto; EasyCrypt; Transfer; Lifting; Archive Formal Proofs; CryptHOLReferences:
| [1] | G. Asharov, A. Beimel, N. Makriyannis, E. Omri, Complete characterization of fairness in secure two-party computation of boolean functions, in Dodis, Y., Nielsen, J.B. (eds.) TCC 2015. LNCS, vol. 9014, (Springer, 2015), pp. 199-228 · Zbl 1354.94020 |
| [2] | Audebaud, P.; Paulin-Mohring, C., Proofs of randomized algorithms in Coq, Sci. Comput. Program., 74, 8, 568-589 (2009) · Zbl 1178.68667 |
| [3] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge: Cambridge University Press, Cambridge |
| [4] | M. Backes, M. Berg, D. Unruh, A formal language for cryptographic pseudocode, in LPAR 2008. LNCS, vol. 5330, (Springer, 2008), pp. 353-376 · Zbl 1182.94035 |
| [5] | G. Barthe, C. Fournet, B. Grégoire, P.Y. Strub, N. Swamy, S. Zanella Béguelin, Probabilistic relational verification for cryptographic implementations. in POPL 2014. (ACM, 2014) pp. 193-205 · Zbl 1284.68380 |
| [6] | G. Barthe, B. Grégoire, S. Heraud, S. Zanella Béguelin, Computer-aided security proofs for the working cryptographer. in CRYPTO 2011. LNCS, vol. 6841, (Springer 2011), pp. 71-90 · Zbl 1287.94048 |
| [7] | G. Barthe, B. Grégoire, J. Hsu, P.Y. Strub, Coupling proofs are probabilistic product programs. in POPL 2017. (ACM, 2017), pp. 161-174 · Zbl 1380.68267 |
| [8] | G. Barthe, B. Grégoire, S. Zanella Béguelin, Formal certification of code-based cryptographic proofs. in POPL 2009. (ACM, 2009), pp. 90-101 · Zbl 1315.68081 |
| [9] | Basin, D.; Kaufmann, M.; Huet, G.; Plotkin, G., The Boyer-Moore prover and Nuprl: An experimental comparison, Logical Frameworks, 89-119 (1991), Cambridge: Cambridge University Press, Cambridge · Zbl 0799.68169 |
| [10] | M. Bellare, A. Boldyreva, S. Micali, Public-key encryption in a multi-user setting: Security proofs and improvements. in Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, (Springer, 2000), pp. 259-274 · Zbl 1082.94504 |
| [11] | M. Bellare, P. Rogaway, Optimal asymmetric encryption. in Workshop on the Theory and Application of Cryptographic Techniques. (Springer, 1994), pp. 92-111 · Zbl 0881.94010 |
| [12] | M. Bellare, P. Rogaway, Code-based game-playing proofs and the security of triple encryption. Cryptology ePrint Archive, Report 2004/331 (2004), http://eprint.iacr.org/2004/331 · Zbl 1140.94321 |
| [13] | M. Bellare, P. Rogaway, The security of triple encryption and a framework for code-based game-playing proofs. in EUROCRYPT 2006. LNCS, vol. 4004, (Springer, 2006), pp. 409-426 · Zbl 1140.94321 |
| [14] | Bengtson, J.; Bhargavan, K.; Fournet, C.; Gordon, AD; Maffeis, S., Refinement types for secure implementations, ACM Trans. Program. Lang. Syst., 33, 2, 8:1-8:45 (2011) |
| [15] | M. Berg, Formal verification of cryptographic security proofs. Ph.D. thesis, Universität des Saarlandes (2013) |
| [16] | S. Berghofer, M. Wenzel, Logic-free reasoning in Isabelle/Isar. in Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) CICM 2008. LNCS, vol. 5144, (Springer, 2008), pp. 355-369 · Zbl 1166.68337 |
| [17] | K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, P.Y. Strub, Implementing TLS with verified cryptographic security. in S&P 2013. (IEEE, 2013), pp. 445-459 |
| [18] | Blanchet, B., A computationally sound mechanized prover for security protocols, IEEE Trans. Dependable Secure Comput., 5, 4, 193-207 (2008) |
| [19] | J.C. Blanchette, A. Bouzy, A. Lochbihler, A. Popescu, D. Traytel, Friends with benefits: Implementing corecursion in foundational proof assistants. in Yang, H. (ed.) ESOP 2017. LNCS, (Springer 2017), pp. 111-140 · Zbl 1485.68280 |
| [20] | J.C. Blanchette, J. Hölzl, A. Lochbihler, L. Panny, Popescu, A., D. Traytel, Truly modular (co)datatypes for Isabelle/HOL. in ITP 2014. LNCS, vol. 8558, (Springer, 2014), pp. 93-110 · Zbl 1416.68151 |
| [21] | D. Butler, D. Aspinall, A. Gascon, How to simulate it in Isabelle: Towards formal proof for secure multi-party computation (2017), accepted at ITP 2017 · Zbl 1483.68486 |
| [22] | D. Butler, D. Aspinall, A. Gascón, On the formalisation of \(\varSigma \)-protocols and commitment schemes. in Nielson, F., Sands, D. (eds.) POST 2019. LNCS, vol. 11426, (Springer, 2019), pp. 175-196 · Zbl 1524.94062 |
| [23] | R. Canetti, Universally composable security: A new paradigm for cryptographic protocols. in Proceedings of 42nd IEEE Symposium on Foundations of Computer Science, 2001. (IEEE, 2001), pp. 136-145 |
| [24] | Church, A., A formulation of the simple theory of types, J. Symb. Log., 5, 2, 56-68 (1940) · JFM 66.1192.06 |
| [25] | R. Cohen, S. Coretti, J. Garay, V. Zikas, Probabilistic termination and composability of cryptographic protocols. in Robshaw, M., Katz, J. (eds.) CRYPTO 2016. LNCS, vol. 9816, (Springer ,2016), pp. 240-269 · Zbl 1406.94040 |
| [26] | Easycrypt: Reference manual. https://www.easycrypt.info/documentation/refman.pdf (2018), version 1.x, 19 February 2018 |
| [27] | Elgamal, T., A public key cryptosystem and a signature scheme based on discrete logarithms, IEEE Trans. Inf. Theory, 31, 4, 469-472 (1985) · Zbl 0571.94014 |
| [28] | Goldwasser, S.; Micali, S., Probabilistic encryption, J. Comput. Syst. Sci., 28, 2, 270-299 (1984) · Zbl 0563.94013 |
| [29] | Gordon, SD; Hazay, C.; Katz, J.; Lindell, Y., Complete fairness in secure two-party computation, J. ACM, 58, 6, 24:1-24:37 (2011) · Zbl 1281.94081 |
| [30] | O. Grumberg, N. Francez, S. Katz, Fair termination of communicating processes. in PODC 1984. (ACM, 1984), pp. 254-265 |
| [31] | S. Halevi, A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181 (2005) |
| [32] | M. Hofmann, A. Karbyshev, H. Seidl, What is a pure functional? in Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, (Springer 2010), pp. 199-210 · Zbl 1288.68037 |
| [33] | J. Hölzl, A. Lochbihler, D. Traytel, A formalized hierarchy of probabilistic system types. in ITP 2015. LNCS, vol. 9236, (Springer, 2015), pp. 203-220 · Zbl 1465.68199 |
| [34] | B. Huffman, O. Kunčar, Lifting and Transfer: A modular design for quotients in Isabelle/HOL. in CPP 2013. LNCS, vol. 8307, (Springer, 2013), pp. 131-146 · Zbl 1426.68284 |
| [35] | J. Hurd, A formal approach to probabilistic termination. in TPHOLs 2002. LNCS, vol. 2410, (Springer, 2002), pp. 230-245 · Zbl 1013.68193 |
| [36] | Kilian, J.; Rogaway, P., How to protect DES against exhaustive key search (an analysis of DESX), J. Cryptol., 14, 1, 17-35 (2001) · Zbl 1068.94531 |
| [37] | Knuth, DE; Yao, AC; Traub, JF, The complexity of nonuniform random number generation, Algorithms and Complexity-New Directions and Recent Results, 357-428 (1976), New York: Academic Press Inc, New York · Zbl 0395.65004 |
| [38] | Koblitz, N.; Menezes, AJ, Another look at “provable security”, J. Cryptol., 20, 1, 3-37 (2007) · Zbl 1115.68078 |
| [39] | A. Krauss, Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. Ph.D. thesis, Technische Universität München (2009) |
| [40] | A. Krauss, Recursive definitions of monadic functions. in PAR 2010. EPTCS, vol. 43, pp. 1-13 (2010) |
| [41] | O. Kunčar, A. Popescu, A consistent foundation for Isabelle/HOL. in Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, (Springer, 2015), pp. 234-252 · Zbl 1433.68556 |
| [42] | O. Kunčar, A. Popescu, Comprehending Isabelle/HOL’s consistency. in Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, (Springer, 2017), pp. 724-749 · Zbl 1485.68285 |
| [43] | O. Kunčar, A. Popescu, Safety and conservativity of definitions in HOL and Isabelle/HOL. in POPL 2018. Proc. ACM Program. Lang., vol. 2, (ACM, 2017), pp. 24:1-24:26 |
| [44] | P. Lammich, Automatic data refinement. in ITP 2013. LNCS, vol. 7998, (Springer, 2013), pp. 84-99 · Zbl 1317.68216 |
| [45] | Larsen, KG; Skou, A., Bisimulation through probabilistic testing, Inf. Comp., 94, 1, 1-28 (1991) · Zbl 0756.68035 |
| [46] | Lindvall, T., Lectures on the Coupling Method (2002), New York: Dover Publications, Inc., New York · Zbl 1013.60001 |
| [47] | A. Lochbihler, A formal proof of the max-flow min-cut theorem for countable networks. Archive of Formal Proofs (2016), http://isa-afp.org/entries/MFMC_Countable.shtml, Formal proof development · Zbl 07699442 |
| [48] | A. Lochbihler, Probabilistic functions and cryptographic oracles in higher order logic. in Thiemann, P. (ed.) Programming Languages and Systems (ESOP 2016). LNCS, vol. 9632, (Springer, 2016), pp. 503-531 · Zbl 1335.68033 |
| [49] | A. Lochbihler, CryptHOL. Archive of Formal Proofs (2017), http://isa-afp.org/entries/CryptHOL.shtml, Formal proof development |
| [50] | A. Lochbihler, Probabilistic while loop. Archive of Formal Proofs (2017), http://isa-afp.org/entries/Probabilistic_While.html, Formal proof development |
| [51] | A. Lochbihler, S.R. Sefidgar, A tutorial introduction to CryptHOL. Cryptology ePrint Archive, Report 2018/941 (2018), https://eprint.iacr.org/2018/941 |
| [52] | A. Lochbihler, S.R. Sefidgar, D.A. Basin, U. Maurer, Formalizing constructive cryptography using CryptHOL. in CSF 2019. (IEEE Computer Society, 2019), pp. 152-166 |
| [53] | A. Lochbihler, S.R. Sefidgar, B. Bhatt, Game-based cryptography in HOL. Archive of Formal Proofs (2017), http://isa-afp.org/entries/Game_Based_Crypto.shtml, Formal proof development |
| [54] | A. Lochbihler, M. Züst, Programming TLS in Isabelle/HOL. Isabelle Workshop 2014 (2014) |
| [55] | J. Lumbroso, Optimal discrete uniform generation from coin flips, and applications. CoRR arXiv:1304.1916 (2013) |
| [56] | U. Maurer, Constructive cryptography – a new paradigm for security definitions and proofs. in Moedersheim, S., Palamidessi, C. (eds.) Theory of Security and Applications (TOSCA 2011). LNCS, vol. 6993, (Springer, 2011), pp. 33-56 · Zbl 1378.94055 |
| [57] | D. Micciancio, S. Tessaro, An equational approach to secure multi-party computation. in ITCS 2013. (ACM, 2013), pp. 355-372 · Zbl 1362.68080 |
| [58] | Milner, R.; Rose, HE; Shepherdson, J., Processes: A mathematical model of computing agents, Logic Colloquium 1973, Studies in Logic and the Foundations of Mathematics, 157-173 (1975), New York: Elsevier, New York · Zbl 0316.68017 |
| [59] | Milner, R., A theory of type polymorphism in programming, J. Comput. Syst. Sci., 17, 3, 348-375 (1978) · Zbl 0388.68003 |
| [60] | J.C. Mitchell, Representation independence and data abstraction. in POPL 1986. (ACM, 1986), pp. 263-276 |
| [61] | Nipkow, T.; Klein, G., Concrete Semantics (2014), New York: Springer, New York · Zbl 1410.68004 |
| [62] | Nipkow, T.; Paulson, LC; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS (2002), New York: Springer, New York · Zbl 0994.68131 |
| [63] | R. Pass, E. Shi, F. Tramer, Formal abstractions for attested execution secure processors. Cryptology ePrint Archive, Report 2016/1027 (2016), http://eprint.iacr.org/2016/1027 · Zbl 1411.94082 |
| [64] | A. Petcher, G. Morrisett, The foundational cryptography framework. in POST 2015. LNCS, vol. 9036, (Springer, 2015), pp. 53-72 |
| [65] | A. Petcher, G. Morrisett, A mechanized proof of security for searchable symmetric encryption. in CSF 2015. (IEEE 2015), pp. 481-494 |
| [66] | M. Piróg, J. Gibbons, The coinductive resumption monad. in Jacobs, B., Silva, A., Staton, S. (eds.) MFPS 2014. ENTCS, vol. 308, (2014), pp. 273-288 · Zbl 1337.68189 |
| [67] | Pitts, AM; Gordon, MJC; Melham, TF, The HOL logic, Introduction to HOL: a theorem proving environment for higher order logic, 191-232 (1993), Cambridge: Cambridge University Press, Cambridge · Zbl 0779.68007 |
| [68] | N. Ramsey, A. Pfeffer, Stochastic lambda calculus and monads of probability distributions. in POPL 2002. (ACM, 2002), pp. 154-165 · Zbl 1323.68150 |
| [69] | J.C. Reynolds, Types, abstraction and parametric polymorphism. in IFIP 1983. Information Processing, vol. 83, (North-Holland/IFIP, 1983), pp. 513-523 |
| [70] | J. Sack, L. Zhang, A general framework for probabilistic characterizing formulae. in VMCAI 2012. LNCS, vol. 7148, (Springer, 2012), pp. 396-411 · Zbl 1326.68176 |
| [71] | N. Schirmer, M. Wenzel, State spaces – the locale way. in Huuck, R., Klein, G., Schlich, B. (eds.) SSV 2009. Electronic Notes in Theoretical Computer Science, vol. 254, (2009), pp. 161-179 |
| [72] | R. Segala, Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology (1995) |
| [73] | V. Shoup, OAEP reconsidered. in Annual International Cryptology Conference. (Springer, 2001), pp. 239-259 · Zbl 1002.94519 |
| [74] | V. Shoup, Sequences of games: A tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332 (2004), http://eprint.iacr.org/2004/332 |
| [75] | N.P. Smart, Cryptography Made Simple. Information Security and Cryptography, Springer (2016) · Zbl 1401.94002 |
| [76] | A. Sokolova, Coalgebraic Analysis of Probabilistic Systems. Ph.D. thesis, Technische Universiteit Eindhoven (2005) |
| [77] | J. Stern, D. Pointcheval, J. Malone-Lee, N.P. Smart, Flaws in applying proof methodologies to signature schemes. in Annual International Cryptology Conference. (Springer, 2002), pp. 93-110 · Zbl 1026.94550 |
| [78] | P.Y. Strub, Some questions. Easycrypt Mailing list, post 383. https://lists.gforge.inria.fr/pipermail/easycrypt-club/2016-March/000383.html (2016) |
| [79] | Swamy, N.; Chen, J.; Fournet, C.; Strub, PY; Bhargavan, K.; Yang, J., Secure distributed programming with value-dependent types, J. Funct. Program., 23, 4, 402-451 (2013) · Zbl 1290.68033 |
| [80] | P. Wadler, Theorems for free! in FPCA 1989. (ACM, 1989), pp. 347-359 |
| [81] | P. Wadler, The essence of functional programming. in POPL 1992. (ACM, 1992), pp. 1-14 |
| [82] | F. Wiedijk, A synthesis of the procedural and declarative styles of interactive theorem proving. Logical Methods in Computer Science 8(1:30), (2012) · Zbl 1238.68147 |
| [83] | L. Xi, K. Yang, Z. Zhang, D. Feng, DAA-related APIs in TPM 2.0 revisited. in (International Conference on Trust and Trustworthy Computing). (Springer, 2014), pp. 1-18 |
| [84] | A.C. Yao, Theory and application of trapdoor functions. in FOCS 1982. (IEEE Computer Society, 1982), pp. 80-91 |
| [85] | S. Zanella Béguelin, Formal Certification of Game-Based Cryptographic Proofs. Ph.D. thesis, École Nationale Supérieure des Mines de Paris (2010) · Zbl 1315.68081 |
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.
