2E-4
紛失通信プロトコルの解析のための可能世界意味論に基づく形式体系
○小黒博昭,萩原茂樹,米崎直樹(東工大)
著者らはこれまでに、暗号プロトコルの基本要素としてよく
利用される1-out-of-2型の紛失通信プロトコルに着目し、
同プロトコルの一実現形態であるEGL85プロトコルの性質を
記号論的に解析するための形式体系を提案している。
しかしながら、従来の形式体系には構文に対する直観的な
意味しか与えられておらず、形式的な意味論が与えられて
いなかった。本稿では,従来の形式体系に対し、可能世界
モデルに基づく意味論を与え、その意味論における推論規則の
健全性を示す。この健全性により、EGL85プロトコルは、
「受信者は、送信者が用いた二つの送信対象メッセージが
同じであるか、異なるかを識別できる」という性質を持つ
ことが示される。