暗号プロトコルの安全性判定問題が多項式時間で決定可能となるための十
分条件
前田 昌也 (9651204)
暗号を用いたプロトコルの安全性を形式的に検証する研究が最近さかんになさ
れている。安全性判定問題は、プロトコル中で用いられる操作や暗号化関数の
性質を表す書き換え規則のもとでの、敵対者の目的であるゴール項の意味論的
単一化可能性問題として定義される。しかし、一般的な安全性判定問題は決定
不能であることが証明されており、ごく制限された問題クラスが決定可能であ
る。本発表では、より広いクラスの暗号プロトコルに対して安全性の判定を可
能とする問題クラスを示す。