Probabilistic functions and cryptographic oracles in higher order logic. (English) Zbl 1335.68033

Thiemann, Peter (ed.), Programming languages and systems. 25th European symposium on programming, ESOP 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49497-4/pbk; 978-3-662-49498-1/ebook). Lecture Notes in Computer Science 9632, 503-531 (2016).
Summary: This paper presents a shallow embedding of a probabilistic functional programming language in higher order logic. The language features monadic sequencing, recursion, random sampling, failures and failure handling, and black-box access to oracles. Oracles are probabilistic functions which maintain hidden state between different invocations. To that end, we propose generative probabilistic systems as the semantic domain in which the operators of the language are defined. We prove that these operators are parametric and derive a relational program logic for reasoning about programs from parametricity. Several examples demonstrate that our language is suitable for conducting cryptographic proofs.
For the entire collection see [Zbl 1333.68019].


68N18 Functional programming and lambda calculus
94A60 Cryptography
Full Text: DOI


[1] Abadi, M., Rogaway, P.: Reconciling two views of cryptography (The computational soundness of formal encryption). J. Cryptology 15(2), 103–127 (2002) · Zbl 0994.68066
[2] Affeldt, R., Hagiwara, M., Sénizergues, J.: Formalization of Shannon’s theorems. J. Automat. Reason. 53(1), 63–103 (2014) · Zbl 1315.68216
[3] Aharoni, R., Berger, E., Georgakopoulos, A., Perlstein, A., Sprüssel, P.: The max-flow min-cut theorem for countable networks. J. Combin. Theory Ser. B 101, 1–17 (2011) · Zbl 1221.05186
[4] Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267–282. Springer, Heidelberg (2012) · Zbl 06051091
[5] Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568–589 (2009) · Zbl 1178.68667
[6] Bacelar Almeida, J., Barbosa, M., Bangerter, E., Barthe, G., Krenn, S., Zanella Béguelin, S.: Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols. In: CCS 2012, pp. 488–500. ACM (2012)
[7] Backes, M., Barthe, G., Berg, M., Grégoire, B., Kunz, C., Skoruppa, M., Zanella Béguelin, S.: Verified security of Merkle-Damgård. In: CSF 2012, pp. 354–368 (2012)
[8] Backes, M., Berg, M., Unruh, D.: A formal language for cryptographic pseudocode. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 353–376. Springer, Heidelberg (2008) · Zbl 1182.94035
[9] Backes, M., Hofheinz, D., Unruh, D.: CoSP: a general framework for computational soundness proofs. In: CCS 2009, pp. 66–78. ACM (2009)
[10] Backes, M., Malik, A., Unruh, D.: Computational soundness without protocol restrictions. In: CCS 2012, pp. 699–711. ACM (2012)
[11] Ballarin, C.: Locales: A module system for mathematical theories. J. Automat. Reason. 52(2), 123–153 (2014) · Zbl 1315.68218
[12] Barthe, G., Fournet, C., Grégoire, B., Strub, P.Y., Swamy, N., Zanella Béguelin, S.: Probabilistic relational verification for cryptographic implementations. In: POPL 2014, pp. 193–205. ACM (2014) · Zbl 1284.68380
[13] Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (2011) · Zbl 1287.94048
[14] Barthe, G., Grégoire, B., Zanella Béguelin, S.: Formal certification of code-based cryptographic proofs. In: POPL 2009, pp. 90–101. ACM (2009) · Zbl 1315.68081
[15] Bellare, M., Rogaway, P.: Random oracles are practical: a paradigm for designing efficient protocols. In: CCS 1993, pp. 62–73. ACM (1993)
[16] Bellare, M., Rogaway, P.: The security of triple encryption and a framework for code-based game-playing proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol. 4004, pp. 409–426. Springer, Heidelberg (2006) · Zbl 1140.94321
[17] Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. ACM Trans. Program. Lang. Syst. 33(2), 8:1–8:45 (2011)
[18] Bhargavan, K., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.Y.: Implementing TLS with verified cryptographic security. In: S&P 2013, pp. 445–459. IEEE (2013)
[19] Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW 2001, pp. 82–96. IEEE (2001)
[20] Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Secure Comput. 5(4), 193–207 (2008)
[21] Blanchet, B., Jaggard, A.D., Rao, J., Scedrov, A., Tsay, J.K.: Refining computationally sound mechanized proofs for Kerberos. In: FCC 2009 (2009)
[22] Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (Co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93–110. Springer, Heidelberg (2014) · Zbl 1416.68151
[23] Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: A proof assistant perspective. In: ICFP 2015, pp. 192–204. ACM (2015) · Zbl 1360.68358
[24] Cock, D.: Verifying probabilistic correctness in Isabelle with pGCL. In: SSV 2012. EPTCS, vol. 102, pp. 1–10 (2012)
[25] Cortier, V., Kremer, S., Warinschi, B.: A survey of symbolic methods in computational analysis of cryptographic systems. J. Automat. Reason. 46, 225–259 (2011) · Zbl 1213.94093
[26] Desharnais, J.: Labelled Markov Processes. Ph.D. thesis, McGill University (1999)
[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] Gunter, E.L.: Why we can’t have SML-style datatype declarations in HOL. In: Claesen, L.J.M., Gordon, M.J.C. (eds.) TPHOLs 1992, pp. 561–568. Elsevier, North-Holland (1993)
[29] Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181 (2005)
[30] Hölzl, J., Lochbihler, A., Traytel, D.: A formalized hierarchy of probabilistic system types. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 203–220. Springer, Heidelberg (2015) · Zbl 1465.68199
[31] Huffman, B., Kunčar, O.: Lifting and Transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Heidelberg (2013) · Zbl 1426.68284
[32] Hurd, J.: A formal approach to probabilistic termination. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 230–245. Springer, Heidelberg (2002) · Zbl 1013.68193
[33] Jouannaud, J.P., Xu, W.: Automatic complexity analysis for programs extracted from Coq proof. In: CLASE 2005. ENTCS, vol. 153(1), pp. 35–53 (2006)
[34] Krauss, A.: Recursive definitions of monadic functions. In: PAR 2010. EPTCS, vol. 43, pp. 1–13 (2010)
[35] Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 84–99. Springer, Heidelberg (2013) · Zbl 1317.68216
[36] Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comp. 94(1), 1–28 (1991) · Zbl 0756.68035
[37] Lochbihler, A.: Formalisation accompanying this paper. http://www.infsec.ethz.ch/research/projects/FCSPI/ESOP2016.html
[38] Lochbihler, A., Züst, M.: Programming TLS in Isabelle/HOL. Isabelle Workshop 2014 (2014)
[39] Meier, S., Cremers, C.J.F., Basin, D.: Efficient construction of machine-checked symbolic protocol security proofs. J. Comput. Secur. 21(1), 41–87 (2013)
[40] Mitchell, J.C.: Representation independence and data abstraction. In: POPL 1986, pp. 263–276. ACM (1986)
[41] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131
[42] Petcher, A., Morrisett, G.: The foundational cryptography framework. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 53–72. Springer, Heidelberg (2015) · Zbl 06571759
[43] Petcher, A., Morrisett, G.: A mechanized proof of security for searchable symmetric encryption. In: CSF 2015, pp. 481–494. IEEE (2015)
[44] Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP 1983. Information Processing, vol. 83, pp. 513–523. North-Holland/IFIP (1983)
[45] Rutten, J.J.M.M.: Relators and metric bisimulations. Electr. Notes Theor. Comput. Sci. 11, 252–258 (1998) · Zbl 0917.68146
[46] Sack, J., Zhang, L.: A general framework for probabilistic characterizing formulae. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 396–411. Springer, Heidelberg (2012) · Zbl 1326.68176
[47] Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: CSF 2012, pp. 78–94. IEEE (2012)
[48] Shoup, V.: Sequences of games: A tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332 (2004)
[49] Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. J. Funct. Program. 23(4), 402–451 (2013) · Zbl 1290.68033
[50] Wadler, P.: Theorems for free! In: FPCA 1989, pp. 347–359. ACM (1989)
[51] Zanella Béguelin, S.: 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.