文章基本信息
- 标题：CafeOBJ入門(5) 認証プロトコルの検証
- 本地全文：下载
- 作者：緒方 和博 ; 二木 厚吉 ; 中村 正樹 等
- 期刊名称：コンピュータ ソフトウェア
- 印刷版ISSN：0289-6540
- 出版年度：2009
- 卷号：26
- 期号：1
- 页码：1_71-1_83
- DOI：10.11309/jssst.26.1_71
- 出版社：Japan Society for Software Science and Technology
- 摘要：
代数仕様言語CafeOBJによる認証プロトコルの検証の例を示す．NSLPK認証プロトコルは，公開鍵暗号方式に基づく，2つの主体間の相互認証のためのプロトコルである．NSLPK認証プロトコルに定められたメッセージ送受信を終えると，2つの主体はある情報を共有する．その情報が，たとえ悪意のある主体が存在していたとしても第三者にもれることはない，という性質を秘匿性という．NSLPK認証プロトコルが秘匿性を満たすことの証明譜による検証を解説する．
