Infinite State AMC-Model Checking for Cryptographic Protocols

to full text (526 kB)   ZIP
involved person(s) / institution(s)author :
datePublished :
  • February 2007
size56 S.

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.
Static URLhttps://www.uni-kiel.de/journals/receive/jportal_jparticle_00000117
 
URN:NBNurn:nbn:de:101:1-201205096891
IDNumber of report :
  • TR_0702