User Tools

Site Tools


Infinite State AMC-Model Checking for Cryptographic Protocols (BibTeX)

@TECHREPORT{KaehlerKuestersTruderung-IFI-TR-0702-2007,
  author = {Detlef K{\"a}hler and Ralf K{\"u}sters and Tomasz Truderung},
  title = {{Infinite State AMC-Model Checking for Cryptographic Protocols}},
  institution = {Institut f{\"u}r Informatik, CAU Kiel, Germany},
  year = 2007,
  number = 0702,
  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.}
}