| 講演名 | 2006-11-10 Task-PIOAに基づくIdeal Functionality実現の証明の自動化(「さまざまな分野の形式的検証最前線」及びAI一般) 櫟 粛之, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本論文では,実システムとidealシステムの識別不能に基づくセキュリティプロトコルの安全性証明を定式化した,Canetti, Lynch等[4]のtask-PIOAの枠組において,安全性証明の手続きの中の重要なステップとなるsimulation関係の証明を自動化する手法を提案する.このsimulation関係の証明では,実システムとidealシステムの間の動作の対応を設定し,また,両システムの状態の間に適切な関係を定義して,その関係が,対応する状態遷移で保たれることを証明している.そして,これらの対応設定,関係定義は人間の創意に委ねられている.ここでは,このような動作の対応,状態間の関係を考慮することなく,自動でsimulation関係を証明する方法を,プロセス代数でプロセスのbisimulation関係を示す時に利用されるpartition refinementアルゴリズムを用いて与えた. |
| 抄録(英) | Canetti et al recently proposed a formal framework for proving correctness of security protocols. The framework is based on task-PIOA developed in [4]. For this framework, we give a method of mechanization of proving simulation relation, which is one of main steps of proving security property. This proving step consists of introduction of a proper relation between the states of a real system and an ideal system, making a correspondence between each action of the real system and a sequence of actions of the ideal systems, and proving that the corresponding actions preserve the relation. Currently, these procedures are done manually, and the relation and the correspondence are introduced by human's device. In this paper, we give a method of proving this simulation relation automatically without introducing the relation and the correspondence. In achieving this method, we employed a partition refinement algorithm which is used to prove bisimulation relation in process algebras. |
| キーワード(和) | セキュリティプロトコル / 形式的検証 / シミュレーション / Ideal Functionality / Partition Refinement |
| キーワード(英) | Security Protocol / Formal Verification / Simulation / Ideal Functionality / Partition Refinement |
| 資料番号 | AI2006-18 |
| 発行日 |
| 研究会情報 | |
| 研究会 | AI |
|---|---|
| 開催期間 | 2006/11/3(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | Task-PIOAに基づくIdeal Functionality実現の証明の自動化(「さまざまな分野の形式的検証最前線」及びAI一般) |
| サブタイトル（和） | |
| タイトル（英） | Mechanization of Task-PIOA based Proving Procedure for Realization of Ideal Functionalities |
| サブタイトル（和） | |
| キーワード(1)（和/英） | セキュリティプロトコル / Security Protocol |
| キーワード(2)（和/英） | 形式的検証 / Formal Verification |
| キーワード(3)（和/英） | シミュレーション / Simulation |
| キーワード(4)（和/英） | Ideal Functionality / Ideal Functionality |
| キーワード(5)（和/英） | Partition Refinement / Partition Refinement |
| 第 1 著者 氏名（和/英） | 櫟 粛之 / Tadashi ARARAGI |
| 第 1 著者 所属（和/英） | 日本電信電話株式会社 NTTコミュニケーション科学基礎研究所 NIPPON TELEGRAPH AND TELEPHONE CORPORATION, NTT Communication Science Laboratories |
| 発表年月日 | 2006-11-10 |
| 資料番号 | AI2006-18 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 340 |
| ページ範囲 | pp.- |
| ページ数 | 5 |
| 発行日 | |