Date Added: Jun 2012
In design and verification of cryptographic protocols, symbolic techniques [DY83] have proven very successful. A breakthrough result in this area is that secrecy properties of protocols can be decided in coNP, even if the adversary is allowed to send arbitrarily complex terms. The authors propose a new, widely applicable model for analyzing knowledge-based (epistemic) and strategic properties of cryptographic protocols. They prove that the corresponding model checking problem with respect to an expressive epistemic strategic logic is decidable. As corollaries, they obtain decidability of complex security properties including coercion-resistance of voting protocols, accountability of protocols using a Trusted Third Party, and abuse-freeness of contract signing protocols.