推論を利用した暗号プロトコルの自動検証に関する研究

1997 Fiscal Year Annual Research Report

• Project/Area Number: 07650413
• Research Institution: TOKYO INSTITUTE OF TECHNOLOGY
• Principal Investigator: 黒沢 馨 東京工業大学, 工学部, 教授 (60153409)
• Co-Investigator(Kenkyū-buntansha): 辻井 重男 中央大学, 理工学部, 教授 (50020350) ; 佐藤 敬 東京工業大学, 工学部, 助手 (30262281)
• Keywords: BANロジック / 暗号プロトコル / 論理式 / 鍵配送 / 検証

Research Abstract

BANロジックは,鍵の配送,秘密の共有あるいは情報の転送などを行う暗号プロトコルの検証に有効であることが知られている.しかし,従来は安全な暗号プロトコルが満たすべき論理式が検討されているのみであった.
本研究では,安全でない暗号プロトコルが満たすべき論理式を示すと共に,その有効性を具体例を用いて示している.Pを受信者,Qを送信者,Xを鍵(秘密または情報)を含むメッセージとする.まず,
P believes P sees X ∧ ¬P believes Q says X
を導出できるプロトコルにおいては,敵のなりすまし攻撃が存在する.という定理1を示した.次に
P says X for the first time 〓 fresh(X) ∧ P says X
と定義する.このとき
P believes P sees X ∧ ¬P believes Q says X for the first time
を導出できるプロトコルについては、敵のなりすまし攻撃または,リプレイ攻撃が存在する.という定理2を示した.また
P believes Q said X ∧ ¬P believes fresh(X) ⇒ ¬P believes Q says X for the first time
の導出規則がAbadi-Tuttleの意味論において真であることを証明した.この導出規則をAnderew Square RPC Handshakeに適用して,定理2の論理式が導出できることを示し,本手法の有効性を確認した.