Inductive Verification of Security Protocols with Rewriting

DOI Web Site 1 Citations 35 References
  • OGATA Kazuhiro
    NEC Software Hokuriku, Ltd. Japan Advanced Institute of Science and Technology (JAIST)
  • FUTATSUGI Kokichi
    Japan Advanced Institute of Science and Technology (JAIST)

Bibliographic Information

Other Title
  • 書き換えによるセキュリティプロトコルの帰納的検証
  • カキカエ ニ ヨル セキュリティプロトコル ノ キノウテキ ケンショウ

Search this article

Abstract

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

Journal

  • Computer Software

    Computer Software 20 (3), 266-284, 2003

    Japan Society for Software Science and Technology

Citations (1)*help

See more

References(35)*help

See more

Related Projects

See more

Details 詳細情報について

Report a problem

Back to top