RBAC metamodel

//RBAC metamodel

abstract User
    name : string 
    maxRoles : int ?
    maxRolesRespectingHierarchy ?
    maxSessions : int ?
    role -> Role +
        [parent in this.user]
    session -> Session *
        [parent in this.user]
    pred -> User ?
        [parent in this.succ]
    succ -> User ?
        [parent in this.pred]
    snapshot -> Snapshot 
        [parent in this.user]
    numberOfRoles:int
	[this = if maxRolesRespectingHierarchy then (#(role++role.junior)) else (#role)]
    [maxRoles => numberOfRoles < maxRoles]
    [maxSessions => #session < maxSessions]
    [all r:Resource|r.resourceBasedDynamicSeparationOfDuty => (one u_r:User_Resource|u_r.usr = this && u_r.res = r && lone u_r.tempSet1.action)]
    [all r:Resource|r.historyBasedDynamicSeparationOfDuty =>(one u_r:User_Resource|u_r.usr = this && u_r.res = r && #u_r.tempSet1.action < #r.action)]
    [succ => succ.snapshot = snapshot.succ]
    [succ => succ.name.ref = name.ref]
    


User_Resource *//Hepler clafer, used to implement set comprehensions in constraints that quantifies over all pairs of User-Resource.
    usr -> User
    res -> Resource
    tempSet1 -> Access*
	[this in res.access && this.session.user in (usr ++ usr.succ)]
    [all a:Access| (a in res.access && a.session.user in (usr ++ usr.succ)) => a in tempSet1]

abstract Role
    name : string 
    maxMembers : int ?
    maxJuniors : int ?
    exclusiveJuniorsAllowed ?
    maxSeniors : int ?
    permission -> Permission +
        [parent in this.role]
    user -> User *
        [parent in this.role]
    senior -> Role *
        [parent in this.junior]
    junior -> Role *
        [parent in this.senior]
    required -> Role *
        [parent in this.dependent]
    dependent -> Role *
        [parent in this.required]
    session -> Session *
        [parent in this.role]
    mutuallyExclusiveA -> MutuallyExclusive *
        [parent in this.roleA]
    mutuallyExclusiveB -> MutuallyExclusive *
        [parent in this.roleB]
    [this not in senior]
    [maxMembers => #user < maxMembers]
    [all u:user|required in u.role]
    [maxJuniors => #junior < maxJuniors]
    [maxSeniors => #senior < maxSeniors]
    [exclusiveJuniorsAllowed ||(all r1;r2:junior|(all m:r1.mutuallyExclusiveA |(m.wrtUserAssignment && m.roleB = r2) => m.identicalSeniorAllowed) &&(all m:r1.mutuallyExclusiveB |(m.wrtUserAssignment && m.roleB = r2) => m.identicalSeniorAllowed) )]
//Bug: Can't quantify over set union: [all a:(mutuallyExclusiveA++mutuallyExclusiveB)|......]
    


abstract Permission
    name : string 
    maxRoles : int ?
    maxSessions : int ?
    action -> Action *
        [parent in this.permission]
    resource -> Resource 
        [parent in this.permission]
    role -> Role *
        [parent in this.permission]
    required -> Permission *
        [parent in this.dependent]
    dependent -> Permission *
        [parent in this.required]
    [maxRoles => #role < maxRoles]
    [all r:role|required in r.permission]
    [maxSessions => (all sna:Snapshot|(one p_s:Permission_Snapshot|p_s.perm = this && p_s.snap = sna && #p_s.sess < maxSessions))]

Permission_Snapshot * //Hepler clafer, used to implement set comprehensions in constraints that quantifies over all pairs of Permission-Snapshot.
    perm -> Permission
    snap -> Snapshot
    sess -> Session *
	[this in perm.role.session && this.user.snapshot = snap]
    [all s:Session|(s in perm.role.session && s.user.snapshot = snap) => s in sess]

abstract Action
    name : string 
    access -> Access *
        [parent in this.action]
    mutuallyExclusiveA -> MutuallyExclusiveActions *
        [parent in this.roleA]
    mutuallyExclusiveB -> MutuallyExclusiveActions *
        [parent in this.roleB]
    permission -> Permission *
        [parent in this.action]
    resource -> Resource *
        [parent in this.action]

abstract Resource
    name : string 
    resourceBasedDynamicSeparationOfDuty ?
    historyBasedDynamicSeparationOfDuty ?
    access -> Access *
        [parent in this.resource]
    action -> Action *
        [parent in this.resource]
    permission -> Permission *
        [parent in this.resource]

abstract Session
    id : string 
    user -> User 
        [parent in this.session]
    role -> Role *
        [parent in this.session]
    access -> Access *
        [parent in this.session]
	neededPermissions -> Permission *
	    [this in parent.action.permission && this.resource = parent.resource]
	[all p:Permission|(p in this.action.permission && p.resource = this.resource) => p in neededPermissions]
    pred -> Session ?
        [parent in this.succ]
    succ -> Session ?
        [parent in this.pred]
    [user.role in (user.role ++ user.role.junior)]
    [all a:access|some a.neededPermissions && a.neededPermissions in (role.permission ++ role.junior.permission)]
    [this not in succ && (some s:Snapshot| (Snapshot -- s) in s.succ)]
    [succ => succ.user = user.succ]
    [succ => succ.id.ref = id.ref]				
	
abstract Access
    id : string 
    session -> Session 
        [parent in this.access]
    action -> Action 
        [parent in this.access]
    resource -> Resource 
        [parent in this.access]
    pred -> Access ?
        [parent in this.succ]
    succ -> Access ?
        [parent in this.pred]
    [succ => succ.session = session.succ]
    [succ => succ.id.ref = id.ref]

abstract PrerequisiteActions
    wrtResource ?
    wrtResourceAndUser ?
    required -> Action *
    dependent -> Action *

/*
abstract PrerequisiteActions_Resource *
    prerquis -> PrerequisiteActions
    resc -> Resource
    tempSet1 -> Access *
	[this in prerquis.dependent.access && this.resource = resc]
    [all a:Access|(a in prerquis.dependent.access && a.resource = resc) => a in tempSet1]
*/

abstract MutuallyExclusive
    id : string 
    wrtUserAssignment ?
    identicalSeniorAllowed ?
    wrtPermissionAssignment ?
    wrtActiveRoles ?
    wrtJuniors ?
    wrtSeniors ?
    roleA -> Role 
        [parent in this.mutuallyExclusiveA]
    roleB -> Role 
        [parent in this.mutuallyExclusiveB]
    [wrtUserAssignment || wrtPermissionAssignment || wrtActiveRoles|| wrtJuniors || wrtSeniors]
    [roleA != roleB]

abstract MutuallyExclusiveActions
    id : string 
    wrtResourceAndUser ?
    roleA -> Action 
        [parent in this.mutuallyExclusiveA]
    roleB -> Action 
        [parent in this.mutuallyExclusiveB]
    

abstract Snapshot
    pred -> Snapshot ?
        [parent in this.succ]
    succ -> Snapshot ?
        [parent in this.pred]
    user -> User *
        [parent in this.snapshot]