Petri nets for the verification of ubiquitous systems with transient secure association

Abstract

Transient Secure Association has been widely accepted as a possible alternative to traditional authentication in the context of Ubiquitous Computing. We develop a formal model for the Resurrecting Duckling Policy that implements it, called TSA systems, which is based on Petri Nets, thus obtaining amenable graphical representations of our systems. We prove that TSA specifications have the same expressive power as P/T nets, so that coverability, that can be used to specify security properties, is decidable for TSA systems. Then we address the problem of implementing TSA systems with a lower level model that only relies on the secure exchange of keys. If we view these systems as closed then our implementation is still equivalent to P/T nets. However, if we consider an open framework then we need a mechanism of fresh name creation to get a correct implementation. This last model is not equivalent to P/T nets, but the coverability problem is still decidable for them. © Springer-Verlag Berlin Heidelberg 2007.