| 研究概要 |
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 Psees 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の論理式が導出できることを示し,本手法の有効性を確認した.
|
