Formal analysis of fairness for optimistic multiparty contract signing protocol
Summary: Optimistic multiparty contract signing (OMPCS) protocols are proposed for exchanging multiparty digital signatures in a contract. Compared with general two-party exchanging protocols, such protocols are more complicated, because the number of protocol messages and states increases considerably when signatories increase. Moreover, fairness property in such protocols requires protection from each signatory rather than from an external hostile agent. It thus presents a challenge for formal verification. In our analysis, we employ and combine the strength of extended modeling language CSP\(\#\) and linear temporal logic (LTL) to verify the fairness of OMPCS protocols. Furthermore, for solving or mitigating the state space explosion problem, we set a state reduction algorithm which can decrease the redundant states properly and reduce the time and space complexity greatly. Finally, this paper illustrates the feasibility of our approach by analyzing the GM and CKS protocols, and several fairness flaws have been found in certain computation times.
- Finite-state analysis of two contract signing protocols
- Fair multi-party contract signing using private contract signatures
- Deciding strategy properties of contract-signing protocols
- scientific article; zbMATH DE number 2044546 (Why is no real title available?)
- scientific article; zbMATH DE number 1759355 (Why is no real title available?)
- Compositional analysis of contract-signing protocols
- Formal analysis of multiparty contract signing
This page was built for publication: Formal analysis of fairness for optimistic multiparty contract signing protocol
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2336896)
