Skip to Main content Skip to Navigation

Verification of cryptographic protocols with lists of unbounded lengths

Abstract : In this thesis, we propose two different techniques for verifying security protocols that manipulate lists of unbounded length. In the first part of the thesis, we present a simple technique for proving secrecy properties for protocols that manipulate list elements in a uniform way, for an unbounded number of sessions. More specifically, this 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. The second technique presented in this thesis automatically proves secrecy and authentication properties for security protocols that manipulate different list elements in different ways. 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. Finally, we present an extension of the input language of ProVerif, a variant of the applied pi calculus, to model protocols with lists of unbounded length, give its formal semantics, and translate it automatically to Horn clauses.
Document type :
Complete list of metadata
Contributor : Bruno Blanchet Connect in order to contact the contributor
Submitted on : Wednesday, January 14, 2015 - 9:44:56 AM
Last modification on : Tuesday, January 11, 2022 - 11:16:26 AM
Long-term archiving on: : Friday, September 11, 2015 - 6:42:58 AM


  • HAL Id : tel-01103104, version 1


Miriam Paiola. Verification of cryptographic protocols with lists of unbounded lengths. Cryptography and Security [cs.CR]. Université Paris-Diderot (Paris 7), 2014. English. ⟨tel-01103104v1⟩



Record views


Files downloads