Policy Controlled System and Its Model Checking

Shigeta KUNINOBU  Yoshiaki TAKATA  Naoya NITTA  Hiroyuki SEKI  

IEICE TRANSACTIONS on Information and Systems   Vol.E88-D   No.7   pp.1685-1696
Publication Date: 2005/07/01
Online ISSN: 
DOI: 10.1093/ietisy/e88-d.7.1685
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Application Information Security
policy control,  policy controlled system,  verification,  model checking,  pushdown system,  

Full Text: PDF(1.3MB)>>
Buy this Article

A policy is an execution rule (or constraint) for objects in a system to retain security and integrity of the system. We introduce a simple policy specification language and define its operational semantics. A new NFA construction algorithm that works in linear time is proposed and a model checking method for policy controlled system (PCS) is presented. We conducted verification of a sample PCS for hotel reservation by our automatic verification tool and the experimental results showed the efficiency of the proposed method.