PaiolaBlanchetJCS13
Bruno Blanchet
Back to publications
Miriam Paiola and Bruno Blanchet.
Verification of Security Protocols with Lists: from Length
One to Unbounded Length.
Journal of Computer Security, 21(6):781-816, December 2013.
Special issue POST'12.
Get the paper
.pdf, 244 Kb
Abstract
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.
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.
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.
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.
Bibtex
@ARTICLE{PaiolaBlanchetJCS13,
AUTHOR = {Miriam Paiola and Bruno Blanchet},
TITLE = {Verification of Security Protocols with Lists:
from Length One to Unbounded Length},
JOURNAL = {Journal of Computer Security},
YEAR = 2013,
VOLUME = 21,
NUMBER = 6,
PAGES = {781--816},
MONTH = DEC,
NOTE = {Special issue POST'12}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)