Deciding Properties of Contract-Signing Protocols
We show that for infinite transition systems induced by cryptographic protocols in the Rusinowitch/Turuani style with finite number of sessions, unbounded message size, and the Dolev-Yao intruder certain fundamental branching properties are decidable. As a consequence, we obtain that crucial properties of contract-signing protocols such as balance are decidable.
Preview
Rights
Use and reproduction:
No license. The provisions of the German Copyright Act (UrhG) apply.
Please note that individual components of the publication may be subject to other licensing or copyright conditions.
Cite
Citation style:
Could not load citation form.