Task-PIOAに基づくIdeal Functionality実現の証明の自動化(「さまざまな分野の形式的検証最前線」及びAI一般)
スポンサーリンク
概要
- 論文の詳細を見る
本論文では,実システムとidealシステムの識別不能に基づくセキュリティプロトコルの安全性証明を定式化した,Canetti, Lynch等[4]のtask-PIOAの枠組において,安全性証明の手続きの中の重要なステップとなるsimulation関係の証明を自動化する手法を提案する.このsimulation関係の証明では,実システムとidealシステムの間の動作の対応を設定し,また,両システムの状態の間に適切な関係を定義して,その関係が,対応する状態遷移で保たれることを証明している.そして,これらの対応設定,関係定義は人間の創意に委ねられている.ここでは,このような動作の対応,状態間の関係を考慮することなく,自動でsimulation関係を証明する方法を,プロセス代数でプロセスのbisimulation関係を示す時に利用されるpartition refinementアルゴリズムを用いて与えた.
- 2006-11-03
著者
関連論文
- Techniques to accelerate request processing for Byzantine fault tolerance (コンピュテーション)
- UC frameworkにおけるfunctionalityの合成について(情報通信基礎サブソサイエティ合同研究会)
- OWLオントロジー間の自動対応付け手法の提案と評価(「さまざまな分野の形式的検証最前線」及びAI一般)
- Byzantine Agreement on the Order of Processing Received Requests is Solvable Deterministically in Asynchronous Systems
- BDIアーキテクチャにおけるコミットメント戦略を実現するための形式的検証手続き(ソフトウェア基礎,プログラム理論)
- エージェントの相互信念を扱う拡張BDI logicの演繹体系
- 合理的エージェントの心的状態に関する整合性の実現と応用について(ソフトウェアエージェントとその応用論文)
- エージェントの相互信念を扱う拡張BDI logicの演繹体系
- BDI Logicのsequent calculusによる演繹体系(マルチエージェント)
- 確率的近似法を用いた頑強なオンライン評判メカニズム(分散協調とエージェント)