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.

Vorschau

Logo BII

BII

Rechte

Nutzung und Vervielfältigung:

Keine Lizenz. Es gelten die Bestimmungen des deutschen Urheberrechts (UrhG).

Bitte beachten Sie, dass einzelne Bestandteile der Publikation anderweitigen Lizenz- bzw. urheberrechtlichen Bedingungen unterliegen können.

Zitieren

Zitierform:
Zitierform konnte nicht geladen werden.