SPINに基づくセキュリティプロトコル検証システム

情報処理学会 Web Site 被引用文献4件 参考文献12件

書誌事項

タイトル別名
  • SPIN ニ モトヅク セキュリティプロトコル ケンショウ システム
  • Security Protocol Verification System Based on SPIN
  • プロトコル検証

この論文をさがす

抄録

本論文では，SPINによるセキュリティプロトコルの検証を行うシステムの提案と実装および評価について述べる．SPINに基づくセキュリティプロトコルの検証については，J?o sangがすでに考察を行っており，その実現性については問題があるという結論に達している．我々は，セキュリティプロトコルの運用にある制限を設定し，その範囲での動作について総当たりで検証するシステムの開発を行った．我々のシステムの特徴は，メッセージの暗号化，復号化などのセキュリティプロトコルに特有の処理を記述するためにPROMELAを拡張したSPROMELAを開発した点である．また，PROMELAから，SPROMELAへ変換し，さらに攻撃者プロセス，セキュリティ条件が破られたことを判定するモニタプロセスを自動的に生成するトランスレータを開発した．検証の際のシミュレーション条件設定やシミュレーション実行は，SPINの環境と統合され，GUIを使って操作できる環境となっている．この環境で，セキュリティホールがあることが分かっているOtway-Reesプロトコルの検証を行い，具体的なアタックの手順を導出することができた．

This paper describes the system which verifies security protocols using SPIN.J\o sang has already considered verification of security protocols based on SPIN,and there is a problem about the implementability in conclusion.We restrict the operation of a security protocol within limits,and developed the system verifying the protocol.The feature of our system is extension to PROMELA (SPROMELA) for describing security protocols,such as encryption of a message, and decryption.And, we developed translater which converts SPROMELA to PROMELA,and which automatically generates the attacker process andthe monitor process checking whether security conditions are broken.When we verify protocols,configuration and execution of the simulator are unified to the environment of SPIN using GUI.In this environment, we verified the Otway-Rees protocol that has wellknown security holes,and derived procedure of attack.

収録刊行物

被引用文献 (4)*注記

もっと見る

参考文献 (12)*注記

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ