Computationally Sound Analysis of a Probabilistic Contract Signing Protocol

We propose a probabilistic contract signing protocol that achieves balance even in the presence of an adversary that may delay messages sent over secure channels. To show that this property holds in a computational setting, we first propose a probabilistic framework for protocol analysis, then prove that in a symbolic setting the protocol satisfies a probabilistic alternating-time temporal formula expressing balance, and finally establish a general result stating that the validity of formulas such as our balance formula is preserved when passing from the symbolic to a computational setting. The key idea of the protocol is to take a ``gradual commitment'' approach.

Logo BII

BII

Zitieren

Zitierform:
Zitierform konnte nicht geladen werden.

Rechte

Nutzung und Vervielfältigung:Keine Creative-Commons-Lizenz - Es gelten die Bestimmungen des dt. Urheberrechts (UrhG)Bitte beachten Sie, dass einzelne Bestandteile der Publikation anderweitigen Lizenz- bzw. urheberrechtlichen Bedingungen unterliegen können.