User Tools

Site Tools


Deciding Properties of Contract-Signing Protocols

Detlef Kähler, Ralf Küsters, and Thomas Wilke

We show that for infinite transition systems induced by cryptographic protocols in the Rusinowitch/Turuani style certain fundamental branching properties are decidable. As a consequence, we obtain that crucial properties of contract-signing protocols such as balance are decidable.