Analysis of Contract Signing Protocol Based Probabilistic Model Checking
Rongsheng Dong · Journal of Guilin University of Electronic Technology · 2005
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.