Formal Analysis of Fairness for Optimistic Multiparty Contract Signing Protocol
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...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2014-01-01
|
| Series: | Journal of Applied Mathematics |
| Online Access: | http://dx.doi.org/10.1155/2014/983204 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832555352866947072 |
|---|---|
| author | Xiaoru Li Xiaohong Li Guangquan Xu Jing Hu Zhiyong Feng |
| author_facet | Xiaoru Li Xiaohong Li Guangquan Xu Jing Hu Zhiyong Feng |
| author_sort | Xiaoru Li |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-b1e8079c69f34c82ab208f232a91a94f |
| institution | Kabale University |
| issn | 1110-757X 1687-0042 |
| language | English |
| publishDate | 2014-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Applied Mathematics |
| spelling | doaj-art-b1e8079c69f34c82ab208f232a91a94f2025-02-03T05:48:25ZengWileyJournal of Applied Mathematics1110-757X1687-00422014-01-01201410.1155/2014/983204983204Formal Analysis of Fairness for Optimistic Multiparty Contract Signing ProtocolXiaoru Li0Xiaohong Li1Guangquan Xu2Jing Hu3Zhiyong Feng4School of Computer Science and Technology, Tianjin University, Tianjin 300072, ChinaSchool of Computer Science and Technology, Tianjin University, Tianjin 300072, ChinaSchool of Computer Science and Technology, Tianjin University, Tianjin 300072, ChinaSchool of Computer Science and Technology, Tianjin University, Tianjin 300072, ChinaSchool of Computer Science and Technology, Tianjin University, Tianjin 300072, ChinaOptimistic 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.http://dx.doi.org/10.1155/2014/983204 |
| spellingShingle | Xiaoru Li Xiaohong Li Guangquan Xu Jing Hu Zhiyong Feng Formal Analysis of Fairness for Optimistic Multiparty Contract Signing Protocol Journal of Applied Mathematics |
| title | Formal Analysis of Fairness for Optimistic Multiparty Contract Signing Protocol |
| title_full | Formal Analysis of Fairness for Optimistic Multiparty Contract Signing Protocol |
| title_fullStr | Formal Analysis of Fairness for Optimistic Multiparty Contract Signing Protocol |
| title_full_unstemmed | Formal Analysis of Fairness for Optimistic Multiparty Contract Signing Protocol |
| title_short | Formal Analysis of Fairness for Optimistic Multiparty Contract Signing Protocol |
| title_sort | formal analysis of fairness for optimistic multiparty contract signing protocol |
| url | http://dx.doi.org/10.1155/2014/983204 |
| work_keys_str_mv | AT xiaoruli formalanalysisoffairnessforoptimisticmultipartycontractsigningprotocol AT xiaohongli formalanalysisoffairnessforoptimisticmultipartycontractsigningprotocol AT guangquanxu formalanalysisoffairnessforoptimisticmultipartycontractsigningprotocol AT jinghu formalanalysisoffairnessforoptimisticmultipartycontractsigningprotocol AT zhiyongfeng formalanalysisoffairnessforoptimisticmultipartycontractsigningprotocol |