On Higher-Order Cryptography
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.
Higher-order computation
probabilistic computation
game semantics
cryptography
Theory of computation~Denotational semantics
Theory of computation~Probabilistic computation
Theory of computation~Cryptographic primitives
108:1-108:16
Track B: Automata, Logic, Semantics, and Theory of Programming
An extended version [Barak et al., 2020] of this paper is available at https://arxiv.org/abs/2002.07218.
We thank Juspreet Singh Sandhu for helpful discussions during the early stages of this project.
Boaz
Barak
Boaz Barak
Harvard University, Cambridge, MA, USA
is supported by NSF awards CCF 1565264 and CNS 1618026 and by a Simons Investigator Fellowship.
Raphaëlle
Crubillé
Raphaëlle Crubillé
IMDEA Software Institute, Madrid, Spain
University of Paris, IRIF, France
Ugo
Dal Lago
Ugo Dal Lago
University of Bologna, Italy
INRIA, Sophia Antipolis, France
is supported by the ERC CoG 818616 "DIAPASoN", and by the ANR grants 19CE480014 "PPS" and 16CE250011 "REPAS".
10.4230/LIPIcs.ICALP.2020.108
Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. J. Symb. Log., 59(2):543-574, 1994.
Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409-470, 2000.
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.
http://arxiv.org/abs/2002.07218
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.
Manuel Blum and Silvio Micali. How to generate cryptographically strong sequences of pseudo-random bits. SIAM J. Comput., 13(4):850-864, 1984.
Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A core quantitative coeffect calculus. In Proc. of ESOP 2014, pages 351-370, 2014.
Ran Canetti. Universally composable security: A new paradigm for cryptographic protocols. In Proc. of FOCS 2001, pages 136-145, 2001.
Pierre Clairambault and Hugo Paquet. Fully abstract models of the probabilistic lambda-calculus. In Proc. of CSL 2018, pages 16:1-16:17, 2018.
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.
Pierre-Louis Curien and Hugo Herbelin. Abstract machines for dialogue games. CoRR, abs/0706.2544, 2007.
Vincent Danos and Russell Harmer. Probabilistic game semantics. ACM Trans. Comput. Log., 3(3):359-382, 2002.
Danny Dolev and Andrew Chi-Chih Yao. On the security of public key protocols. IEEE Trans. Inf. Theory, 29(2):198-207, 1983.
Hugo Férée. Game semantics approach to higher-order complexity. J. Comput. Syst. Sci., 87:1-15, 2017.
Olle Fredriksson and Dan R. Ghica. Abstract machines for game semantics, revisited. In Proc. of LICS 2013, pages 560-569, 2013.
Dan R. Ghica. Geometry of synthesis: a structured approach to VLSI design. In Proc. of POPL 2007, pages 363-375, 2007.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987.
Jean-Yves Girard. Geometry of interaction 1: Interpretation of system F. Logic Colloquium 88, 1989.
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.
Oded Goldreich. Foundations of Cryptography: Volume 1. Cambridge University Press, 2006.
Oded Goldreich. Foundations of Cryptography: Volume 2, Basic Applications. Cambridge University Press, 2009.
Oded Goldreich, Shafi Goldwasser, and Silvio Micali. How to construct random functions. J. ACM, 33(4):792-807, 1986.
Martin Hyland. Game semantics. In Andy Pitts and Peter Dybjer, editors, Semantics and Logics of Computation. Cambridge University Press, 1997.
Martin Hyland and Luke Ong. On full abstraction for PCF: I, II, and III. Inf. Comput., 163(2):285-408, 2000.
Jonathan Katz and Yehuda Lindell. Introduction to Modern Cryptography. Chapman & Hall/CRC, 2007.
Akitoshi Kawamura and Stephen A. Cook. Complexity theory for operators in analysis. TOCT, 4(2):5:1-5:24, 2012.
John Longley and Dag Normann. Higher-Order Computability. Theory and Applications of Computability. Springer, 2015.
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.
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.
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.
Eijiro Sumii and Benjamin C. Pierce. Logical relations for encryption. Journal of Computer Security, 11(4):521-554, 2003.
Klaus Weihrauch. Computable Analysis: An Introduction. Springer Publishing Company, Incorporated, 2013.
Nicholas Wolverson. Game semantics for an object-oriented language. PhD thesis, University of Edinburgh, UK, 2009.
Boaz Barak, Raphaëlle Crubillé, and Ugo Dal Lago
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode