基于角色的区块链拍卖合约抽象建模及其时间安全性与公平性验证  

Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness

作　　者：王昌晶[1] 欧阳俊媛 张取发 左正康[1] 程着 卢家兴[1] WANG Changjing;OUYANG Junyuan;ZHANG Qufa;ZUO Zhengkang;CHENG Zhuo;LU Jiaxing(School of Computer and Information Engineering,Jiangxi Normal University,Nanchang 330022,China;School of Software,East China University of Technology,Nanchang 330013,China;National-level International Science and Technology Cooperation Base of Networked Supporting Software,Jiangxi Normal University,Nanchang 330022,China)

机构地区：[1]江西师范大学计算机信息工程学院,江西南昌330022 [2]东华理工大学软件学院,江西南昌330013 [3]江西师范大学国家网络化支撑软件国际合作基地,江西南昌330022

出　　处：《通信学报》2024年第10期225-242,共18页Journal on Communications

基　　金：国家自然科学基金资助项目(No.62462037,No.62462036);江西省主要学科学术与技术带头人培养基金资助项目(No.20232BCJ22013);江西省自然科学基金资助项目(No.20242BAB26017);江西省教育厅科技基金资助项目(No.GJJ2200303,No.GJJ210340)。

摘　　要：为提升拍卖合约时间安全性验证效率及验证公平性,提出基于角色的拍卖合约抽象建模及其验证方法。首先,对合约源代码进行基于账户角色的抽象建模,转换为时间自动机网络模型,并对时间安全性进行形式化描述,用UPPAAL工具验证。其次,提取合约源代码机制,建立智能合约机制模型,同样转换为时间自动机网络模型,并对4种公平性进行形式化描述,再用UPPAAL验证。最后,通过2个经典案例证明了所提方法的可行性和有效性。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.

关 键 词：拍卖合约 时间安全性 公平性 时间自动机 UPPAAL 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]