102 lines
5.8 KiB
Plaintext
102 lines
5.8 KiB
Plaintext
section signature:
|
|
|
|
user_to_role : user * role -> fact
|
|
poto : userORrole * taskName -> fact
|
|
task_to_data : taskName * set * set -> fact
|
|
aknows : entity * data -> fact
|
|
mc_pair : data * data -> data
|
|
contains : set * data -> fact
|
|
task : taskName * nat -> taskInstance
|
|
canExecute : user * role * humanTaskName -> fact
|
|
granted : user * role * taskInstance -> fact
|
|
executed : user * taskInstance -> fact
|
|
ready : taskInstance -> fact
|
|
done : taskInstance -> fact
|
|
entity > organization
|
|
entity > user
|
|
data > object
|
|
data > set
|
|
userORrole > user
|
|
userORrole > role
|
|
taskName > automatedTaskName
|
|
taskName > humanTaskName
|
|
|
|
section types:
|
|
|
|
parallelgateway1_to_usertask7,parallelgateway1_to_servicetask3,parallelgateway2_to_servicetask4,start_event_startevent2: fact
|
|
HT,usertask1,usertask2,usertask3,usertask4,usertask5,usertask6,usertask7,usertask8,usertask9: humanTaskName
|
|
IN,OUT,in_usertask1,out_usertask1,in_servicetask1,out_servicetask1,in_usertask2,out_usertask2,in_servicetask2,out_servicetask2,in_usertask3,out_usertask3,in_usertask4,out_usertask4,in_usertask5,out_usertask5,in_usertask6,out_usertask6,in_usertask7,out_usertask7,in_servicetask3,out_servicetask3,in_servicetask4,out_servicetask4,in_usertask8,out_usertask8,in_usertask9,out_usertask9,in_servicetask5,out_servicetask5: set
|
|
manager,supervisor,clerk,R: role
|
|
N,N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10,N11,N12,N13,N14,N15,N16,N17,N18,N19,N20,N21,N22,N23,N24,N25,N26,N27,N28,N29,N30,N31,N32,N33,N34: nat
|
|
AT,servicetask1,servicetask2,servicetask3,servicetask4,servicetask5: automatedTaskName
|
|
user1_manager,user2_manager,user1_supervisor,user2_supervisor,user1_clerk,user2_clerk,A,U0,U1: user
|
|
|
|
section inits:
|
|
|
|
initial_state init_1 :=
|
|
|
|
user_to_role(user1_manager,manager).
|
|
user_to_role(user2_manager,manager).
|
|
user_to_role(user1_supervisor,supervisor).
|
|
user_to_role(user2_supervisor,supervisor).
|
|
user_to_role(user1_clerk,clerk).
|
|
user_to_role(user2_clerk,clerk).
|
|
task_to_data(usertask1,in_usertask1,out_usertask1).
|
|
task_to_data(servicetask1,in_servicetask1,out_servicetask1).
|
|
task_to_data(usertask2,in_usertask2,out_usertask2).
|
|
task_to_data(servicetask2,in_servicetask2,out_servicetask2).
|
|
task_to_data(usertask3,in_usertask3,out_usertask3).
|
|
task_to_data(usertask4,in_usertask4,out_usertask4).
|
|
task_to_data(usertask5,in_usertask5,out_usertask5).
|
|
task_to_data(usertask6,in_usertask6,out_usertask6).
|
|
task_to_data(usertask7,in_usertask7,out_usertask7).
|
|
task_to_data(servicetask3,in_servicetask3,out_servicetask3).
|
|
task_to_data(servicetask4,in_servicetask4,out_servicetask4).
|
|
task_to_data(usertask8,in_usertask8,out_usertask8).
|
|
task_to_data(usertask9,in_usertask9,out_usertask9).
|
|
task_to_data(servicetask5,in_servicetask5,out_servicetask5).
|
|
start_event_startevent2
|
|
|
|
section hornClauses:
|
|
|
|
hc rbac_ac (A,R,HT) := canExecute(A,R,HT) :- user_to_role(A,R), poto(R,HT)
|
|
hc direct_ac (A,R,HT) := canExecute(A,R,HT) :- user_to_role(A,R), poto(A,HT)
|
|
hc poto_usertask1:= poto(clerk,usertask1)
|
|
hc poto_usertask2:= poto(clerk,usertask2)
|
|
hc poto_usertask3:= poto(manager,usertask3)
|
|
hc poto_usertask4:= poto(manager,usertask4)
|
|
hc poto_usertask5:= poto(clerk,usertask5)
|
|
hc poto_usertask6:= poto(manager,usertask6)
|
|
hc poto_usertask7:= poto(clerk,usertask7)
|
|
hc poto_usertask8:= poto(supervisor,usertask8)
|
|
hc poto_usertask9:= poto(supervisor,usertask9)
|
|
|
|
section rules:
|
|
|
|
step authorizeTaskExecution(A,R,HT,N) := canExecute(A,R,HT). ready(task(HT,N)) => granted(A,R,task(HT,N))
|
|
step h_taskExecution(A,R,HT,N,IN,OUT) := granted(A,R,task(HT,N)). task_to_data(HT,IN,OUT) => executed(A,task(HT,N)). done(task(HT,N)). task_to_data(HT,IN,OUT). aknows(A,IN). aknows(A,OUT)
|
|
step atask_execution(AT,N,IN,OUT) := ready(task(AT,N)). task_to_data(AT,IN,OUT) => done(task(AT,N)). task_to_data(AT,IN,OUT)
|
|
step w_usertask1(N0) := start_event_startevent2=[exists N0] => ready(task(usertask1,N0))
|
|
step w_servicetask1(N2,N1) := done(task(usertask1,N2))=[exists N1] => ready(task(servicetask1,N1))
|
|
step w_usertask2(N4,N3) := done(task(servicetask1,N4))=[exists N3] => ready(task(usertask2,N3))
|
|
step w_servicetask2(N6,N5) := done(task(usertask2,N6))=[exists N5] => ready(task(servicetask2,N5))
|
|
step w_usertask3(N8,N7) := done(task(servicetask2,N8))=[exists N7] => ready(task(usertask3,N7))
|
|
step w_usertask4(N10,N9) := done(task(usertask3,N10))=[exists N9] => ready(task(usertask4,N9))
|
|
step w_usertask5(N12,N11) := done(task(usertask4,N12))=[exists N11] => ready(task(usertask5,N11))
|
|
step w_usertask6(N14,N13) := done(task(usertask5,N14))=[exists N13] => ready(task(usertask6,N13))
|
|
step w_parallelgateway1(N15) := done(task(usertask6,N15)) => parallelgateway1_to_usertask7. parallelgateway1_to_servicetask3
|
|
step w_usertask7(N16) := parallelgateway1_to_usertask7=[exists N16] => ready(task(usertask7,N16))
|
|
step w_servicetask3(N17) := parallelgateway1_to_servicetask3=[exists N17] => ready(task(servicetask3,N17))
|
|
step w_parallelgateway2(N18,N19) := done(task(usertask7,N18)). done(task(servicetask3,N19)) => parallelgateway2_to_servicetask4
|
|
step w_servicetask4(N20) := parallelgateway2_to_servicetask4=[exists N20] => ready(task(servicetask4,N20))
|
|
step w_usertask8(N22,N21) := done(task(servicetask4,N22))=[exists N21] => ready(task(usertask8,N21))
|
|
step w_usertask9(N24,N23) := done(task(usertask8,N24))=[exists N23] => ready(task(usertask9,N23))
|
|
step w_servicetask5(N26,N25) := done(task(usertask9,N26))=[exists N25] => ready(task(servicetask5,N25))
|
|
|
|
section goals:
|
|
|
|
attack_state sod_securitySod1_1(U0,N27,N28):= executed(U0,task(usertask9,N27)). executed(U0,task(usertask2,N28))
|
|
attack_state sod_securitySod2_1(U0,N29,N30):= executed(U0,task(usertask4,N29)). executed(U0,task(usertask3,N30))
|
|
attack_state bod_securityBod1_1(U0,U1,N31,N32):= executed(U0,task(usertask8,N31)). executed(U1,task(usertask9,N32))& not(equal(U0,U1))
|
|
attack_state bod_securityBod1_2(U0,U1,N33,N34):= executed(U0,task(usertask9,N33)). executed(U1,task(usertask8,N34))& not(equal(U0,U1))
|