| Presentation | 2006-11-10 Mechanization of Task-PIOA based Proving Procedure for Realization of Ideal Functionalities Tadashi ARARAGI, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | 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. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Security Protocol / Formal Verification / Simulation / Ideal Functionality / Partition Refinement |
| Paper # | AI2006-18 |
| Date of Issue |
| Conference Information | |
| Committee | AI |
|---|---|
| Conference Date | 2006/11/3(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Mechanization of Task-PIOA based Proving Procedure for Realization of Ideal Functionalities |
| Sub Title (in English) | |
| Keyword(1) | Security Protocol |
| Keyword(2) | Formal Verification |
| Keyword(3) | Simulation |
| Keyword(4) | Ideal Functionality |
| Keyword(5) | Partition Refinement |
| 1st Author's Name | Tadashi ARARAGI |
| 1st Author's Affiliation | NIPPON TELEGRAPH AND TELEPHONE CORPORATION, NTT Communication Science Laboratories() |
| Date | 2006-11-10 |
| Paper # | AI2006-18 |
| Volume (vol) | vol.106 |
| Number (no) | 340 |
| Page | pp.pp.- |
| #Pages | 5 |
| Date of Issue | |