Mechanized Proofs of Adversarial Complexity and Application to Universal Composability: Journal pre-print: full version
| Autor: | Pierre-Yves Strub, Gilles Barthe, Adrien Koutsos, Benjamin Grégoire, Manuel Barbosa |
|---|---|
| Přispěvatelé: | Faculdade de Ciências da Universidade do Porto (FCUP), Universidade do Porto = University of Porto, Institute for Systems and Computer Engineering, Technology and Science [Porto] (INESC TEC), Max Planck Institute for Security and Privacy [Bochum] (MPI Security and Privacy), Institute IMDEA Software [Madrid], Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Programming securely with cryptography (PROSECCO), Inria de Paris, École polytechnique (X), Universidade do Porto, Programming securely with cryptography (PROSECCO ), CRACS & Inesc TEC [Porto], Meta France, ANR-17-CE39-0004,TECAP,Analyse de protocoles - unir les outils existants(2017), ANR-22-PECY-0006,SVP,Verification of Security Protocols(2022) |
| Rok vydání: | 2023 |
| Předmět: |
Interactive Proof System
Theoretical computer science General Computer Science Computer science Cryptography Verification of Cryptographic Primitives 0102 computer and information sciences 02 engineering and technology Hoare logic Mathematical proof 01 natural sciences Formal Methods [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Universal composability 0202 electrical engineering electronic engineering information engineering Complexity class [INFO]Computer Science [cs] Concrete security Safety Risk Reliability and Quality business.industry Proof assistant Interactive proof system 020207 software engineering Complexity Analysis 010201 computation theory & mathematics business |
| Zdroj: | CCS 2021-ACM SIGSAC Conference on Computer and Communications Security CCS 2021-ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2541-2563, ⟨10.1145/3460120.3484548⟩ CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2541-2563, ⟨10.1145/3460120.3484548⟩ CCS |
| ISSN: | 2471-2574 2471-2566 |
| DOI: | 10.1145/3589962 |
| Popis: | International audience; 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). |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|