Description
CryptoVerif is a security protocol verifier sound in the computational model of cryptography. It produces proofs by sequences of games, like those done manually by cryptographers. It has an automatic proof strategy and can also be guided by the user. It provides a generic method for specifying security assumptions on many cryptographic primitives, and can prove secrecy, authentication, and indistinguishability properties. A successful proof guarantees asymptotic security, in the presence of polynomial-time adversaries, and also provides an exact security bound of the probability of success of an attack as a function of the probability of breaking the primitives.
After a general introduction to CryptoVerif, we will focus on recent extensions introduced for dealing with key compromise. We will also briefly mention a few other recent results: post-quantum CryptoVerif, CV2EC, CV2F*.
Infos pratiques
Prochains exposés
-
Endomorphisms via Splittings
Orateur : Min-Yi Shen - No Affiliation
One of the fundamental hardness assumptions underlying isogeny-based cryptography is the problem of finding a non-trivial endomorphism of a given supersingular elliptic curve. In this talk, we show that the problem is related to the problem of finding a splitting of a principally polarised superspecial abelian surface. In particular, we provide formal security reductions and a proof-of-concept[…]-
Cryptography
-