Information Technology Reference
In-Depth Information
•
(
EC3
)
HoldsAt
(
f,t
2
) ←
Happens
(
a,t
1
) &
Initiates
(
a,f,t
1
) &
t
1
<
t
2
& ¬
Clipped
(
t
1
,
f,t
2
)
•
(
EC4
) ¬
HoldsAt
(
f,t
2
) ←
Happens
(
a
,
t
1
) &
Terminates
(
a
,
f,t
1
) &
t
1
<
t
2
&
¬
Declipped
(
t
1
,
f,t
2
)
•
(EC5)
HoldsAt
(
f, t
) ←
InitiallyTrue
(
f
) & ¬
Clipped
(0,
f,t
)
•
(EC6) ¬
HoldsAt
(
f,t
) ←
InitiallyFalse
(
f
) & ¬
Declipped
(0,
f,t
)
•
(EC7)
InitiallyTrue
(
f
) |
InitiallyFalse
(
f
)
Let us consider a typical example of authorization conflict, which arises when user
is assigned to two roles that have opposite authorization permissions.
The following predicates are introduced: (1)
User
(<
name
>) denotes a user with a
name <
name
>, (2)
Action
(<
name
>) defines an action with a name <
name
> that a user
(subject) can process on a target, (3)
Role
(<
name
>) determines a role with the name
<
name
>, (4)
ContradictoryRoles
(<
role1
>, <
role2
>, <
time
>, <
action
>) describes that
roles
role1
and
role2
have opposite (negative and positive) permissions for processing
an action <
action
> at a time point
t
.
The following events are used: (1)
AssignUserRole
(<
user
>,<
role
>) denotes a
request of a user <
user
> for assignment to a role <
role
>, (2)
RolePermitAction
(<
role
>,<
action
>) specifies a request for permission of an action
<
action
> for a role <
role
>, (3)
RoleDenyAction
(<
role
>,<
action
>) defines a request
for denial of action <
action
> for a role <
role
>.
The following fluents are assumed: (1)
Assigned
(<
user
>,<
role
>) specifies that user
<
user
> is assigned to a role <
role
>, (2)
RoleHavePermission
(<
role
>, <
action
>)
defines that a role <
role
> is permitted to a process action <
action
>, (3)
horizationConflict
(<
role1
>,<
role2
>) denotes that there is an authorization conflict in
the system, i.e. there exist a user who is assigned to contradictory roles.
Domain dependent axioms are as follows:
•
The first axiom initiates
RoleHavePermission
(
r,a
) fluent when the
RolePermitAction
(
r, a
) event happens if this fluent is currently not true:
(
AC1
)
Initiates
(
RoleHavePermission
(
r, a
),
RolePermitAction
(
r, a
),
t
) ←
Happens
(
RolePermitAction
(
r, a
),
t
) & (¬
HoldsAt
(
RoleHavePermission
(
r, a
),
t
)) ;
•
The second axiom implements deny for role
r
to process the action
a
as a
termination of fluent
RoleHavePermission
(
r, a
) when
RoleDenyActivity
(
r, a
) event
happens:
(
AC2
)
Terminates
(
RoleHavePermission
(
r, a
),
RoleDenyActivity
(
r, a
),
t
) ←
Happens
(
RoleDenyActivity
(
r, a
),
t
) &
HoldsAt
(
RoleHavePermission
(
r, a
),
t
) ;
•
The third axiom assigns user
u
to the role
r
when
AssignUserRole
(
u, r
) event
happens if
AuthorizationConflict
(
r, r0
) between the role
r
and some other role
r0
is not presented in the system:
(
AC3
)
Initiates
(
Assigned
(
u, r
),
AssignUserRole
(
u, r
),
t
) ←
Happens
(
AssignUserRole
(
u, r
),
t
) & (¬
HoldsAt
(
AuthorizationConflict
(
r, r0
),
t
)) ;
•
The fourth axiom defines two roles, one of which has and another one does not
have permission for some action. Here we note that OR-statement allows to not fix
which role has positive permission and which role has negative permission. Thus,
ContradictoryRoles is symmetrical regarding r1 and r2.
(
AC4
)
ContradictoryRoles
(
r1, r2, t, a
) ← (
HoldsAt
(
RoleHavePermission
(
r1, a
),
t
) & (¬
HoldsAt
(
RoleHavePermission
(
r2, a
),
t
))) | (
HoldsAt
(
RoleHavePermission
(
r2, a
),
t
) & (¬
HoldsAt
(
RoleHavePermission
(
r1, a
),
t
))) ;
