Name
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1109/LICS.2007.26 | Wroclaw |
Keywords | Field | DocType |
cryptographic protocols,game theory,Dolev-Yao intruder,contract-signing protocols,cryptographic protocols,game-theoretic security properties,infinite state AMC-model checking | Authentication,Telecommunications network,Model checking,Cryptographic protocol,Computer science,Theoretical computer science,Decidability,Cryptographic primitive,Error detection and correction,Game theory | Conference |
ISSN | ISBN | Citations |
1043-6871 | 0-7695-2908-9 | 10 |
PageRank | References | Authors |
0.56 | 19 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Detlef Kahler | 1 | 10 | 0.56 |
| Ralf Küsters | 2 | 1014 | 69.62 |
| Tomasz Truderung | 3 | 439 | 17.37 |