BlanchetPaiolaCCS13
Bruno Blanchet
Back to publications
Bruno Blanchet and Miriam Paiola.
Automatic Verification of Protocols with Lists of Unbounded
Length.
In ACM Conference on Computer and Communications Security
(CCS'13), pages 573-584, Berlin, Germany, November 2013. ACM.
Get the paper
.pdf, 365 Kb
Links
Official ACM version (you can download the full text from there):
Long version of the paper, with proofs
Prototype implementation and examples under the CeCILL license (French license compatible with GPL)
Abstract
We present a novel automatic technique for proving secrecy and authentication properties for
security protocols that manipulate lists of unbounded length, for
an unbounded number of sessions. This result is achieved by extending the Horn clause approach of the automatic protocol verifier ProVerif. We extend the Horn clauses to be able to represent lists of unbounded length. We adapt the resolution algorithm to handle the new class of Horn clauses, and prove the soundness of this new algorithm.
We have implemented our algorithm and successfully tested it on several protocol examples, including XML protocols coming from web services.
Bibtex
@INPROCEEDINGS{BlanchetPaiolaCCS13,
AUTHOR = {Bruno Blanchet and Miriam Paiola},
TITLE = {Automatic Verification of Protocols with Lists of Unbounded Length},
BOOKTITLE = {ACM Conference on Computer and Communications Security (CCS'13)},
PAGES = {573--584},
YEAR = 2013,
ADDRESS = {Berlin, Germany},
MONTH = NOV,
PUBLISHER = {ACM}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)