PrT-Net Based Analysis of Information Flow Security Nets

摘要

Information Flow Security Nets (IFS-nets) provide a framework for the definitionof security models. The aim of this work is to show how the security properties of an IFS-net can be inspected indirectly by constructing a Predicate/Transition net (PrT-net) and by examining the reachability graph of the constructed PrT-net. It is shown that there exists a one-to-one correspondence between the reachable markings of the IFS-net and the reachable markings of the corresponding PrT-net. It is also shown that there exists a one-to-one correspondence between the firing sequences of an IFS-net and the firing sequences of the corresponding PrT-net. Several results linking the security properties of IFS-nets to the properties of the reachability graphs of the corresponding PrT-nets are provided. Finally, the use of the proposed approach is illustrated in an example where the upgrading and downgrading of data must be properly done.