| 引用本文: | 李任翔,蒋忠元,高胜,钱肖,沈秀轩,刘柄呈,陶梅悦,马建峰.智能合约法律化原则与转化验证模型.软件学报,2025,36(11):5296-5333 |
| |
|
| |
|
|
| 本文已被：浏览 967次 下载 1177次 |
码上扫一扫！ |
|
|
| 智能合约法律化原则与转化验证模型 |
|
李任翔1, 蒋忠元1, 高胜2, 钱肖1, 沈秀轩1, 刘柄呈1, 陶梅悦1, 马建峰1
|
|
1.西安电子科技大学 网络与信息安全学院, 陕西 西安 710071;2.中央财经大学 信息学院, 北京 102206
|
|
| 摘要: |
| 日常民事纠纷中合同类案件占比高, 数量多. 传统纸质合同存在的查阅困难、管理不便等问题, 已经严重影响了合同执行和纠纷处理的效率. 作为一种执行合同条款的计算机协议, 智能合约凭借其自动化执行, 去中心化和不可篡改的优势, 为法律合同的执行处理提供了新的可能. 但智能合约依赖于严格的编程逻辑, 缺乏法律解释的灵活性, 一旦部署后难以动态调整, 限制了合同参与方的意愿, 在法律适用性和约束力方面仍存在不确定性. 因此, 基于法律合同和智能合约的差异对比提出了文法要求、非赋权原则、有效性审查和安全性准则四大原则, 为具有法律效力的智能合约生成和执行提供了理论框架. 此外, 还设计了满足四大原则的智能合约转化与验证模型, 该模型能够对以过渡系统为表现形式的法律合同进行增强处理, 防止重入攻击, 并将基础和额外增加的规范转换为计算树逻辑验证安全属性, 通过验证的合同可以自动转化为智能合约. 在整体流程中, 模型始终遵循四大原则, 因此转化后的智能合约符合现行法律要求, 可被视为法律合同. 在实验验证部分, 采用一个简化的买卖合同作为案例, 展示其初始、增强过渡系统模型, 部分验证属性结果和最终生成的Solidity智能合约代码, 并在前置处理中通过采集64616篇合同数据共构建包含270592条样本的高质量数据集, 同时在一致性判定实验中验证了模型性能, R@1、R@5、R@10分别达到90.27%、97.91%和99.30%, 证明了模型的准确性和可靠性. 结论表明, 提出的四大原则可行性强, 转化验证模型能够解决纸质合同处理的繁琐问题, 提升法律合同执行和管理的便捷性和灵活性, 同时帮助智能合约获得法律保障, 有效规避潜在风险. |
| 关键词: 法律合同 智能合约 法律化 过渡系统 属性验证 |
| DOI：10.13328/j.cnki.jos.007386 |
| 分类号:TP309 |
| 基金项目:国家重点研发计划(2022YFB2701800) |
|
| Legalization Principles and Transformation Verification Model of Smart Contracts |
|
LI Ren-Xiang1, JIANG Zhong-Yuan1, GAO Sheng2, QIAN Xiao1, SHEN Xiu-Xuan1, LIU Bing-Cheng1, TAO Mei-Yue1, MA Jian-Feng1
|
|
1.School of Cyber Engineering, Xidian University, Xi’an 710071, China;2.School of Information, Central University of Finance and Economics, Beijing 102206, China
|
| Abstract: |
| Contract cases account for a substantial proportion of daily civil disputes, reflecting a considerable volume. The limited accessibility and cumbersome management of traditional paper contracts have significantly hindered the efficiency of contract execution and dispute resolution. As a computer protocol designed to execute contract terms, smart contracts offer new possibilities for the execution and processing of legal contracts, with advantages such as automated execution, decentralization, and immutability. However, their reliance on strict programming logic, lack of interpretative flexibility, and difficulty in dynamic adjustments after deployment constrain the intentions of contract participants and result in uncertainties regarding legal applicability and binding force. Based on the distinctions between legal contracts and smart contracts, this study proposes four key principles, including grammatical requirements, the non-empowerment principle, validity review, and security criteria, providing a theoretical framework for generating and executing legally effective smart contracts. A smart contract transformation and verification model is further designed to adhere to these four principles. The proposed model enhances the processing of legal contracts expressed as transition systems, prevents re-entry attacks, and converts core and additional specifications into computational tree logic for security property verification. Contract passing verification is automatically converted into smart contracts. The entire transformation process complies with the proposed four principles, ensuring that the resulting smart contracts meet current legal standards and can be regarded as legal contracts. Experimental validation includes a simplified sales contract as a case study, demonstrating its initial and enhanced transition system models, partial verification results, and the representative Solidity code generated. The pre-processing operation yields a high-quality dataset constructed from 270592 samples. Consistency evaluation between contract terms and legal provisions achieves Recall rates of 90.27% at R@1, 97.91% at R@5, and 99.30% at R@10. The feature extraction model, aided by a format conversion tool with nearly 100% fidelity, achieves 91.87% accuracy at the token level, confirming the model’s accuracy and reliability. The findings indicate that the proposed principles are highly feasible, while the transformation and verification model effectively addresses the cumbersome nature of paper contract processing, enhances the convenience and flexibility of legal contract execution and management, and enables smart contracts to obtain legal protection while mitigating potential risks. |
| Key words: legal contract smart contract legalization transition system property verification |
|
|
|
|
