Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness
To enhance the efficiency of time security verification and fairness verification of auction contracts, an abstract modeling and verification method for role-based auction contracts was proposed. Firstly, the source code of the contract was abstractly modeled based on account roles and converted int...
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | zho |
| Published: |
Editorial Department of Journal on Communications
2024-10-01
|
| Series: | Tongxin xuebao |
| Subjects: | |
| Online Access: | http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2024074/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1841537129672343552 |
|---|---|
| author | WANG Changjing OUYANG Junyuan ZHANG Qufa ZUO Zhengkang CHENG Zhuo LU Jiaxing |
| author_facet | WANG Changjing OUYANG Junyuan ZHANG Qufa ZUO Zhengkang CHENG Zhuo LU Jiaxing |
| author_sort | WANG Changjing |
| collection | DOAJ |
| description | To enhance the efficiency of time security verification and fairness verification of auction contracts, an abstract modeling and verification method for role-based auction contracts was proposed. Firstly, the source code of the contract was abstractly modeled based on account roles and converted into a timed automaton network model. Formal descriptions of time security were provided and verified using the UPPAAL tool. Secondly, the mechanisms in the source code of the contract were extracted to establish a smart contract mechanism model, which was also converted into a timed automaton network model. Formal descriptions of four types of fairness were provided and verified using UPPAAL. Finally, the feasibility and effectiveness of the proposed method were demonstrated through two classic cases. |
| format | Article |
| id | doaj-art-e5330e5a3ce94cb3af8e38285230a62d |
| institution | Kabale University |
| issn | 1000-436X |
| language | zho |
| publishDate | 2024-10-01 |
| publisher | Editorial Department of Journal on Communications |
| record_format | Article |
| series | Tongxin xuebao |
| spelling | doaj-art-e5330e5a3ce94cb3af8e38285230a62d2025-01-14T08:46:01ZzhoEditorial Department of Journal on CommunicationsTongxin xuebao1000-436X2024-10-014522524277077528Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairnessWANG ChangjingOUYANG JunyuanZHANG QufaZUO ZhengkangCHENG ZhuoLU JiaxingTo enhance the efficiency of time security verification and fairness verification of auction contracts, an abstract modeling and verification method for role-based auction contracts was proposed. Firstly, the source code of the contract was abstractly modeled based on account roles and converted into a timed automaton network model. Formal descriptions of time security were provided and verified using the UPPAAL tool. Secondly, the mechanisms in the source code of the contract were extracted to establish a smart contract mechanism model, which was also converted into a timed automaton network model. Formal descriptions of four types of fairness were provided and verified using UPPAAL. Finally, the feasibility and effectiveness of the proposed method were demonstrated through two classic cases.http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2024074/auction contractstemporal securityfairnesstime automataUPPAAL |
| spellingShingle | WANG Changjing OUYANG Junyuan ZHANG Qufa ZUO Zhengkang CHENG Zhuo LU Jiaxing Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness Tongxin xuebao auction contracts temporal security fairness time automata UPPAAL |
| title | Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness |
| title_full | Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness |
| title_fullStr | Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness |
| title_full_unstemmed | Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness |
| title_short | Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness |
| title_sort | role based abstract modeling of blockchain auction contracts and verification of temporal security and fairness |
| topic | auction contracts temporal security fairness time automata UPPAAL |
| url | http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2024074/ |
| work_keys_str_mv | AT wangchangjing rolebasedabstractmodelingofblockchainauctioncontractsandverificationoftemporalsecurityandfairness AT ouyangjunyuan rolebasedabstractmodelingofblockchainauctioncontractsandverificationoftemporalsecurityandfairness AT zhangqufa rolebasedabstractmodelingofblockchainauctioncontractsandverificationoftemporalsecurityandfairness AT zuozhengkang rolebasedabstractmodelingofblockchainauctioncontractsandverificationoftemporalsecurityandfairness AT chengzhuo rolebasedabstractmodelingofblockchainauctioncontractsandverificationoftemporalsecurityandfairness AT lujiaxing rolebasedabstractmodelingofblockchainauctioncontractsandverificationoftemporalsecurityandfairness |