電子情報通信学会 2015年ソサイエティ大会
セッション:セキュリティプロトコルのためのシステム数理とその周辺
暗号プロトコル検証入門産業技術総合研究所 情報技術研究部門
磯部 祥尚
暗
号プロトコルは、通信の盗聴やなりすましの防止のために、暗号技術を用いた通信手順である。通信手順に不備があると、暗号文を解読しなくても、攻撃が成功
する可能性もある。本稿では、ニーダム・シュレーダー公開鍵プロトコル(以下、NSPKプロトコル)の既知の脆弱性(なりすまし可能)を例にして、暗号プ
ロトコルの形式的な検証方法を、Gavin Lowe の論文(TACAS 1996)をもとに紹介する。
講演に使用したスライド:
NSPKプロトコルのCSPM記述(FDR検証用):
補足:
- 検証時間目安は CPU 5Y70, 1.1GHz~1.30GHz による
- NSPKプロトコルの本CSPM記述の説明は2015年ソサイエティ大会の原稿参照
(ただし、検証に影響ない範囲で状態数を削減済)