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)
Vice Chair

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