書き換えによるセキュリティプロトコルの帰納的検証

書誌事項

タイトル別名
  • Inductive Verification of Security Protocols with Rewriting
  • カキカエ ニ ヨル セキュリティプロトコル ノ キノウテキ ケンショウ

この論文をさがす

抄録

代数仕様言語で(主に帰納法の)証明を記述し,証明の正しさを書き換えにより確認する方法を用いてセキュリティプロトコルの安全性を検証する方法について記述する.例題として,Loweにより修正されたNSPK認証プロトコルを用いる.本提案手法は,Paulsonの帰納的手法に類似しているが,証明の可読性や理解の容易さの点で強みがある.これは本提案手法における検証の基本機構が,比較的理解が容易である書き換え(一方向の等式推論)であることに起因している.また,代数仕様言語を用いることから,セキュリティプロトコルで使用する各種データ型を適切に定義することができ,セキュリティプロトコル(のモデル)を記述した文書の可読性についても優れている.

収録刊行物

被引用文献 (1)*注記

もっと見る

参考文献 (35)*注記

もっと見る

関連プロジェクト

もっと見る

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

問題の指摘

ページトップへ