Abstract
We define a call-by-value variant of Gödel’s system \(\textsf {T} \) with references, and equip it with a linear dependent type and effect system, called \(\textsf {d}\ell \textsf {T} \), that can estimate the time complexity of programs, as a function of the size of their inputs. We prove that the type system is intentionally sound, in the sense that it over-approximates the complexity of executing the programs on a variant of the CEK abstract machine. Moreover, we define a sound and complete type inference algorithm which critically exploits the subrecursive nature of \(\textsf {d}\ell \textsf {T} \). Finally, we demonstrate the usefulness of \(\textsf {d}\ell \textsf {T} \) for analyzing the complexity of cryptographic reductions by providing an upper bound for the constructed adversary of the Goldreich–Levin theorem.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Notes
The original CEK machine comes from [16] and its name comes from the fact that its states have three components, a term, an environment and a continuation.
References
Accattoli, B., Dal Lago, U.: (Leftmost-outermost) beta reduction is invariant, indeed. Log. Methods Comput. Sci. 12(1) (2016)
Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: design and implementation of a cost and termination analyzer for Java bytecode. In: Formal Methods for Components and Objects, 6th International Symposium, FMCO 2007, pp. 113–132 (2007)
Baillot, P., Barthe, G., Dal Lago, U.: Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs. In: Proceedings of LPAR 2015, Volume 9450 of LNCS, pp. 203–218. Springer, Berlin (2015)
Baillot, P., Terui, K.: Light types for polynomial time computation in lambda calculus. Inf. Comput. 207(1), 41–62 (2009)
Barthe, G., Daubignard, M., Kapron, B., Lakhnech, Y.: Computational indistinguishability logic. In: Proceedings of Computer and Communications Security, CCS 2010, pp. 375–386. ACM, New York (2010)
Barthe, G., Fournet, C., Grégoire, B., Strub, P.-Y., Swamy, N., Zanella-Béguelin, S.: Probabilistic relational verification for cryptographic implementations. In: Proceedings of POPL 2014, pp. 193–206 (2014)
Barthe, G., Gaboardi, M., Gallego Arias, E. J., Hsu, J., Roth, A., Strub, P.-Y.: Higher-order approximate relational refinement types for mechanism design and differential privacy. In: Proceedings of POPL 2015, pp. 55–68. ACM (2015)
Barthe, G., Grégoire, B., Béguelin, S.Z.: Formal certification of code-based cryptographic proofs. In: Proceedings of POPL 2009, pp. 90–101 (2009)
Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Proceedings of CRYPTO 2011, pp. 71–90 (2011)
Bellare, M., Rogaway, P.: Random oracles are practical: a paradigm for designing efficient protocols. In: Proceedings of Computer and Communications Security, pp. 62–73 (1993)
Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy, pp. 140–154 (2006)
Dal Lago, U.: The geometry of linear higher-order recursion. ACM Trans. Comput. Log. 10(2), 8:1–8:38 (2009)
Dal Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. Log. Methods Comput. Sci. 8(4) (2011)
Dal Lago, U., Petit, B.: The geometry of types. In: Proceedings of POPL 2013, pp. 167–178 (2013)
Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Proceedings of POPL 2008, pp. 133–144 (2008)
Felleisen, M., Friedman, D.P.: Control operators, the SECD-machine, and the lambda-calculus. In: 3rd Working Conference on the Formal Description of Programming Concepts (1986)
Goldreich, O.: On expected probabilistic polynomial-time adversaries: a suggestion for restricted definitions and their benefits. In: Theory of Cryptography, pp. 174–193. Springer, Berlin (2007)
Grobauer, B.: Cost recurrences for DML programs. In: International Conference on Functional Programming (ICFP ’01), pp. 253–264 (2001)
Gulwani, S., Mehra, K.K., Chilimbi, T.M.: Speed: precise and efficient static estimation of program computational complexity. In: Proceedings of POPL 2009, pp. 127–139 (2009)
Halevi, S.: A plausible approach to computer-aided cryptographic proofs. IACR Cryptology ePrint Archive, p. 181 (2005)
Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Proceedings of ESOP 2010, pp. 287–306 (2010)
Hofmann, M.: Safe recursion with higher types and BCK-algebra. Ann. Pure Appl. Log. 104(1–3), 113–166 (2000)
Jones, N.D., Kristiansen, L.: A flow calculus of mwp-bounds for complexity analysis. ACM Trans. Comput. Log. 10(4), 28 (2009)
Katz, J., Lindell, Y.: Introduction to Modern Cryptography. Chapman & Hall Cryptography and Network Security Series. Chapman & Hall, London (2007)
Leivant, D., Marion, J.-Y.: Lambda calculus characterizations of poly-time. Fundam. Inform. 19(1/2), 167–184 (1993)
Lesourd, M.: Type inference for complexity analysis of functional programs (2016). Master Thesis, ENS Lyon. https://ilsordo.github.io/research/rapport2016.pdf
Petcher, A., Morrisett, G.: The foundational cryptography framework. In: Proceedings of POST 2015, Volume 9036 of LNCS, pp. 203–218 (2015)
Swamy, N., Chen, J., Fournet, C., Strub, P.-Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: Proceedings of ICFP 2011, pp. 266–278 (2011)
Xi, H.: Dependent types for program termination verification. Higher-Order Symb. Comput. 15(1), 91–131 (2002)
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Baillot, P., Barthe, G. & Dal Lago, U. Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. J Autom Reasoning 63, 813–855 (2019). https://doi.org/10.1007/s10817-019-09530-2
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-019-09530-2