電子情報通信学会 2015年ソサイエティ大会
セッション:セキュリティプロトコルのためのシステム数理とその周辺

暗号プロトコル検証入門

産業技術総合研究所 情報技術研究部門
磯部 祥尚

暗 号プロトコルは、通信の盗聴やなりすましの防止のために、暗号技術を用いた通信手順である。通信手順に不備があると、暗号文を解読しなくても、攻撃が成功 する可能性もある。本稿では、ニーダム・シュレーダー公開鍵プロトコル(以下、NSPKプロトコル)の既知の脆弱性(なりすまし可能)を例にして、暗号プ ロトコルの形式的な検証方法を、Gavin Lowe の論文(TACAS 1996)をもとに紹介する。

講演に使用したスライド:
NSPKプロトコルのCSPM記述(FDR検証用):
補足: