近年，インターネットが普及し，通信と処理を保護するためにセキュリティプロトコ ルの重要性が増大してきた．このような背景から侵入者の攻撃や不正行為に対して安 全であることを検証する方法が開発されている．その方法の一つとして一階論理の定 理自動証明系であるSPASSを用いた方法がある． 本研究では，セキュリティプロトコルの検証に定理自動証明系を応用することの可能 性を調査することを目的とする．本研究はNeuman-Stubblebine ProtocolのSPASSによ る分析と修正の過程を追跡し，新たな修正方法を与えてNeuman-Stubblebine Protocolとは異なるプロトコルを作成してその安全性をSPASSにより確認する．また 既存の他のプロトコルに対してSPASSで分析を行い，プロトコルの欠点を修正し，安 全性の高いものに改良する．