基于概率模型检测的合同签订协议分析

概率合同签订协议的公平性具有典型的概率性质。概率模型检测是一种验证存在随机行为系统的分析技术。基于概率模型检测技术，在原协议的基础上建立了离散马尔可夫链和有限状态机模型，用概率模型检测工具——PRISM验证了它的公平性，发现其公平性不满足时，在此基础上对原协议从双方交换信息的策略上进行了扩充改进，使协议更为公平，满足了合同签订的基本要求。

Analysis of Contract Signing Protocol Based on Probabilistic Model Checking

The fairness of probabilistic contract signing is a probabilistic property. Probabilistic model checking is a formal verification technique for the analysis of systems which exhibit stochastic behavior. This paper focus on probabilistic contract signing based on probabilistic model checking. It is exemplified by the probabilistic contract signing of EGL which is constructed as Discrete Time Markov Chains-- DTMCs. Its finite state automata as well as its fairness properties are verified with the tool of probabilistic model checking --PRISM. Moreover, it has been greatly improved based on the schedule of message exchanging between both participators. It thus satisfies the basic conditions of contract signing.