Description
Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs. However, the guarantees that it offers have been quite unclear.<br/> We present two results that show soundness of formal models with respect to computational notions of security.<br/> First, we establish that symbolic integrity and secrecy proofs are sound with respect to the computational model in the case of protocols that use signatures and asymmetric encryption. This is a join work with Bogdan Warinschi. Secondly, we study the link between formal and cryptographic models for security protocols in the presence of a passive adversary, for abitrary equational theories. We define a framework for comparing a cryptographic implementation and its idealization w.r.t. various security notions. In particular, we concentrate on the computationnal soundness of static equivalence, a standard tool in cryptographic $\pi$-calculi. This is a join work with Mathieu Baudet and Steve Kremer.
Prochains exposés
-
Post-Quantum Public-Key Pseudorandom Correlation Functions for OT
Orateur : Mahshid Riahinia - ENS, CNRS
Public-Key Pseudorandom Correlation Functions (PK-PCF) are an exciting recent primitive introduced to enable fast secure computation. Despite significant advances in the group-based setting, success in the post-quantum regime has been much more limited. In this talk, I will introduce an efficient lattice-based PK-PCF for the string OT correlation. At the heart of our result lie several technical[…] -
Predicting Module-Lattice Reduction
Orateur : Paola de Perthuis - CWI
Is module-lattice reduction better than unstructured lattice reduction? This question was highlighted as `Q8' in the Kyber NIST standardization submission (Avanzi et al., 2021), as potentially affecting the concrete security of Kyber and other module-lattice-based schemes. Foundational works on module-lattice reduction (Lee, Pellet-Mary, Stehlé, and Wallet, ASIACRYPT 2019; Mukherjee and Stephens[…]-
Cryptography
-