Description
We present a novel, simple technique for proving secrecy properties for security protocols that manipulate lists of unbounded length, for an unbounded number of sessions.<br/> More specifically, our technique relies on the Horn clause approach used in the automatic verifier ProVerif: we show that if a protocol is proven secure by our technique with lists of length one, then it is secure for lists of unbounded length.<br/> Interestingly, this theorem relies on approximations made by our verification technique: in general, secrecy for lists of length one does not imply secrecy for lists of unbounded length.<br/> Our result can be used in particular to prove secrecy properties for group protocols with an unbounded number of participants and for some XML protocols (web services) with ProVerif.
Prochains exposés
-
Encryption homomorphe sans bruit à l'aide de groupes
Orateur : Pierre Guillot - Ravel Technologies (dispo Université de Strasbourg, IRMA)
Je vais rappeler les travaux de Nuida et Ostrovski sur l'utilisation des groupes pour l'élaboration de schémas cryptographiques homomorphes. Je vais présenter nos travaux qui fournissent des encodages à la fois plus efficaces et plus généraux, et qui déterminent exactement quels groupes peuvent être utilisés. Puis je vais discuter GRAFHEN, un protocole qui utilise ces idées. Je dirai juste[…]-
Cryptography
-