DISCRETE EVENT SYSTEMS APPROACH TO THE VERIFICATION OF THE INFORMATION FLOW PROPERTIES IN SECURE PROTOCOLS

摘要

This paper introduces a new algorithmic approach to the problem of checking the intransitive non-interference (INI) using discrete event systems (DES) tools and concepts. INI is an information flow property widely used in formal verification of computer systems and security protocols. First a new property called iP-observability (observability based on a purge function) is introduced to capture INI. An equivalence between iP-observability and P-observability (observability as used in DES) is then established. This paper also presents an algorithm to transform the automaton modelling the system/protocol into an automaton where P-observability can be checked, which is equivalent to verifying INI for the original system. Since P-obervability can be checked with a polynomial complexity, this algorithmic approach can effectively verify the important security property of INI.