计算机工程与应用
計算機工程與應用
계산궤공정여응용
Computer Engineering and Applications
2015年
19期
32-36
,共5页
形式化验证%交替时态逻辑(ATL)%MOCHA工具%公平交换协议
形式化驗證%交替時態邏輯(ATL)%MOCHA工具%公平交換協議
형식화험증%교체시태라집(ATL)%MOCHA공구%공평교환협의
formal verification%Alternating-Time Temporal Logic(ATL)%MOCHA%fair exchange protocol
如何对电子商务协议进行分析与验证一直是研究的热点，基于ATL（交替时态逻辑）对电子商务协议中的公平交换协议（Fair Exchange Protocols）进行形式化分析与验证，并选取了其中的一个电子合同签署协议进行形式化验证。用ATL语言来形式化描述公平交换协议，并使用ATS（Alternating Transition Systems，交替转移系统）来为公平交换协议进行形式化建模，再用形式化验证工具MOCHA对公平交换协议的公平性（Fairness）、及时性（Timeli-ness）和不可滥用性（Abuse-Freeness）进行有效的验证；对验证结果进行分析与讨论，发现了该协议不满足公平性和不可滥用性，不符合设计的要求。
如何對電子商務協議進行分析與驗證一直是研究的熱點，基于ATL（交替時態邏輯）對電子商務協議中的公平交換協議（Fair Exchange Protocols）進行形式化分析與驗證，併選取瞭其中的一箇電子閤同籤署協議進行形式化驗證。用ATL語言來形式化描述公平交換協議，併使用ATS（Alternating Transition Systems，交替轉移繫統）來為公平交換協議進行形式化建模，再用形式化驗證工具MOCHA對公平交換協議的公平性（Fairness）、及時性（Timeli-ness）和不可濫用性（Abuse-Freeness）進行有效的驗證；對驗證結果進行分析與討論，髮現瞭該協議不滿足公平性和不可濫用性，不符閤設計的要求。
여하대전자상무협의진행분석여험증일직시연구적열점，기우ATL（교체시태라집）대전자상무협의중적공평교환협의（Fair Exchange Protocols）진행형식화분석여험증，병선취료기중적일개전자합동첨서협의진행형식화험증。용ATL어언래형식화묘술공평교환협의，병사용ATS（Alternating Transition Systems，교체전이계통）래위공평교환협의진행형식화건모，재용형식화험증공구MOCHA대공평교환협의적공평성（Fairness）、급시성（Timeli-ness）화불가람용성（Abuse-Freeness）진행유효적험증；대험증결과진행분석여토론，발현료해협의불만족공평성화불가람용성，불부합설계적요구。
How to analyze and verify the e-commerce protocols has been a hot research. This paper bases on ATL(Alter-nating-Time Temporal Logic)to formal analyze and verify the fair exchange protocol, and chooses a electronic contract signing protocol for formal verification. It describes the fair exchange protocol by using the ATL language, and formal model of the fair exchange protocol by using ATS(Alternating Transition Systems), and verifies the fairness, timeliness and abuse-freeness of the fair exchange protocol effective by using the formal verification tool MOCHA. The paper analyzes and discusses the result of the verification in the end, and finds that this protocol does not satisfy the fairness and abuse-freeness.
