A usage control policy specification with Petri nets

In this paper we propose a novel usage control policy specification based on Coloured Petri Nets formalism. Recently, usage control has been proposed in order to overcome the shortcomings of transitional access control that fails to meet new security requirements of today´s highly dynamic and distributed systems. These new environments require for example (i) a continuity of control, (ii) fulfillment checks of obligatory tasks, during or after the usage end, (iii) an integration between functional behavior and security policy, and (iv) the management and control of concurrent and parallel usages by different subjects. Taking all these requirements into consideration, our usage control policy includes three main rule types: behavioral, security and concurrency rules. Security rules, can be further classified either into instant-, -ongoing, and post rules or into authorization and obligation rules. Instant rules must be checked before the execution of an action is granted, ongoing rules are checked during the execution of an action, and finally post rules are checked after the execution is finished. Therefore, post rules are only of type obligation. Coloured Petri nets are used because of their powerful modeling capabilities of distributed and concurrent systems and their efficiency for specification of systems by embodying the support of ML functional programming language.