A Finite Automata Model for Optimistic Contract Signing Protocols
Chang Liang · Journal of Guilin University of Electronic Technology · 2004
The optimistic electronic contract signing protocol is a kind of typical security protocols for fair electronic contracts exchange,which is more complicated,and brings more challenges for its formal analysis.Model checking is an efficient way to analyze security protocols,where modeling the protocol and its running environment exactly and comprehensively is the key issue and starting point.In this paper,a novel model is presented,and illustrated by Garays' protocol,where the honest principals,dishonest principals,and different kinds of communication channels are modeled as finite automata respectively.