| 研究概要 |
本年度は,昨年度に引き続き,暗号プロトコルの安全性に関する種々の性質を扱うための拡張を行い,かつその拡張体系の公理が妥当となるような計算論的モデルの構築を行った.特に前半では,Gergely Bana氏らの協力のもとで,昨年度までに得られた論理推論体系とそのモデルを論文として取りまとめ,国際会議への投稿したものの,不採録となった.その際に査読者に指摘された問題点は,研究代表者らの提案する推論体系が十分簡略化されておらず,実際のプロトコル証明への適用が難しいということであった.
以上をふまえて,本年度の後半以降は,再度国際会議への投稿を目指し,それまでに得られた論理推論体系の簡略化の作業をBana氏らと共同で行った.また,プロトコル合成による検証法の構築や,定理証明支援系Isabelleを用いた推論体系のプロトタイプ実装の作業にも着手した.これらの成果を論文としてまとめ,国際会議に投稿したものの,再度不採録となった.この結果から,推論体系の簡略化をより一層進める必要のあることを認識し,これまで採用してきた安全性に関わる述語記号に新たな種類のものを加える検討を進めた.また,これまで採用してきた一階述語論理を基にするアプローチの他に,新たに動的論理(Dynamic Logic)などの枠組みを用いた公理化なども試みてみたが,十分な簡略化された体系を得ることができなかった.そのため,一階述語論理の枠組みを維持しながら,安全性証明の対象として,プロトコルの認証に関する性質のみに焦点を絞り,プロトコルで扱われる情報の秘匿性については,論理体系の仮定として扱うという方針で研究を進めた.
|
