In: Lecture Notes in Computer Science : Automated Technology for Verification and Analysis, Volume 4218, 2006, pages 461-476. 2006. URL: http://dx.doi.org/10.1007/1190191434.
Abstract: We study Mobile Synchronizing Petri Nets (MSPN), that allow the description of systems composed of a collection of interacting mobile components. Unlike in other models of modular or mobile Petri Nets, we focus on security issues. For that purpose, we introduce a fresh name generation mechanism to provide special authentication tokens. These names are treated in an abstract way, which allows us to retain the decidability of some properties that hold for Place/Transition nets (P/T nets). In this paper, we are interested in checking that the desired security properties of a system still hold, even when in an arbitrary malicious environment. However, since we are dealing with security properties, we must regard that some names of the system are assumed to be secret, which restricts the set of possible environments. We develop a symbolic semantics that takes into account the behaviour of any of those environments, though in an abstract way. We establish the desired relations between the original and the symbolic semantics to conclude that the latter is correct and complete with respect to the former.
Back to the Petri Nets Bibliography