文章基本信息

标题：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認証プロトコルが秘匿性を満たすことの証明譜による検証を解説する．