CafeOBJ入門(5) 認証プロトコルの検証 Introducing CafeOBJ (5) : Verification of an Authentication Protocol

この論文にアクセスする

著者

    • 緒方 和博 OGATA Kazuhiro
    • 北陸先端科学技術大学院大学情報科学研究科 Graduate School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
    • 二木 厚吉 FUTATSUGI Kokichi
    • 北陸先端科学技術大学院大学情報科学研究科 Graduate School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)

抄録

代数仕様言語CafeOBJによる認証プロトコルの検証の例を示す.NSLPK認証プロトコルは,公開鍵暗号方式に基づく,2つの主体間の相互認証のためのプロトコルである.NSLPK認証プロトコルに定められたメッセージ送受信を終えると,2つの主体はある情報を共有する.その情報が,たとえ悪意のある主体が存在していたとしても第三者にもれることはない,という性質を秘匿性という.NSLPK認証プロトコルが秘匿性を満たすことの証明譜による検証を解説する.

An example of verification of authentication protocols with CafeOBJ algebraic specification language is shown. The NSLPK authentication protocol is based on the public-key cryptosystem. Two principals can use the protocol to achieve the mutual authentication between them. The successful completion of the message exchanges specified by the protocol lets two principals share some information. The secrecy property is as follows: even when there exist malicious principals, the information is never leaked to any third parties. Described is the verification with proof score that the protocol satisfies the (nonce) secrecy property.

収録刊行物

  • コンピュータ ソフトウェア

    コンピュータ ソフトウェア 26(1), 71-83, 2009

    日本ソフトウェア科学会

各種コード

  • NII論文ID(NAID)
    130004549136
  • 本文言語コード
    UNK
  • ISSN
    0289-6540
  • データ提供元
    J-STAGE 
ページトップへ