Inference of Local Properties in Petri Nets Composed through an Interface

We study a notion of visibility of the local states of an Elementary Petri net obtained by composition through an interface. The components are three EN systems: the defender, providing a service to the environment, the attacker, a client of the service, and the interface, that models the protocol of interaction between the other two nets. Intuitively, the definition of visibility is meant to capture the idea that an attacker tries to infer the validity of a local state of the defender even if he can observe only the interface and itself. Our analysis is based on the notion of invariant properties and bisimilarity in Petri nets. We suggest also a measure of the degree of visibility of local states of the defender as seen by the attacker.