Automatic Verification System for Authentication Protocols

概要

論文の詳細を見る
There are strong needs of the security for the network softwares, especially for the authentication protocols. It is necessary for the security of the authentication protocol to holds the BAN logic's completeness, which stands for working properly. In general, it is not necessarily easy to confirm protocols' completeness in the BAN logic by the hand work. Then, we constructed the system which was able to verify the completeness of an authentication protocol automatically. The verification with the system is performed as the following procedure. Firstly, the specification of the given authentication protocol and the assumption for it are described as the propositions of the BAN logic. Nextly, the both propositions are input to the inference system, implemented in the CafeOBJ. Then, the inference of BAN logic is automatically performed by the system. Finally, the user of system can detect if it is complete or not according to the result. We could verify the completeness of some authentication protocols by using this system. In this paper, as an example, we show the process of dealing with the two protocols: Needham-Schroeder shared key protocol and public key protocol.
社団法人電子情報通信学会の論文
2002-02-01