談話会

セキュリティ・プロトコルについて概説。BAN Logicを中心とした歴史の説明。次回はPCL。
Needham-Shroeder公開鍵認証プロトコルは、BAN Logicで安全性が証明されたにもかかわらず、実はアタックがありうることがLoweによって示された（PCLに拡張するとこのアタックがあり得たことは証明される）。この失敗の原因は

1. BAN論理のような証明論的技法では反例（この場合はアタック）を構成するのが難しい（証明論的技法の欠点！）
2. BAN論理の言語への翻訳が恣意的（Loweのアタックはこの時切り落とした情報を使って行われる）

である、ということでよろしいのでしょうか。
あと、余り関係ないけれど、BAN論理はいわゆる意味論を持たない dudctive system で、例えばRestallだったらこれを論理とは呼ばないだろう。