Paper: Infinite State AMC-Model Checking for Cryptographic Protocols (at LICS 2007)

Authors: Detlef Kähler Ralf Küsters Tomasz Truderung

Abstract

Only very little is known about the automatic analysis of cryptographic protocols for game-theoretic security properties. In this paper, we therefore study decidability and complexity of the model checking problem for AMC-formulas over infinite state concurrent game structures induced by cryptographic protocols and the Dolev-Yao intruder. We show that the problem is NEXPTIME-complete when making reasonable assumptions about protocols and for an expressive fragment of AMC, which contains, for example, all properties formulated by Kremer and Raskin in fair ATL for contract-signing and non-repudiation protocols. We also prove that our assumptions on protocols are necessary to obtain decidability, unless other restrictions are imposed on protocols.

BibTeX

  @InProceedings{KhlerKustersKstersT-InfiniteStateAMCMod,
    author = 	 {Detlef Kähler and Ralf Küsters and Tomasz Truderung},
    title = 	 {Infinite State AMC-Model Checking for Cryptographic Protocols},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {181--190},
    location =   {Wroclaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }