Conception de protocoles de sécurité et analyse symbolique : protocoles hybrides, Modèles d'adversaires dérivés et Théories équationnelles affinées

Abstract

The security proof of a protocol, though formally rigorous within a given model, is entirely contingent on the model's assumptions. If the adversary's capabilities are underspecified, the cryptographic primitives are idealized, or the security properties are incompletely formalized, the proof may not hold in practice.The first contribution advances prior work on refining symbolic models for crypto- graphic primitives to better capture their behaviors. Specifically, we propose more precise equational theories for the ElGamal cryptosystem, DSA signatures, and Zero-Knowledge Proofs. Standard symbolic modeling of these primitives disregards their algebraic prop- erties, which may lead to missed attacks in larger protocols. Additionally, we introduce a formal model of exponentiation and re-encryption Mix-Networks. By combining these models with our equational theories, we can automatically find attacks based on the incorrect use of the Mix-Networks missed by previous symbolic models.The second contribution involves analyzing the WireGuard protocol. We examine the protocol's claimed security properties under an adversary capable of compromising any possible key combinations. To systematize this analysis, we introduce the concepts of minimal defensive model and minimal offensive adversary model. The defensive models ensures that violating a security property requires possessing specific atomic capabilities. Minimal offensive models define the smallest sets of adversarial capabilities that break security. Theses derivations helped to identify an implementation optimization that introduces new attack vectors.The third contribution presents a hybrid protocol combining WireGuard and Post- Quantum WireGuard, aligning with recommendations for a secure transition to post- quantum cryptography. Although a symbolic analysis of PQ-WireGuard existed, we uncover discrepancies between the model and the protocol's specifications, including pre- viously missed Unknown Key-Share attacks. We propose fixes and ensure the hybrid protocol's security relies on both the corrected post-quantum and classical WireGuard protocols. We formally defined a hybrid protocol's security as when there exists both minimal defensive models dependent on post-quantum keys and defensive models depen- dent on classical keys. Our work underscores the importance of iterative analysis during design, as achieving hybrid security required repeated refinement between modeling and verification.