Paper 2021/156

Mechanized Proofs of Adversarial Complexity and Application to Universal Composability

Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, and Pierre-Yves Strub

Abstract

EasyCrypt is a proof assistant used for verifying computational security proofs of cryptographic constructions. It has been applied to several prominent examples, including the SHA3 standard and a critical component of AWS Key Management Services. In this paper we enhance the EasyCrypt proof assistant to reason about computational complexity of adversaries. The key technical tool is a Hoare logic for reasoning about computational complexity (execution time and oracle calls) of adversarial computations. Our Hoare logic is built on top of the module system used by EasyCrypt for modeling adversaries. We prove that our logic is sound w.r.t. the semantics of EasyCrypt programs --- we also provide full semantics for the EasyCrypt module system, which was previously lacking. We showcase (for the first time in EasyCrypt and in other computer-aided cryptographic tools) how our approach can express precise relationships between the probability of adversarial success and their execution time. In particular, we can quantify existentially over adversaries in a complexity class, and express general composition statements in simulation-based frameworks. Moreover, such statements can be composed to derive standard concrete security bounds for cryptographic constructions whose security is proved in a modular way. As a main benefit of our approach, we revisit security proofs of some well-known cryptographic constructions and we present a new formalization of Universal Composability (UC).

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. Major revision. ACM CCS'21
Keywords
Verification of Cryptographic PrimitivesFormal MethodsInteractive Proof SystemComplexity Analysis
Contact author(s)
adrien koutsos @ inria fr
gjbarthe @ gmail com
mbb @ fc up pt
benjamin gregoire @ inria fr
pierre-yves @ strub nu
History
2021-09-07: revised
2021-02-17: received
See all versions
Short URL
https://ia.cr/2021/156
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2021/156,
      author = {Manuel Barbosa and Gilles Barthe and Benjamin Grégoire and Adrien Koutsos and Pierre-Yves Strub},
      title = {Mechanized Proofs of Adversarial Complexity and Application to Universal Composability},
      howpublished = {Cryptology ePrint Archive, Paper 2021/156},
      year = {2021},
      note = {\url{https://eprint.iacr.org/2021/156}},
      url = {https://eprint.iacr.org/2021/156}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.