Abstract
We define a call-by-value variant of Gödel’s System \(\mathsf {T} \) with references, and equip it with a linear dependent type and effect system, called \(\mathsf {d}\ell \mathsf {T} \), that can estimate the 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 \(\mathsf {d}\ell \mathsf {T} \). Finally, we demonstrate the usefulness of \(\mathsf {d}\ell \mathsf {T} \) for analyzing the complexity of cryptographic reductions by providing an upper bound for the constructed adversary of the Goldreich-Levin theorem.
This work has been partially supported by ANR Project ELICA ANR-14-CE25-0005.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: design and implementation of a cost and termination analyzer for java bytecode. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 113–132. Springer, Heidelberg (2008)
Baillot, P., Barthe, G., Dal Lago, U.: Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs (long version). Technical report, september 2015, HAL archive. http://hal.archives-ouvertes.fr/hal-01197456
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: Computer and Communications Securitym, CCS 2010, pp. 375–386. ACM, New York (2010)
Barthe, G., Grégoire, B., Béguelin, S.Z.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90–101 (2009)
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)
Bellare, M., Rogaway, P.: Random oracles are practical: a paradigm for designing efficient protocols. In: 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. Logical Methods Comput. Sci. 8(4), 133–142 (2011)
Dal Lago, U., Petit, B.: The geometry of types. In: POPL, pp. 167–178 (2013)
Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: POPL, pp. 133–144 (2008)
Goldreich, O.: On expected probabilistic polynomial-time adversaries: a suggestion for restricted definitions and their benefits. In: Vadhan, S.P. (ed.) TCC 2007. LNCS, vol. 4392, pp. 174–193. Springer, Heidelberg (2007)
Grobauer, B.: Cost recurrences for DML programs. In: International Conference on Functional Programming (ICFP 2001), pp. 253–264 (2001)
Gulwani, S., Mehra, K.K., Chilimbi, T.M.: Speed: precise and efficient static estimation of program computational complexity. In: POPL, pp. 127–139 (2009)
Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 287–306. Springer, Heidelberg (2010)
Hofmann, M.: Safe recursion with higher types and BCK-algebra. Ann. Pure Appl. Logic 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:1–28:41 (2009)
Katz, J., Lindell, Y.: Introduction to Modern Cryptography. Chapman & Hall Cryptography and Network Security Series. Chapman & Hall, New York (2007)
Leivant, D., Marion, J.: Lambda calculus characterizations of poly-time. Fundam. Inform. 19(1/2), 167–184 (1993)
Petcher, A., Morrisett, G.: The foundational cryptography framework (2015). to appear
Xi, H.: Dependent types for program termination verification. High. Order Symb. Comput. 15(1), 91–131 (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baillot, P., Barthe, G., Lago, U.D. (2015). Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2015. Lecture Notes in Computer Science(), vol 9450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48899-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-662-48899-7_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-48898-0
Online ISBN: 978-3-662-48899-7
eBook Packages: Computer ScienceComputer Science (R0)