Interleaving vs True Concurrency: Some Instructive Security Examples

Abstract

Information flow security properties were defined some years ago in terms of suitable equivalence checking problems. These definitions were provided by using sequential models of computations (e.g., labeled transition systems [ 17 , 26 ]), and interleaving behavioral equivalences (e.g., bisimulation equivalence [ 27 ]). More recently, the distributed model of Petri nets has been used to study non-interference in [ 1 , 5 , 6 ], but also in these papers an interleaving semantics was used. By exploiting a simple process algebra, called CFM [ 18 ] and equipped with a Petri net semantics, we provide some examples showing that team equivalence, a truly-concurrent behavioral equivalence proposed in [ 19 , 20 ], is much more suitable to define information flow security properties. The distributed non-interference property we propose, called DNI, is very easily checkable on CFM processes, as it is compositional, so that it does not suffer from the state-space explosion problem. Moreover, DNI is characterized syntactically on CFM by means of a type system.