Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4955740 | Journal of Information Security and Applications | 2017 | 11 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computer Networks and Communications
Authors
Kazuhiro Ogata,