Model checking the iKP electronic payment protocols

There are two main contributions described in this article: (1) to propose an effective way to write OTSs as rewrite theory specifications, and (2) to conduct a case study in which an electronic commerce protocol has been model checked. Contribution (1) can be regarded as an effective way to translate equational theory specifications of OTSs for interactive theorem proving into rewrite theory specifications of OTSs for model checking. Moreover, since rewrite theory specifications of OTSs can be used for interactive theorem proving as well, contribution (1) may lead to the desirable situation aforementioned.