セキュリティプロトコルの簡易検証I : 具体意味論

概要

論文の詳細を見る
To represent secure systems over open networks, there exists cryptosystems and its application. Robustness of a cryptosystem is given by computational approaches and formal ones. The computational approach relies on issues of complexity and probability, on the other hand, the formal method omit discussions about complexity of systems using an idealized cryptography, which is called "Computational hardness assumptions". Even if we omit computational discussion, it is still hard to prove the safety properties of network protocols. To cope with undecidability and complexity of analyzing formal systems, the author introduces "Yield-Arrow Nonce Protocol Inspection Method (YANPI method)". Using this method, we expect to get lightweight and intuitive verification method. The YANPI Method's model is established on a concrete semantics using directed graphs, however, its analyzing algorithms use abstracted directed graphs and its refinement. In this paper, we introduce the formal concrete model of the YANPI method. In the next paper, we are planning to present YANPI method's abstraction and refinement algorithms.
2007-03-31