Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Simulating Cities: A Software Engineering Perspective Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Probabilistic Functions and Cryptographic Oracles in Higher Order Logic

Author : Andreas Lochbihler

Published in: Programming Languages and Systems

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter A Classical Realizability Model for a Semantical Value Restriction
next chapter Extensible and Efficient Automation Through Reflective Tactics
Footnotes
1
In the formalisation, we construct the type https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq94_HTML.gif by combining the existing monad for probability mass functions [30] with an exception monad. This way, most of our primitive operations can be defined in terms of the primitive operations of the two monads. Hence, we can derive many of their properties, in particular parametricity (Sect. 2.4), from the latter’s.
 
2
As our embedding is shallow, we cannot define a deduction system in the logic. Rather, we derive the rules directly from the semantics, i.e., show soundness. Completeness is therefore achieved dynamically: new rules can be derived if necessary, in particular when a new operation is introduced.
 
3
Wadler showed that if all types are \(\omega \)-ccpos, all functions are continuous and all relations are admissible and strict, then the fixpoint operator (defined by countable iteration) is parametric [50]. We do not consider the fixpoint operator as part of the language itself, but as a definition principle for recursive user-specified functions. That is, we assume that https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq313_HTML.gif is always applied to a (monotone) function. Consequently, preservation of parametricity suffices and we do not need Wadler’s restrictions of the semantic domains. Instead, monotonicity (instead of continuity, see the discussion in Sect. 2.3) is expressed as a precondition on the given functions.
 
4
Note that https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq354_HTML.gif is not the greatest fixpoint of a polynomial functor, as the recursion goes through the non-polynomial functor https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq355_HTML.gif . Still, the type is well-defined, as https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq356_HTML.gif is a bounded natural functor [30] which Isabelle’s codatatype package supports [22].
 
5
The type constructor https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq426_HTML.gif takes three type arguments, so we should expect https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq427_HTML.gif to take three relations, too. However, the third argument occurs in a negative position in the codatatype definition. Therefore, the relator does not enjoy useful properties such as monotonicity and distributivity over relation composition. Consequently, Isabelle’s infrastructure for parametricity treats these arguments as fixed (dead in the terminology of [22]). So, https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq428_HTML.gif takes only relations for the first two arguments and fixes the third to the identity relation https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq429_HTML.gif as can be seen in (5). In practice, we have not found this specialisation to be restrictive.
 
6
In fact, parametricity actually yields a rule stronger than (6), namely the gpv v need not be the same on both sides. If https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq440_HTML.gif and the premises of (6) hold, then https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq441_HTML.gif .
 
7
The oracle transformation in this reduction is degenerate, as https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq502_HTML.gif emulates the oracle without access to further oracles. Thus, we use https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq503_HTML.gif directly instead of https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49498-1_20/978-3-662-49498-1_20_IEq504_HTML.gif .
 
Literature
1.
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (The computational soundness of formal encryption). J. Cryptology 15(2), 103–127 (2002)MathSciNetCrossRefMATH
2.
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)MathSciNetCrossRefMATH
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)CrossRef
5.
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)CrossRef
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.
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)
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)CrossRef
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)
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)CrossRef
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)CrossRef
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)CrossRef
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)
23.
Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: A proof assistant perspective. In: ICFP 2015, pp. 192–204. ACM (2015)
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)MathSciNetCrossRefMATH
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)MathSciNetCrossRefMATH
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)
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)CrossRef
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)CrossRef
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)CrossRef
36.
37.
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)CrossRef
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)MATH
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)
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.
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)CrossRef
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)MathSciNetCrossRefMATH
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)
Metadata
Title
Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
Author
Andreas Lochbihler
Copyright Year
2016
Publisher
Springer Berlin Heidelberg
Book
Programming Languages and Systems

Print ISBN: 978-3-662-49497-4

Electronic ISBN: 978-3-662-49498-1

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-662-49498-1_20

Premium Partner

    Image Credits