A Probabilistic Logic for Concrete Security - Ecole Normale Supérieure paris-Saclay Accéder directement au contenu
Communication Dans Un Congrès Année : 2024

A Probabilistic Logic for Concrete Security

David Baelde
  • Fonction : Auteur
  • PersonId : 1135652
Caroline Fontaine
Adrien Koutsos
Guillaume Scerri
Théo Vignon
  • Fonction : Auteur
  • PersonId : 1383265

Résumé

The Squirrel Prover is a proof assistant designed for the computational verification of cryptographic protocols. It implements a probabilistic logic that captures cryptographic and probabilistic arguments used in security proofs. This logic operates in the asymptotic security setting, which limits the expressiveness of formulas and proofs. As a consequence, it can only prove security for finite interactions with a protocol, falling outside of the polynomial-level of security usually expected by cryptographers. We lift all these limitations by moving to a concrete security setting. We extend the logic with concrete security predicates, and design a corresponding proof system. We show the usefulness of these extensions on a case study, and through a novel proof-transformation result which shows that a large class of asymptotic logic security proofs can be automatically rewritten into concrete logic security proofs, improving security bounds exponentially.
Fichier principal
Vignette du fichier
main.pdf (672.15 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
licence : CC BY - Paternité

Dates et versions

hal-04577828 , version 1 (16-05-2024)

Identifiants

  • HAL Id : hal-04577828 , version 1

Citer

David Baelde, Caroline Fontaine, Adrien Koutsos, Guillaume Scerri, Théo Vignon. A Probabilistic Logic for Concrete Security. CSF 2024 - 37th IEEE Computer Security Foundations Symposium, Jul 2024, Enschede, Netherlands. ⟨hal-04577828⟩
0 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More