Petri nets with name creation for transient secure association

Transient secure association has been widely accepted as a possible alternative to traditional authentication in the context of Ubiquitous Computing. Two components in a distributed system with transient secure association may share a master-slave relationship, which creates a hierarchical but dynamic structure of components. In this paper we develop several formal models for distributed systems with transient secure association, with incremental expressive power, all based on Petri nets. The first model, that we call transient secure association (TSA) systems, considers finitely many components. Then we consider a small extension of TSA systems, in which slaves are initialized whenever a master-slave relation is broken. Last, we define unbounded TSA (uTSA) systems, for which the number of components is not bounded. For each of the defined formalisms, we establish a link to a known class of Petri nets, thus inheriting the corresponding (un)decidability results from them.