Task-PIOAに基づくIdeal Functionality実現の証明の自動化(「さまざまな分野の形式的検証最前線」及びAI一般)

スポンサーリンク

概要

論文の詳細を見る
本論文では,実システムとidealシステムの識別不能に基づくセキュリティプロトコルの安全性証明を定式化した,Canetti, Lynch等[4]のtask-PIOAの枠組において,安全性証明の手続きの中の重要なステップとなるsimulation関係の証明を自動化する手法を提案する.このsimulation関係の証明では,実システムとidealシステムの間の動作の対応を設定し,また,両システムの状態の間に適切な関係を定義して,その関係が,対応する状態遷移で保たれることを証明している.そして,これらの対応設定,関係定義は人間の創意に委ねられている.ここでは,このような動作の対応,状態間の関係を考慮することなく,自動でsimulation関係を証明する方法を,プロセス代数でプロセスのbisimulation関係を示す時に利用されるpartition refinementアルゴリズムを用いて与えた.
2006-11-03

著者

関連論文

もっと見る

スポンサーリンク