490 lines
45 KiB
Plaintext
490 lines
45 KiB
Plaintext
chapter {* Analysing DenningSacco *}
|
|
(* ***********************************
|
|
This file is automatically generated from the AnB file "AnB/Denning-Sacco.AnB".
|
|
Backend: Open Source Fixedpoint Model Checker version 2009c
|
|
************************************ *)
|
|
|
|
theory
|
|
"Denning-Sacco"
|
|
imports
|
|
"../src/ofmc"
|
|
begin
|
|
|
|
|
|
|
|
section {* Protocol Model (DenningSacco) *}
|
|
datatype Role = rA | rB | rs
|
|
|
|
datatype Purpose = purposeNI | purposeT | purposetimestamp | purposePayload
|
|
datatype Agent = honest nat
|
|
| dishonest nat
|
|
|
|
datatype Nonce = "ni" "nat"
|
|
| "timestamp" "nat"
|
|
| "payload" "Msg" "nat"
|
|
| "NI"
|
|
| "T"
|
|
| "Payload"
|
|
and Msg = Nonce "Nonce"
|
|
| Agent "Agent"
|
|
| Purpose "Purpose"
|
|
| pair "Msg*Msg"
|
|
| scrypt "Msg*Msg"
|
|
| crypt "Msg*Msg"
|
|
| inv "Msg"
|
|
| SID "nat"
|
|
| Step "nat"
|
|
| authentication
|
|
| secrecy
|
|
(* SymKeys *)
|
|
| SymKey "Msg"
|
|
| "sk" "Msg" "nat"
|
|
(* Functions *)
|
|
|
|
datatype Fact = Iknows Msg
|
|
| State "Role * (Msg list)"
|
|
| Secret "Msg * Msg"
|
|
| Attack "Msg"
|
|
| Witness "Msg * Msg * Msg * Msg"
|
|
| Request "Msg * Msg * Msg * Msg * Msg"
|
|
|
|
|
|
|
|
|
|
section {* Inductive Protocol Definition (DenningSacco) *}
|
|
inductive_set
|
|
DenningSacco::"Fact list set"
|
|
where
|
|
init_0: "[ Iknows(Nonce((ni Abs_NI)))] : DenningSacco"
|
|
| init_1: "[ Iknows(Agent(dishonest(i)))] : DenningSacco"
|
|
| init_2: "[ State(rA, [Agent(honest(a)), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), Agent(dishonest(i)), SID(sid)] )] : DenningSacco"
|
|
| init_3: "[ State(rA, [Agent(honest(a)), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), Agent(honest(a)), SID(sid)] )] : DenningSacco"
|
|
| init_4: "[ Iknows(Step(0))] : DenningSacco"
|
|
| init_5: "[ Iknows(Nonce((timestamp Abs_T)))] : DenningSacco"
|
|
| init_6: "[ Iknows(SymKey((sk(pair(Agent(dishonest(i)), Agent(honest(a)))) Abs_KAB)))] : DenningSacco"
|
|
| init_7: "[ Iknows(SID(sid))] : DenningSacco"
|
|
| init_8: "[ Iknows(Agent(honest(a)))] : DenningSacco"
|
|
| init_9: "[ State(rB, [Agent(honest(a)), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), Agent(dishonest(i)), SID(sid)] )] : DenningSacco"
|
|
| init_10: "[ State(rB, [Agent(honest(a)), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), Agent(honest(a)), SID(sid)] )] : DenningSacco"
|
|
| init_11: "[ State(rs, [Agent(honest(a)), Step(0), SymKey((sk(pair(Agent(dishonest(i)), Agent(honest(a)))) Abs_KAB)), SymKey((sk(pair(Agent(dishonest(i)), Agent(honest(a)))) Abs_KAB)), Agent(dishonest(i)), Agent(dishonest(i)), SID(sid)] )] : DenningSacco"
|
|
| init_12: "[ State(rs, [Agent(honest(a)), Step(0), SymKey((sk(pair(Agent(dishonest(i)), Agent(honest(a)))) Abs_KAB)), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), Agent(dishonest(i)), Agent(honest(a)), SID(sid)] )] : DenningSacco"
|
|
| init_13: "[ State(rs, [Agent(honest(a)), Step(0), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), SymKey((sk(pair(Agent(dishonest(i)), Agent(honest(a)))) Abs_KAB)), Agent(honest(a)), Agent(dishonest(i)), SID(sid)] )] : DenningSacco"
|
|
| init_14: "[ State(rs, [Agent(honest(a)), Step(0), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), Agent(honest(a)), Agent(honest(a)), SID(sid)] )] : DenningSacco"
|
|
| rule_0: "[| t :DenningSacco;
|
|
Iknows(crypt(K, M)) : (set t);
|
|
Iknows(inv(K)) : (set t)|]
|
|
==>
|
|
((Iknows(M))
|
|
#t) : DenningSacco"
|
|
| rule_1: "[| t :DenningSacco;
|
|
Iknows(crypt(inv(K), M)) : (set t);
|
|
Iknows(K) : (set t)|]
|
|
==>
|
|
((Iknows(M))
|
|
#t) : DenningSacco"
|
|
| rule_2: "[| t :DenningSacco;
|
|
Iknows(scrypt(K, M)) : (set t);
|
|
Iknows(K) : (set t)|]
|
|
==>
|
|
((Iknows(M))
|
|
#t) : DenningSacco"
|
|
| rule_3: "[| t :DenningSacco;
|
|
Iknows(pair(M1, M2)) : (set t)|]
|
|
==>
|
|
((Iknows(M1))
|
|
#(Iknows(M2))
|
|
#t) : DenningSacco"
|
|
| rule_4: "[| t :DenningSacco;
|
|
Secret(M, Agent(honest(a))) : (set t);
|
|
Iknows(M) : (set t)|]
|
|
==>
|
|
((Attack(pair(secrecy, M)))
|
|
#t) : DenningSacco"
|
|
| rule_5: "[| t :DenningSacco;
|
|
Request(A, B, Purpose(purposePayload), M, SID(sid)) : (set t);
|
|
~ ( ? i .
|
|
B = Agent(dishonest(i)));
|
|
~ ( ? B A Abs_Payload .
|
|
M = Nonce((payload(pair(B, A)) Abs_Payload)))|]
|
|
==>
|
|
((Attack(pair(authentication, pair(A, pair(B, M)))))
|
|
#t) : DenningSacco"
|
|
| rule_6: "[| t :DenningSacco;
|
|
Request(A, B, Purpose(purposeKAB), M, SID(sid)) : (set t);
|
|
~ ( ? i .
|
|
B = Agent(dishonest(i)));
|
|
~ ( ? B A Abs_KAB .
|
|
M = SymKey((sk(pair(B, A)) Abs_KAB)))|]
|
|
==>
|
|
((Attack(pair(authentication, pair(A, pair(B, M)))))
|
|
#t) : DenningSacco"
|
|
| rule_7: "[| t :DenningSacco;
|
|
State(rA, [Agent(A), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), SID(sid)] ) : (set t)|]
|
|
==>
|
|
((State(rA, [Agent(A), Step(1), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), SID(sid)] ))
|
|
#(Iknows(pair(Agent(A), Agent(B))))
|
|
#t) : DenningSacco"
|
|
| rule_8: "[| t :DenningSacco;
|
|
State(rs, [Agent(honest(a)), Step(0), SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), Agent(A), SID(sid)] ) : (set t);
|
|
Iknows(Agent(A)) : (set t);
|
|
Iknows(Agent(B)) : (set t)|]
|
|
==>
|
|
((State(rs, [Agent(honest(a)), Step(1), SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), Agent(A), pair(Agent(A), Agent(B)), SymKey((sk(pair(Agent(A), Agent(B))) Abs_KAB)), Nonce((timestamp Abs_T)), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey((sk(pair(Agent(A), Agent(B))) Abs_KAB)), pair(Nonce((timestamp Abs_T)), scrypt(SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), pair(Agent(A), pair(SymKey((sk(pair(Agent(A), Agent(B))) Abs_KAB)), Nonce((timestamp Abs_T))))))))), SID(sid)] ))
|
|
#(Iknows(scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey((sk(pair(Agent(A), Agent(B))) Abs_KAB)), pair(Nonce((timestamp Abs_T)), scrypt(SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), pair(Agent(A), pair(SymKey((sk(pair(Agent(A), Agent(B))) Abs_KAB)), Nonce((timestamp Abs_T)))))))))))
|
|
#t) : DenningSacco"
|
|
| rule_9: "[| t :DenningSacco;
|
|
State(rA, [Agent(A), Step(1), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), SID(sid)] ) : (set t);
|
|
Iknows(scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i))))))) : (set t)|]
|
|
==>
|
|
((State(rA, [Agent(A), Step(2), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), Agent(dishonest(i)), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i)))))), SID(sid)] ))
|
|
#(Iknows(Agent(dishonest(i))))
|
|
#t) : DenningSacco"
|
|
| rule_10: "[| t :DenningSacco;
|
|
State(rA, [Agent(A), Step(1), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), SID(sid)] ) : (set t);
|
|
Iknows(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB))) : (set t);
|
|
Iknows(Agent(B)) : (set t);
|
|
Iknows(SymKey(KAB)) : (set t);
|
|
Iknows(Nonce(T)) : (set t);
|
|
Iknows(Agent(dishonest(i))) : (set t)|]
|
|
==>
|
|
((State(rA, [Agent(A), Step(2), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), Agent(dishonest(i)), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i)))))), SID(sid)] ))
|
|
#(Iknows(Agent(dishonest(i))))
|
|
#t) : DenningSacco"
|
|
| rule_11: "[| t :DenningSacco;
|
|
State(rB, [Agent(B), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), Agent(A), SID(sid)] ) : (set t);
|
|
Iknows(scrypt(SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), pair(Agent(A), pair(SymKey(KAB), Nonce(T))))) : (set t)|]
|
|
==>
|
|
((Secret(Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload)), Agent(A)))
|
|
#(Witness(Agent(B), Agent(A), Purpose(purposePayload), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload))))
|
|
#(State(rB, [Agent(B), Step(1), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), Agent(A), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), pair(Agent(A), pair(SymKey(KAB), Nonce(T)))), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload)), scrypt(SymKey(KAB), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload))), SID(sid)] ))
|
|
#(Iknows(scrypt(SymKey(KAB), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload)))))
|
|
#t) : DenningSacco"
|
|
| rule_12: "[| t :DenningSacco;
|
|
State(rB, [Agent(B), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), Agent(A), SID(sid)] ) : (set t);
|
|
Iknows(SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB))) : (set t);
|
|
Iknows(Agent(A)) : (set t);
|
|
Iknows(SymKey(KAB)) : (set t);
|
|
Iknows(Nonce(T)) : (set t)|]
|
|
==>
|
|
((Secret(Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload)), Agent(A)))
|
|
#(Witness(Agent(B), Agent(A), Purpose(purposePayload), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload))))
|
|
#(State(rB, [Agent(B), Step(1), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), Agent(A), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), pair(Agent(A), pair(SymKey(KAB), Nonce(T)))), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload)), scrypt(SymKey(KAB), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload))), SID(sid)] ))
|
|
#(Iknows(scrypt(SymKey(KAB), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload)))))
|
|
#t) : DenningSacco"
|
|
| rule_13: "[| t :DenningSacco;
|
|
State(rA, [Agent(A), Step(2), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), Agent(dishonest(i)), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i)))))), SID(sid)] ) : (set t);
|
|
Iknows(scrypt(SymKey(KAB), Nonce(Payload))) : (set t)|]
|
|
==>
|
|
((Request(Agent(A), Agent(B), Purpose(purposePayload), Nonce(Payload), SID(sid)))
|
|
#(State(rA, [Agent(A), Step(3), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), Agent(dishonest(i)), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i)))))), Nonce(Payload), scrypt(SymKey(KAB), Nonce(Payload)), SID(sid)] ))
|
|
#t) : DenningSacco"
|
|
| rule_14: "[| t :DenningSacco;
|
|
State(rA, [Agent(A), Step(2), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), Agent(dishonest(i)), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i)))))), SID(sid)] ) : (set t);
|
|
Iknows(SymKey(KAB)) : (set t);
|
|
Iknows(Nonce(Payload)) : (set t)|]
|
|
==>
|
|
((Request(Agent(A), Agent(B), Purpose(purposePayload), Nonce(Payload), SID(sid)))
|
|
#(State(rA, [Agent(A), Step(3), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), Agent(dishonest(i)), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i)))))), Nonce(Payload), scrypt(SymKey(KAB), Nonce(Payload)), SID(sid)] ))
|
|
#t) : DenningSacco"
|
|
|
|
|
|
section {* Fixed-point Definition (DenningSacco) *}
|
|
definition
|
|
"DenningSacco_fp = {m. ( ? Abs_NI0 i8 i9 i10 i11 i12 i13 i14 i15 a10 a11 a12 a13 a14 a15 a16 a17 Abs_KAB5 a18 a19 a20 Abs_KAB6 i7 a5 a6 Abs_KAB3 Abs_T2 a7 a8 Abs_KAB4 a9 Abs_Payload1 sid0 Abs_Payload0 i3 i4 i5 i6 a0 a1 a2 a3 Abs_KAB1 a4 Abs_KAB2 Abs_T1 i0 i1 i2 Abs_KAB0 Abs_T0 .
|
|
(m = Iknows(Nonce((ni Abs_NI0))))
|
|
| (m = Iknows(Agent(dishonest(i0))))
|
|
| (m = State(rA, [Agent(honest(a0)), Step(0), Nonce((timestamp Abs_T0)), SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB0)), Agent(dishonest(i0)), SID(sid0)] ))
|
|
| (m = State(rA, [Agent(honest(a0)), Step(0), Nonce((timestamp Abs_T0)), SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB0)), Agent(honest(a3)), SID(sid0)] ))
|
|
| (m = Iknows(Step(0)))
|
|
| (m = Iknows(Nonce((timestamp Abs_T0))))
|
|
| (m = Iknows(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0))))
|
|
| (m = Iknows(SID(sid0)))
|
|
| (m = Iknows(Agent(honest(a0))))
|
|
| (m = State(rB, [Agent(honest(a0)), Step(0), Nonce((timestamp Abs_T0)), SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB0)), Agent(dishonest(i0)), SID(sid0)] ))
|
|
| (m = State(rB, [Agent(honest(a0)), Step(0), Nonce((timestamp Abs_T0)), SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB0)), Agent(honest(a3)), SID(sid0)] ))
|
|
| (m = State(rs, [Agent(honest(a0)), Step(0), SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a1)))) Abs_KAB0)), SymKey((sk(pair(Agent(dishonest(i1)), Agent(honest(a2)))) Abs_KAB1)), Agent(dishonest(i2)), Agent(dishonest(i3)), SID(sid0)] ))
|
|
| (m = State(rs, [Agent(honest(a0)), Step(0), SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a1)))) Abs_KAB0)), SymKey((sk(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_KAB1)), Agent(dishonest(i1)), Agent(honest(a4)), SID(sid0)] ))
|
|
| (m = State(rs, [Agent(honest(a0)), Step(0), SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB0)), SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a3)))) Abs_KAB1)), Agent(honest(a4)), Agent(dishonest(i1)), SID(sid0)] ))
|
|
| (m = State(rs, [Agent(honest(a0)), Step(0), SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB0)), SymKey((sk(pair(Agent(honest(a3)), Agent(honest(a4)))) Abs_KAB1)), Agent(honest(a5)), Agent(honest(a6)), SID(sid0)] ))
|
|
| (m = Iknows(pair(Agent(honest(a0)), Agent(honest(a1)))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), Agent(dishonest(i0)))))
|
|
| (m = State(rA, [Agent(honest(a0)), Step(1), Nonce((timestamp Abs_T0)), SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB0)), Agent(dishonest(i0)), pair(Agent(honest(a3)), Agent(dishonest(i1))), SID(sid0)] ))
|
|
| (m = State(rA, [Agent(honest(a0)), Step(1), Nonce((timestamp Abs_T0)), SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB0)), Agent(honest(a3)), pair(Agent(honest(a4)), Agent(honest(a5))), SID(sid0)] ))
|
|
| (m = State(rs, [Agent(honest(a0)), Step(1), SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a1)))) Abs_KAB0)), SymKey((sk(pair(Agent(dishonest(i1)), Agent(honest(a2)))) Abs_KAB1)), Agent(dishonest(i2)), Agent(dishonest(i3)), pair(Agent(dishonest(i4)), Agent(dishonest(i5))), SymKey((sk(pair(Agent(dishonest(i6)), Agent(dishonest(i7)))) Abs_KAB2)), Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i8)), Agent(honest(a3)))) Abs_KAB3)), pair(Agent(dishonest(i9)), pair(SymKey((sk(pair(Agent(dishonest(i10)), Agent(dishonest(i11)))) Abs_KAB4)), pair(Nonce((timestamp Abs_T1)), scrypt(SymKey((sk(pair(Agent(dishonest(i12)), Agent(honest(a4)))) Abs_KAB5)), pair(Agent(dishonest(i13)), pair(SymKey((sk(pair(Agent(dishonest(i14)), Agent(dishonest(i15)))) Abs_KAB6)), Nonce((timestamp Abs_T2))))))))), SID(sid0)] ))
|
|
| (m = State(rs, [Agent(honest(a0)), Step(1), SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a1)))) Abs_KAB0)), SymKey((sk(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_KAB1)), Agent(dishonest(i1)), Agent(honest(a4)), pair(Agent(honest(a5)), Agent(dishonest(i2))), SymKey((sk(pair(Agent(honest(a6)), Agent(dishonest(i3)))) Abs_KAB2)), Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a7)), Agent(honest(a8)))) Abs_KAB3)), pair(Agent(dishonest(i4)), pair(SymKey((sk(pair(Agent(honest(a9)), Agent(dishonest(i5)))) Abs_KAB4)), pair(Nonce((timestamp Abs_T1)), scrypt(SymKey((sk(pair(Agent(dishonest(i6)), Agent(honest(a10)))) Abs_KAB5)), pair(Agent(honest(a11)), pair(SymKey((sk(pair(Agent(honest(a12)), Agent(dishonest(i7)))) Abs_KAB6)), Nonce((timestamp Abs_T2))))))))), SID(sid0)] ))
|
|
| (m = State(rs, [Agent(honest(a0)), Step(1), SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB0)), SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a3)))) Abs_KAB1)), Agent(honest(a4)), Agent(dishonest(i1)), pair(Agent(dishonest(i2)), Agent(honest(a5))), SymKey((sk(pair(Agent(dishonest(i3)), Agent(honest(a6)))) Abs_KAB2)), Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i4)), Agent(honest(a7)))) Abs_KAB3)), pair(Agent(honest(a8)), pair(SymKey((sk(pair(Agent(dishonest(i5)), Agent(honest(a9)))) Abs_KAB4)), pair(Nonce((timestamp Abs_T1)), scrypt(SymKey((sk(pair(Agent(honest(a10)), Agent(honest(a11)))) Abs_KAB5)), pair(Agent(dishonest(i6)), pair(SymKey((sk(pair(Agent(dishonest(i7)), Agent(honest(a12)))) Abs_KAB6)), Nonce((timestamp Abs_T2))))))))), SID(sid0)] ))
|
|
| (m = State(rs, [Agent(honest(a0)), Step(1), SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB0)), SymKey((sk(pair(Agent(honest(a3)), Agent(honest(a4)))) Abs_KAB1)), Agent(honest(a5)), Agent(honest(a6)), pair(Agent(honest(a7)), Agent(honest(a8))), SymKey((sk(pair(Agent(honest(a9)), Agent(honest(a10)))) Abs_KAB2)), Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a11)), Agent(honest(a12)))) Abs_KAB3)), pair(Agent(honest(a13)), pair(SymKey((sk(pair(Agent(honest(a14)), Agent(honest(a15)))) Abs_KAB4)), pair(Nonce((timestamp Abs_T1)), scrypt(SymKey((sk(pair(Agent(honest(a16)), Agent(honest(a17)))) Abs_KAB5)), pair(Agent(honest(a18)), pair(SymKey((sk(pair(Agent(honest(a19)), Agent(honest(a20)))) Abs_KAB6)), Nonce((timestamp Abs_T2))))))))), SID(sid0)] ))
|
|
| (m = Iknows(scrypt(SymKey((sk(pair(Agent(honest(a0)), Agent(honest(a1)))) Abs_KAB0)), pair(Agent(honest(a2)), pair(SymKey((sk(pair(Agent(honest(a3)), Agent(honest(a4)))) Abs_KAB1)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a5)), Agent(honest(a6)))) Abs_KAB2)), pair(Agent(honest(a7)), pair(SymKey((sk(pair(Agent(honest(a8)), Agent(honest(a9)))) Abs_KAB3)), Nonce((timestamp Abs_T1)))))))))))
|
|
| (m = Iknows(scrypt(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0)), pair(Agent(honest(a1)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(honest(a2)))) Abs_KAB1)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a3)), Agent(honest(a4)))) Abs_KAB2)), pair(Agent(dishonest(i2)), pair(SymKey((sk(pair(Agent(dishonest(i3)), Agent(honest(a5)))) Abs_KAB3)), Nonce((timestamp Abs_T1)))))))))))
|
|
| (m = Iknows(scrypt(SymKey((sk(pair(Agent(honest(a0)), Agent(honest(a1)))) Abs_KAB0)), pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(honest(a2)), Agent(dishonest(i1)))) Abs_KAB1)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a3)))) Abs_KAB2)), pair(Agent(honest(a4)), pair(SymKey((sk(pair(Agent(honest(a5)), Agent(dishonest(i3)))) Abs_KAB3)), Nonce((timestamp Abs_T1)))))))))))
|
|
| (m = Iknows(scrypt(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(dishonest(i3)))) Abs_KAB1)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i4)), Agent(honest(a1)))) Abs_KAB2)), pair(Agent(dishonest(i5)), pair(SymKey((sk(pair(Agent(dishonest(i6)), Agent(dishonest(i7)))) Abs_KAB3)), Nonce((timestamp Abs_T1)))))))))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), Agent(honest(a1)))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), Agent(dishonest(i0)))))
|
|
| (m = Iknows(pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(dishonest(i3)))) Abs_KAB1)), Nonce((timestamp Abs_T1))))))))
|
|
| (m = Iknows(pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(dishonest(i1)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a0)))) Abs_KAB1)), pair(Agent(dishonest(i3)), pair(SymKey((sk(pair(Agent(dishonest(i4)), Agent(dishonest(i5)))) Abs_KAB2)), Nonce((timestamp Abs_T1)))))))))
|
|
| (m = Iknows(pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(dishonest(i2)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i3)), Agent(honest(a0)))) Abs_KAB1)), pair(Agent(dishonest(i4)), pair(SymKey((sk(pair(Agent(dishonest(i5)), Agent(dishonest(i6)))) Abs_KAB2)), Nonce((timestamp Abs_T1))))))))))
|
|
| (m = Iknows(pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a0)), Agent(honest(a1)))) Abs_KAB0)), pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(honest(a2)))) Abs_KAB1)), Nonce((timestamp Abs_T1))))))))
|
|
| (m = Iknows(pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB1)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a3)))) Abs_KAB2)), Nonce((timestamp Abs_T1)))))))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a1)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_KAB1)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a4)))) Abs_KAB2)), Nonce((timestamp Abs_T1))))))))))
|
|
| (m = Iknows(scrypt(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(dishonest(i3)))) Abs_KAB1)), Nonce((timestamp Abs_T0)))))))
|
|
| (m = Iknows(SymKey((sk(pair(Agent(dishonest(i0)), Agent(dishonest(i1)))) Abs_KAB0))))
|
|
| (m = Iknows(scrypt(SymKey((sk(pair(Agent(honest(a0)), Agent(honest(a1)))) Abs_KAB0)), pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(honest(a2)))) Abs_KAB1)), Nonce((timestamp Abs_T0)))))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), Agent(honest(a1)))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), Agent(dishonest(i0)))))
|
|
| (m = Iknows(pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(dishonest(i3)))) Abs_KAB1)), Nonce((timestamp Abs_T1))))))))
|
|
| (m = Iknows(pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(dishonest(i1)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a0)))) Abs_KAB1)), pair(Agent(dishonest(i3)), pair(SymKey((sk(pair(Agent(dishonest(i4)), Agent(dishonest(i5)))) Abs_KAB2)), Nonce((timestamp Abs_T1)))))))))
|
|
| (m = Iknows(pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(dishonest(i2)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i3)), Agent(honest(a0)))) Abs_KAB1)), pair(Agent(dishonest(i4)), pair(SymKey((sk(pair(Agent(dishonest(i5)), Agent(dishonest(i6)))) Abs_KAB2)), Nonce((timestamp Abs_T1))))))))))
|
|
| (m = Iknows(pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a0)), Agent(honest(a1)))) Abs_KAB0)), pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(honest(a2)))) Abs_KAB1)), Nonce((timestamp Abs_T1))))))))
|
|
| (m = Iknows(pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB1)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a3)))) Abs_KAB2)), Nonce((timestamp Abs_T1)))))))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a1)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_KAB1)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a4)))) Abs_KAB2)), Nonce((timestamp Abs_T1))))))))))
|
|
| (m = Iknows(pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(dishonest(i1)))) Abs_KAB0)), Nonce((timestamp Abs_T0)))))
|
|
| (m = Iknows(pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(dishonest(i2)))) Abs_KAB0)), Nonce((timestamp Abs_T0))))))
|
|
| (m = Secret(Nonce((payload(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_Payload0)), Agent(dishonest(i1))))
|
|
| (m = Witness(Agent(honest(a0)), Agent(dishonest(i0)), Purpose(purposePayload), Nonce((payload(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_Payload0))))
|
|
| (m = State(rB, [Agent(honest(a0)), Step(1), Nonce((timestamp Abs_T0)), SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB0)), Agent(dishonest(i0)), Nonce((timestamp Abs_T1)), SymKey((sk(pair(Agent(dishonest(i1)), Agent(honest(a3)))) Abs_KAB1)), scrypt(SymKey((sk(pair(Agent(honest(a4)), Agent(honest(a5)))) Abs_KAB2)), pair(Agent(dishonest(i2)), pair(SymKey((sk(pair(Agent(dishonest(i3)), Agent(honest(a6)))) Abs_KAB3)), Nonce((timestamp Abs_T2))))), Nonce((payload(pair(Agent(honest(a7)), Agent(dishonest(i4)))) Abs_Payload0)), scrypt(SymKey((sk(pair(Agent(dishonest(i5)), Agent(honest(a8)))) Abs_KAB4)), Nonce((payload(pair(Agent(honest(a9)), Agent(dishonest(i6)))) Abs_Payload1))), SID(sid0)] ))
|
|
| (m = Iknows(scrypt(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0)), Nonce((payload(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_Payload0)))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), Agent(honest(a1)))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), Agent(dishonest(i0)))))
|
|
| (m = Iknows(pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(dishonest(i3)))) Abs_KAB1)), Nonce((timestamp Abs_T1))))))))
|
|
| (m = Iknows(pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(dishonest(i1)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a0)))) Abs_KAB1)), pair(Agent(dishonest(i3)), pair(SymKey((sk(pair(Agent(dishonest(i4)), Agent(dishonest(i5)))) Abs_KAB2)), Nonce((timestamp Abs_T1)))))))))
|
|
| (m = Iknows(pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(dishonest(i2)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i3)), Agent(honest(a0)))) Abs_KAB1)), pair(Agent(dishonest(i4)), pair(SymKey((sk(pair(Agent(dishonest(i5)), Agent(dishonest(i6)))) Abs_KAB2)), Nonce((timestamp Abs_T1))))))))))
|
|
| (m = Iknows(pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a0)), Agent(honest(a1)))) Abs_KAB0)), pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(honest(a2)))) Abs_KAB1)), Nonce((timestamp Abs_T1))))))))
|
|
| (m = Iknows(pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB1)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a3)))) Abs_KAB2)), Nonce((timestamp Abs_T1)))))))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a1)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_KAB1)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a4)))) Abs_KAB2)), Nonce((timestamp Abs_T1))))))))))
|
|
| (m = Iknows(pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(dishonest(i1)))) Abs_KAB0)), Nonce((timestamp Abs_T0)))))
|
|
| (m = Iknows(pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(dishonest(i2)))) Abs_KAB0)), Nonce((timestamp Abs_T0))))))
|
|
| (m = Iknows(Nonce((payload(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_Payload0))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), Agent(honest(a1)))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), Agent(dishonest(i0)))))
|
|
| (m = Iknows(pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(dishonest(i3)))) Abs_KAB1)), Nonce((timestamp Abs_T1))))))))
|
|
| (m = Iknows(pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(dishonest(i1)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a0)))) Abs_KAB1)), pair(Agent(dishonest(i3)), pair(SymKey((sk(pair(Agent(dishonest(i4)), Agent(dishonest(i5)))) Abs_KAB2)), Nonce((timestamp Abs_T1)))))))))
|
|
| (m = Iknows(pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(dishonest(i2)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(dishonest(i3)), Agent(honest(a0)))) Abs_KAB1)), pair(Agent(dishonest(i4)), pair(SymKey((sk(pair(Agent(dishonest(i5)), Agent(dishonest(i6)))) Abs_KAB2)), Nonce((timestamp Abs_T1))))))))))
|
|
| (m = Iknows(pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a0)), Agent(honest(a1)))) Abs_KAB0)), pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(honest(a2)))) Abs_KAB1)), Nonce((timestamp Abs_T1))))))))
|
|
| (m = Iknows(pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB1)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a3)))) Abs_KAB2)), Nonce((timestamp Abs_T1)))))))))
|
|
| (m = Iknows(pair(Agent(honest(a0)), pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(honest(a1)))) Abs_KAB0)), pair(Nonce((timestamp Abs_T0)), scrypt(SymKey((sk(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_KAB1)), pair(Agent(dishonest(i1)), pair(SymKey((sk(pair(Agent(dishonest(i2)), Agent(honest(a4)))) Abs_KAB2)), Nonce((timestamp Abs_T1))))))))))
|
|
| (m = Iknows(pair(SymKey((sk(pair(Agent(dishonest(i0)), Agent(dishonest(i1)))) Abs_KAB0)), Nonce((timestamp Abs_T0)))))
|
|
| (m = Iknows(pair(Agent(dishonest(i0)), pair(SymKey((sk(pair(Agent(dishonest(i1)), Agent(dishonest(i2)))) Abs_KAB0)), Nonce((timestamp Abs_T0))))))
|
|
)}"
|
|
|
|
|
|
section {* Checking Fixed-point (DenningSacco) *}
|
|
lemma fp_attack_free: "~ (Attack m : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_0: "Iknows(Nonce((ni Abs_NI))) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_1: "Iknows(Agent(dishonest(i))) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_2: "State(rA, [Agent(honest(a)), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), Agent(dishonest(i)), SID(sid)] ) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_3: "State(rA, [Agent(honest(a)), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), Agent(honest(a)), SID(sid)] ) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_4: "Iknows(Step(0)) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_5: "Iknows(Nonce((timestamp Abs_T))) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_6: "Iknows(SymKey((sk(pair(Agent(dishonest(i)), Agent(honest(a)))) Abs_KAB))) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_7: "Iknows(SID(sid)) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_8: "Iknows(Agent(honest(a))) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_9: "State(rB, [Agent(honest(a)), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), Agent(dishonest(i)), SID(sid)] ) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_10: "State(rB, [Agent(honest(a)), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), Agent(honest(a)), SID(sid)] ) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_11: "State(rs, [Agent(honest(a)), Step(0), SymKey((sk(pair(Agent(dishonest(i)), Agent(honest(a)))) Abs_KAB)), SymKey((sk(pair(Agent(dishonest(i)), Agent(honest(a)))) Abs_KAB)), Agent(dishonest(i)), Agent(dishonest(i)), SID(sid)] ) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_12: "State(rs, [Agent(honest(a)), Step(0), SymKey((sk(pair(Agent(dishonest(i)), Agent(honest(a)))) Abs_KAB)), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), Agent(dishonest(i)), Agent(honest(a)), SID(sid)] ) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_13: "State(rs, [Agent(honest(a)), Step(0), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), SymKey((sk(pair(Agent(dishonest(i)), Agent(honest(a)))) Abs_KAB)), Agent(honest(a)), Agent(dishonest(i)), SID(sid)] ) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma init_14: "State(rs, [Agent(honest(a)), Step(0), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), SymKey((sk(pair(Agent(honest(a)), Agent(honest(a)))) Abs_KAB)), Agent(honest(a)), Agent(honest(a)), SID(sid)] ) : DenningSacco_fp"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_0: "[|
|
|
Iknows(crypt(K, M)) : DenningSacco_fp;
|
|
Iknows(inv(K)) : DenningSacco_fp|]
|
|
==>
|
|
(Iknows(M) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_1: "[|
|
|
Iknows(crypt(inv(K), M)) : DenningSacco_fp;
|
|
Iknows(K) : DenningSacco_fp|]
|
|
==>
|
|
(Iknows(M) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_2: "[|
|
|
Iknows(scrypt(K, M)) : DenningSacco_fp;
|
|
Iknows(K) : DenningSacco_fp|]
|
|
==>
|
|
(Iknows(M) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_3: "[|
|
|
Iknows(pair(M1, M2)) : DenningSacco_fp|]
|
|
==>
|
|
(Iknows(M1) : DenningSacco_fp) &
|
|
(Iknows(M2) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_4: "[|
|
|
Secret(M, Agent(honest(a))) : DenningSacco_fp;
|
|
Iknows(M) : DenningSacco_fp|]
|
|
==>
|
|
(Attack(pair(secrecy, M)) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_5: "[|
|
|
Request(A, B, Purpose(purposePayload), M, SID(sid)) : DenningSacco_fp;
|
|
~ ( ? i .
|
|
B = Agent(dishonest(i)));
|
|
~ ( ? B A Abs_Payload .
|
|
M = Nonce((payload(pair(B, A)) Abs_Payload)))|]
|
|
==>
|
|
(Attack(pair(authentication, pair(A, pair(B, M)))) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_6: "[|
|
|
Request(A, B, Purpose(purposeKAB), M, SID(sid)) : DenningSacco_fp;
|
|
~ ( ? i .
|
|
B = Agent(dishonest(i)));
|
|
~ ( ? B A Abs_KAB .
|
|
M = SymKey((sk(pair(B, A)) Abs_KAB)))|]
|
|
==>
|
|
(Attack(pair(authentication, pair(A, pair(B, M)))) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_7: "[|
|
|
State(rA, [Agent(A), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), SID(sid)] ) : DenningSacco_fp|]
|
|
==>
|
|
(State(rA, [Agent(A), Step(1), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), SID(sid)] ) : DenningSacco_fp) &
|
|
(Iknows(pair(Agent(A), Agent(B))) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_8: "[|
|
|
State(rs, [Agent(honest(a)), Step(0), SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), Agent(A), SID(sid)] ) : DenningSacco_fp;
|
|
Iknows(Agent(A)) : DenningSacco_fp;
|
|
Iknows(Agent(B)) : DenningSacco_fp|]
|
|
==>
|
|
(State(rs, [Agent(honest(a)), Step(1), SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), Agent(A), pair(Agent(A), Agent(B)), SymKey((sk(pair(Agent(A), Agent(B))) Abs_KAB)), Nonce((timestamp Abs_T)), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey((sk(pair(Agent(A), Agent(B))) Abs_KAB)), pair(Nonce((timestamp Abs_T)), scrypt(SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), pair(Agent(A), pair(SymKey((sk(pair(Agent(A), Agent(B))) Abs_KAB)), Nonce((timestamp Abs_T))))))))), SID(sid)] ) : DenningSacco_fp) &
|
|
(Iknows(scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey((sk(pair(Agent(A), Agent(B))) Abs_KAB)), pair(Nonce((timestamp Abs_T)), scrypt(SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), pair(Agent(A), pair(SymKey((sk(pair(Agent(A), Agent(B))) Abs_KAB)), Nonce((timestamp Abs_T)))))))))) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_9: "[|
|
|
State(rA, [Agent(A), Step(1), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), SID(sid)] ) : DenningSacco_fp;
|
|
Iknows(scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i))))))) : DenningSacco_fp|]
|
|
==>
|
|
(State(rA, [Agent(A), Step(2), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), Agent(dishonest(i)), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i)))))), SID(sid)] ) : DenningSacco_fp) &
|
|
(Iknows(Agent(dishonest(i))) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_10: "[|
|
|
State(rA, [Agent(A), Step(1), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), SID(sid)] ) : DenningSacco_fp;
|
|
Iknows(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB))) : DenningSacco_fp;
|
|
Iknows(Agent(B)) : DenningSacco_fp;
|
|
Iknows(SymKey(KAB)) : DenningSacco_fp;
|
|
Iknows(Nonce(T)) : DenningSacco_fp;
|
|
Iknows(Agent(dishonest(i))) : DenningSacco_fp|]
|
|
==>
|
|
(State(rA, [Agent(A), Step(2), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), Agent(dishonest(i)), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i)))))), SID(sid)] ) : DenningSacco_fp) &
|
|
(Iknows(Agent(dishonest(i))) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_11: "[|
|
|
State(rB, [Agent(B), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), Agent(A), SID(sid)] ) : DenningSacco_fp;
|
|
Iknows(scrypt(SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), pair(Agent(A), pair(SymKey(KAB), Nonce(T))))) : DenningSacco_fp|]
|
|
==>
|
|
(Secret(Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload)), Agent(A)) : DenningSacco_fp) &
|
|
(Witness(Agent(B), Agent(A), Purpose(purposePayload), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload))) : DenningSacco_fp) &
|
|
(State(rB, [Agent(B), Step(1), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), Agent(A), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), pair(Agent(A), pair(SymKey(KAB), Nonce(T)))), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload)), scrypt(SymKey(KAB), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload))), SID(sid)] ) : DenningSacco_fp) &
|
|
(Iknows(scrypt(SymKey(KAB), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload)))) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_12: "[|
|
|
State(rB, [Agent(B), Step(0), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), Agent(A), SID(sid)] ) : DenningSacco_fp;
|
|
Iknows(SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB))) : DenningSacco_fp;
|
|
Iknows(Agent(A)) : DenningSacco_fp;
|
|
Iknows(SymKey(KAB)) : DenningSacco_fp;
|
|
Iknows(Nonce(T)) : DenningSacco_fp|]
|
|
==>
|
|
(Secret(Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload)), Agent(A)) : DenningSacco_fp) &
|
|
(Witness(Agent(B), Agent(A), Purpose(purposePayload), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload))) : DenningSacco_fp) &
|
|
(State(rB, [Agent(B), Step(1), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), Agent(A), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(B), Agent(honest(a)))) Abs_KAB)), pair(Agent(A), pair(SymKey(KAB), Nonce(T)))), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload)), scrypt(SymKey(KAB), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload))), SID(sid)] ) : DenningSacco_fp) &
|
|
(Iknows(scrypt(SymKey(KAB), Nonce((payload(pair(Agent(B), Agent(A))) Abs_Payload)))) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_13: "[|
|
|
State(rA, [Agent(A), Step(2), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), Agent(dishonest(i)), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i)))))), SID(sid)] ) : DenningSacco_fp;
|
|
Iknows(scrypt(SymKey(KAB), Nonce(Payload))) : DenningSacco_fp|]
|
|
==>
|
|
(Request(Agent(A), Agent(B), Purpose(purposePayload), Nonce(Payload), SID(sid)) : DenningSacco_fp) &
|
|
(State(rA, [Agent(A), Step(3), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), Agent(dishonest(i)), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i)))))), Nonce(Payload), scrypt(SymKey(KAB), Nonce(Payload)), SID(sid)] ) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
lemma rule_14: "[|
|
|
State(rA, [Agent(A), Step(2), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), Agent(dishonest(i)), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i)))))), SID(sid)] ) : DenningSacco_fp;
|
|
Iknows(SymKey(KAB)) : DenningSacco_fp;
|
|
Iknows(Nonce(Payload)) : DenningSacco_fp|]
|
|
==>
|
|
(Request(Agent(A), Agent(B), Purpose(purposePayload), Nonce(Payload), SID(sid)) : DenningSacco_fp) &
|
|
(State(rA, [Agent(A), Step(3), Nonce((timestamp Abs_T)), SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), Agent(B), pair(Agent(A), Agent(B)), Agent(dishonest(i)), Nonce(T), SymKey(KAB), scrypt(SymKey((sk(pair(Agent(A), Agent(honest(a)))) Abs_KAB)), pair(Agent(B), pair(SymKey(KAB), pair(Nonce(T), Agent(dishonest(i)))))), Nonce(Payload), scrypt(SymKey(KAB), Nonce(Payload)), SID(sid)] ) : DenningSacco_fp)"
|
|
by(simp only: DenningSacco_fp_def, simp only: set2pred, simp, auto?)+
|
|
|
|
|
|
|
|
section {* Security Proof(s) (DenningSacco) *}
|
|
lemma over_approx: "t : DenningSacco ==> (set t) <= DenningSacco_fp"
|
|
apply(rule DenningSacco.induct, simp_all)
|
|
apply(propagate_fp, cut_tac init_0, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_1, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_2, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_3, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_4, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_5, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_6, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_7, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_8, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_9, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_10, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_11, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_12, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_13, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac init_14, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_0, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_1, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_2, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_3, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_4, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_5, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_6, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_7, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_8, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_9, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_10, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_11, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_12, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_13, (assumption | simp)+)
|
|
apply(propagate_fp, cut_tac rule_14, (assumption | simp)+)
|
|
done
|
|
|
|
|
|
|
|
end (* theory *)
|