A Formalization of Polytime Functions

DOI10.1007/978-3-642-22863-6_11zbMath1342.68286OpenAlexW2952595174MaRDI QIDQ3088001

Sylvain Heraud, David E. Nowak

Publication date: 17 August 2011

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22863-6_11

zbMATH Keywords

cryptographyimplicit computational complexity

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Cryptography (94A60)

Related Items (1)

Formal security proofs with minimal fuss: implicit computational complexity at work

Uses Software

• Coq

Cites Work

• Unnamed Item
• A new recursion-theoretic characterization of the polytime functions
• Safe recursion with higher types and BCK-algebra
• A new function algebra of EXPTIME functions by safe nested recursion
• The computational SLR: a logic for reasoning about computational indistinguishability
• The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs
• New directions in cryptography
• A Calculus for Game-Based Security Proofs
• Formal certification of code-based cryptographic proofs
• Computer Science Logic
• Complexity Analysis by Rewriting
• Theorem Proving in Higher Order Logics
• A Formal Language for Cryptographic Pseudocode

This page was built for publication: A Formalization of Polytime Functions