PrT-net Based Analysis of Information Flow Security Nets

Reference:

Jari Juopperi. PrT-net based analysis of information flow security nets. Research Report A34, Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory, Espoo, Finland, March 1995.

Abstract:

Information Flow Security Nets (IFS-nets) provide a framework for the definition of security models. IFS-nets employ a class of low-level Petri nets as their model of computation while the notion of security is based on the extension of Denning's information flow model. An inconvenient property of IFS-nets is that the direct analysis of the nets without specialized tools is difficult. The aim of this work is to show how the security properties of an IFS-net can be inspected indirectly by constructing a PrT-net and by examining the reachability graph of the constructed PrT-net. The crux of this approach is the mapping which defines how the PrT-net corresponding to an IFS-net can be created. It is shown that there exists an 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 an 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. The IFS-net and the corresponding PrT-net of the example system are created. After this the security properties of the system are analysed with the reachability analysis tool PROD.

Keywords:

security model, information flow model, security analysis, Information Flow Security Nets, Predicate/Transition nets, Petri nets, reachability analysis

Suggested BibTeX entry:

@techreport{HUT-TCS-A34,
    address = {Espoo, Finland},
    author = {Jari Juopperi},
    institution = {Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory},
    month = {March},
    number = {A34},
    pages = {87},
    title = {{P}r{T}-net Based Analysis of Information Flow Security Nets},
    type = {Research Report},
    year = {1995},
}