On Higher-Order Cryptography

Authors Boaz Barak, Raphaëlle Crubillé, Ugo Dal Lago

Thumbnail PDF


  • Filesize: 0.62 MB
  • 16 pages

Document Identifiers

Author Details

Boaz Barak
  • Harvard University, Cambridge, MA, USA
Raphaëlle Crubillé
  • IMDEA Software Institute, Madrid, Spain
  • University of Paris, IRIF, France
Ugo Dal Lago
  • University of Bologna, Italy
  • INRIA, Sophia Antipolis, France


We thank Juspreet Singh Sandhu for helpful discussions during the early stages of this project.

Cite AsGet BibTex

Boaz Barak, Raphaëlle Crubillé, and Ugo Dal Lago. On Higher-Order Cryptography. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 108:1-108:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Type-two constructions abound in cryptography: adversaries for encryption and authentication schemes, if active, are modeled as algorithms having access to oracles, i.e. as second-order algorithms. But how about making cryptographic schemes themselves higher-order? This paper gives an answer to this question, by first describing why higher-order cryptography is interesting as an object of study, then showing how the concept of probabilistic polynomial time algorithm can be generalized so as to encompass algorithms of order strictly higher than two, and finally proving some positive and negative results about the existence of higher-order cryptographic primitives, namely authentication schemes and pseudorandom functions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Probabilistic computation
  • Theory of computation → Cryptographic primitives
  • Higher-order computation
  • probabilistic computation
  • game semantics
  • cryptography


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. J. Symb. Log., 59(2):543-574, 1994. Google Scholar
  2. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409-470, 2000. Google Scholar
  3. Boaz Barak, Raphaëlle Crubillé, and Ugo Dal Lago. On higher-order cryptography (long version). CoRR, abs/2002.07218, 2020. URL: http://arxiv.org/abs/2002.07218.
  4. Karthikeyan Bhargavan, Cédric Fournet, and Andrew D. Gordon. Modular verification of security protocol code by typing. In Proc. of POPL 2010, pages 445-456, 2010. Google Scholar
  5. Manuel Blum and Silvio Micali. How to generate cryptographically strong sequences of pseudo-random bits. SIAM J. Comput., 13(4):850-864, 1984. Google Scholar
  6. Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A core quantitative coeffect calculus. In Proc. of ESOP 2014, pages 351-370, 2014. Google Scholar
  7. Ran Canetti. Universally composable security: A new paradigm for cryptographic protocols. In Proc. of FOCS 2001, pages 136-145, 2001. Google Scholar
  8. Pierre Clairambault and Hugo Paquet. Fully abstract models of the probabilistic lambda-calculus. In Proc. of CSL 2018, pages 16:1-16:17, 2018. Google Scholar
  9. Stephen A. Cook and Bruce M. Kapron. Characterizations of the basic feasible functionals of finite type. In Proc. of FOCS 1989, pages 154-159, 1989. Google Scholar
  10. Pierre-Louis Curien and Hugo Herbelin. Abstract machines for dialogue games. CoRR, abs/0706.2544, 2007. Google Scholar
  11. Vincent Danos and Russell Harmer. Probabilistic game semantics. ACM Trans. Comput. Log., 3(3):359-382, 2002. Google Scholar
  12. Danny Dolev and Andrew Chi-Chih Yao. On the security of public key protocols. IEEE Trans. Inf. Theory, 29(2):198-207, 1983. Google Scholar
  13. Hugo Férée. Game semantics approach to higher-order complexity. J. Comput. Syst. Sci., 87:1-15, 2017. Google Scholar
  14. Olle Fredriksson and Dan R. Ghica. Abstract machines for game semantics, revisited. In Proc. of LICS 2013, pages 560-569, 2013. Google Scholar
  15. Dan R. Ghica. Geometry of synthesis: a structured approach to VLSI design. In Proc. of POPL 2007, pages 363-375, 2007. Google Scholar
  16. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. Google Scholar
  17. Jean-Yves Girard. Geometry of interaction 1: Interpretation of system F. Logic Colloquium 88, 1989. Google Scholar
  18. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: A modular approach to polynomial-time computability. Theor. Comput. Sci., 97(1):1-66, 1992. Google Scholar
  19. Oded Goldreich. Foundations of Cryptography: Volume 1. Cambridge University Press, 2006. Google Scholar
  20. Oded Goldreich. Foundations of Cryptography: Volume 2, Basic Applications. Cambridge University Press, 2009. Google Scholar
  21. Oded Goldreich, Shafi Goldwasser, and Silvio Micali. How to construct random functions. J. ACM, 33(4):792-807, 1986. Google Scholar
  22. Martin Hyland. Game semantics. In Andy Pitts and Peter Dybjer, editors, Semantics and Logics of Computation. Cambridge University Press, 1997. Google Scholar
  23. Martin Hyland and Luke Ong. On full abstraction for PCF: I, II, and III. Inf. Comput., 163(2):285-408, 2000. Google Scholar
  24. Jonathan Katz and Yehuda Lindell. Introduction to Modern Cryptography. Chapman & Hall/CRC, 2007. Google Scholar
  25. Akitoshi Kawamura and Stephen A. Cook. Complexity theory for operators in analysis. TOCT, 4(2):5:1-5:24, 2012. Google Scholar
  26. John Longley and Dag Normann. Higher-Order Computability. Theory and Applications of Computability. Springer, 2015. Google Scholar
  27. John C. Mitchell, Mark Mitchell, and Andre Scedrov. A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In Proc. of FOCS 1998, pages 725-733, 1998. Google Scholar
  28. John C. Mitchell, Ajith Ramanathan, Andre Scedrov, and Vanessa Teague. A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theor. Comput. Sci., 353(1-3):118-164, 2006. Google Scholar
  29. Ryan O'Donnell, Michael E. Saks, Oded Schramm, and Rocco A. Servedio. Every decision tree has an in.uential variable. In Proc. of FOCS 2005, pages 31-39, 2005. Google Scholar
  30. Eijiro Sumii and Benjamin C. Pierce. Logical relations for encryption. Journal of Computer Security, 11(4):521-554, 2003. Google Scholar
  31. Klaus Weihrauch. Computable Analysis: An Introduction. Springer Publishing Company, Incorporated, 2013. Google Scholar
  32. Nicholas Wolverson. Game semantics for an object-oriented language. PhD thesis, University of Edinburgh, UK, 2009. Google Scholar