Deciding Properties of Contract-Signing Protocols

Abstract. 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.

• Type: Conference
• Year: 2005
• Where: STACS
• Authors: Detlef Kähler, Ralf Küsters, Thomas Wilke
• Keywords: Cryptographic Protocols, Fundamental Branching Properties, Infinite Transition Systems, STACS 2005, Theoretical Computer Science