nach oben

Journal of Automated Reasoning

Erschienen in:

31.07.2019

Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs

verfasst von: Patrick Baillot, Gilles Barthe, Ugo Dal Lago

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Preface to the Special Issue on Linearity

Nächster Artikel A Proof Theory for Model Checking

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

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.

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)CrossRef

Baillot, P., Terui, K.: Light types for polynomial time computation in lambda calculus. Inf. Comput. 207(1), 41–62 (2009)MathSciNetCrossRef

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)CrossRef

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)CrossRef

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)CrossRef

10.

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)

11.

Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy, pp. 140–154 (2006)

12.

Dal Lago, U.: The geometry of linear higher-order recursion. ACM Trans. Comput. Log. 10(2), 8:1–8:38 (2009)MathSciNetCrossRef

13.

Dal Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. Log. Methods Comput. Sci. 8(4) (2011)

14.

Dal Lago, U., Petit, B.: The geometry of types. In: Proceedings of POPL 2013, pp. 167–178 (2013)CrossRef

15.

Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Proceedings of POPL 2008, pp. 133–144 (2008)MathSciNetCrossRef

16.

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)

17.

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)

18.

Grobauer, B.: Cost recurrences for DML programs. In: International Conference on Functional Programming (ICFP ’01), pp. 253–264 (2001)

19.

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)CrossRef

20.

Halevi, S.: A plausible approach to computer-aided cryptographic proofs. IACR Cryptology ePrint Archive, p. 181 (2005)

21.

Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Proceedings of ESOP 2010, pp. 287–306 (2010)CrossRef

22.

Hofmann, M.: Safe recursion with higher types and BCK-algebra. Ann. Pure Appl. Log. 104(1–3), 113–166 (2000)MathSciNetCrossRef

23.

Jones, N.D., Kristiansen, L.: A flow calculus of mwp-bounds for complexity analysis. ACM Trans. Comput. Log. 10(4), 28 (2009)MathSciNetCrossRef

24.

Katz, J., Lindell, Y.: Introduction to Modern Cryptography. Chapman & Hall Cryptography and Network Security Series. Chapman & Hall, London (2007)CrossRef

25.

Leivant, D., Marion, J.-Y.: Lambda calculus characterizations of poly-time. Fundam. Inform. 19(1/2), 167–184 (1993)MathSciNetMATH

26.

Lesourd, M.: Type inference for complexity analysis of functional programs (2016). Master Thesis, ENS Lyon. https://ilsordo.github.io/research/rapport2016.pdf

27.

Petcher, A., Morrisett, G.: The foundational cryptography framework. In: Proceedings of POST 2015, Volume 9036 of LNCS, pp. 203–218 (2015)

28.

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)

29.

Xi, H.: Dependent types for program termination verification. Higher-Order Symb. Comput. 15(1), 91–131 (2002)MathSciNetCrossRef

Titel: Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
verfasst von: Patrick Baillot
Gilles Barthe
Ugo Dal Lago
Publikationsdatum: 31.07.2019
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 4/2019
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-019-09530-2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2019

Selected Extended Papers of NFM 2017: Preface

Explaining AI Decisions Using Efficient Methods for Learning Sparse Boolean Formulae

Preface to the Special Issue on Linearity

QPCF: Higher-Order Languages and Quantum Circuits

Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics

Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants