Smatch: Formal dynamic session management model for RBAC

This paper extends RBAC sessions with shareability, reusability and switchability properties. We define the Smatch (Secure MAnagement of swiTCH) model in which authorized users can join, leave, reopen and reuse dynamic sessions. In Smatch, subjects can also share sessions and dynamically switch their role or function with other subjects from the same or different organizations. Subjects can authenticate using their function which will automatically activate the set of roles associated with this function. The Smatch model is based on the situation calculus which extends first order logic with actions. It provides means to specify contextual access control and authentication policies which apply to control functional behavior of dynamic sessions. We formally analyze decidability and complexity of several problems like decision, planning and proof of properties in the Smatch model. We also suggest an implementation of Smatch using Eyeos, an open-source web based Operating System.