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. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Aizatulin, M., Schnoor, H., & Wilke, T. (2009). Computationally sound analysis of a probabilistic contract signing protocol. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5789 LNCS, pp. 571–586). https://doi.org/10.1007/978-3-642-04444-1_35
Mendeley helps you to discover research relevant for your work.