Bruno Blanchet and Paiola Miriam, Automatic Verification of Protocols with Lists of Unbounded Length, the ACM Conference on Computer and Communications Security, CCS'13, To appear.

Get the paper

Long version with proofs available: .pdf, 441.1Kb


ProVerif scripts:

The automatic verifier ProVerifList and examples are available here, under the CeCILL license (French license compatible with GPL).


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.


  AUTHOR = {Bruno Blanchet and Miriam Paiola},
  TITLE = {Automatic Verification of  Protocols with Lists of Unbounded Length},
  BOOKTITLE = {Proceedings of the 2013 ACM conference on 
	Computer and communications security},
  SERIES={CCS '13},
  YEAR = 2013,
  PAGES = {},
  LOCATION = {Berlin, Germany},
  EDITOR = {},
  VOLUME = ,  
  NOTE = {To appear.}