This repository has been archived on 2021-01-01. You can view files and clone it, but cannot push or open issues or pull requests.
isabelle-ofmc/examples/Bilateral-Key_Exchange.thy

610 lines
63 KiB
Plaintext

chapter {* Analysing BilateralKeyExchange *}
(* ***********************************
This file is automatically generated from the AnB file "AnB/Bilateral-Key_Exchange.AnB".
Backend: Open Source Fixedpoint Model Checker version 2009c
************************************ *)
theory
"Bilateral-Key_Exchange"
imports
"../src/ofmc"
begin
section {* Protocol Model (BilateralKeyExchange) *}
datatype Role = rA | rB
datatype Purpose = purposeK | purposeNI | purposeNA | purposeNB
datatype Agent = honest nat
| dishonest nat
datatype Nonce = "ni" "nat"
| "absNB" "Msg" "nat"
| "absNA" "Msg" "nat"
| "NI"
| "NA"
| "NB"
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"
| "absK" "Msg" "nat"
(* Functions *)
| "pk" "Msg" | "f" "Msg"
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 (BilateralKeyExchange) *}
inductive_set
BilateralKeyExchange::"Fact list set"
where
init_0: "[ Iknows(Nonce((ni Abs_NI)))] : BilateralKeyExchange"
| init_1: "[ Iknows(Agent(dishonest(i)))] : BilateralKeyExchange"
| init_2: "[ State(rA, [Agent(honest(a)), Step(0), inv(pk(Agent(honest(a)))), pk(Agent(dishonest(i))), pk(Agent(honest(a))), Agent(dishonest(i)), SID(sid)] )] : BilateralKeyExchange"
| init_3: "[ State(rA, [Agent(honest(a)), Step(0), inv(pk(Agent(honest(a)))), pk(Agent(honest(a))), pk(Agent(honest(a))), Agent(honest(a)), SID(sid)] )] : BilateralKeyExchange"
| init_4: "[ Iknows(Step(0))] : BilateralKeyExchange"
| init_5: "[ Iknows(inv(pk(Agent(dishonest(i)))))] : BilateralKeyExchange"
| init_6: "[ Iknows(pk(Agent(dishonest(i))))] : BilateralKeyExchange"
| init_7: "[ Iknows(SID(sid))] : BilateralKeyExchange"
| init_8: "[ Iknows(pk(Agent(honest(a))))] : BilateralKeyExchange"
| init_9: "[ Iknows(Agent(honest(a)))] : BilateralKeyExchange"
| init_10: "[ State(rB, [Agent(honest(a)), Step(0), inv(pk(Agent(honest(a)))), pk(Agent(honest(a))), pk(Agent(dishonest(i))), Agent(dishonest(i)), SID(sid)] )] : BilateralKeyExchange"
| init_11: "[ State(rB, [Agent(honest(a)), Step(0), inv(pk(Agent(honest(a)))), pk(Agent(honest(a))), pk(Agent(honest(a))), Agent(honest(a)), SID(sid)] )] : BilateralKeyExchange"
| rule_0: "[| t :BilateralKeyExchange;
Iknows(crypt(K, M)) : (set t);
Iknows(inv(K)) : (set t)|]
==>
((Iknows(M))
#t) : BilateralKeyExchange"
| rule_1: "[| t :BilateralKeyExchange;
Iknows(crypt(inv(K), M)) : (set t);
Iknows(K) : (set t)|]
==>
((Iknows(M))
#t) : BilateralKeyExchange"
| rule_2: "[| t :BilateralKeyExchange;
Iknows(scrypt(K, M)) : (set t);
Iknows(K) : (set t)|]
==>
((Iknows(M))
#t) : BilateralKeyExchange"
| rule_3: "[| t :BilateralKeyExchange;
Iknows(pair(M1, M2)) : (set t)|]
==>
((Iknows(M1))
#(Iknows(M2))
#t) : BilateralKeyExchange"
| rule_4: "[| t :BilateralKeyExchange;
Secret(M, Agent(honest(a))) : (set t);
Iknows(M) : (set t)|]
==>
((Attack(pair(secrecy, M)))
#t) : BilateralKeyExchange"
| rule_5: "[| t :BilateralKeyExchange;
Request(A, B, Purpose(purposeNB), M, SID(sid)) : (set t);
~ ( ? i .
B = Agent(dishonest(i)));
~ ( ? B A Abs_NB .
M = Nonce((absNB(pair(B, A)) Abs_NB)))|]
==>
((Attack(pair(authentication, pair(A, pair(B, M)))))
#t) : BilateralKeyExchange"
| rule_6: "[| t :BilateralKeyExchange;
Request(A, B, Purpose(purposeNA), M, SID(sid)) : (set t);
~ ( ? i .
B = Agent(dishonest(i)));
~ ( ? B A Abs_NA .
M = Nonce((absNA(pair(B, A)) Abs_NA)))|]
==>
((Attack(pair(authentication, pair(A, pair(B, M)))))
#t) : BilateralKeyExchange"
| rule_7: "[| t :BilateralKeyExchange;
Request(A, B, Purpose(purposeK), M, SID(sid)) : (set t);
~ ( ? i .
B = Agent(dishonest(i)));
~ ( ? B A Abs_K .
M = SymKey((absK(pair(B, A)) Abs_K)))|]
==>
((Attack(pair(authentication, pair(A, pair(B, M)))))
#t) : BilateralKeyExchange"
| rule_8: "[| t :BilateralKeyExchange;
State(rB, [Agent(B), Step(0), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), SID(sid)] ) : (set t)|]
==>
((State(rB, [Agent(B), Step(1), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce((absNB(pair(Agent(B), Agent(A))) Abs_NB)), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce((absNB(pair(Agent(B), Agent(A))) Abs_NB)), Agent(B)))), SID(sid)] ))
#(Iknows(pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce((absNB(pair(Agent(B), Agent(A))) Abs_NB)), Agent(B))))))
#t) : BilateralKeyExchange"
| rule_9: "[| t :BilateralKeyExchange;
State(rA, [Agent(A), Step(0), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), SID(sid)] ) : (set t);
Iknows(Agent(B)) : (set t);
Iknows(crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))) : (set t)|]
==>
((Secret(SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)), Agent(B)))
#(Witness(Agent(A), Agent(B), Purpose(purposeK), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K))))
#(State(rA, [Agent(A), Step(1), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), pair(Agent(A), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)))))), SID(sid)] ))
#(Iknows(crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), pair(Agent(A), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K))))))))
#t) : BilateralKeyExchange"
| rule_10: "[| t :BilateralKeyExchange;
State(rA, [Agent(A), Step(0), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), SID(sid)] ) : (set t);
Iknows(Agent(B)) : (set t);
Iknows(pk(Agent(A))) : (set t);
Iknows(Nonce(NB)) : (set t)|]
==>
((Secret(SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)), Agent(B)))
#(Witness(Agent(A), Agent(B), Purpose(purposeK), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K))))
#(State(rA, [Agent(A), Step(1), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), pair(Agent(A), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)))))), SID(sid)] ))
#(Iknows(crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), pair(Agent(A), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K))))))))
#t) : BilateralKeyExchange"
| rule_11: "[| t :BilateralKeyExchange;
State(rA, [Agent(A), Step(0), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), SID(sid)] ) : (set t);
Iknows(Agent(B)) : (set t);
Iknows(Agent(A)) : (set t);
Iknows(Nonce(NB)) : (set t)|]
==>
((Secret(SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)), Agent(B)))
#(Witness(Agent(A), Agent(B), Purpose(purposeK), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K))))
#(State(rA, [Agent(A), Step(1), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), pair(Agent(A), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)))))), SID(sid)] ))
#(Iknows(crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), pair(Agent(A), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K))))))))
#t) : BilateralKeyExchange"
| rule_12: "[| t :BilateralKeyExchange;
State(rB, [Agent(B), Step(1), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), SID(sid)] ) : (set t);
Iknows(crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K)))))) : (set t)|]
==>
((Request(Agent(B), Agent(A), Purpose(purposeK), SymKey(K), SID(sid)))
#(State(rB, [Agent(B), Step(2), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), SymKey(K), Nonce(NA), f(Nonce(NB)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ))
#(Iknows(scrypt(SymKey(K), f(Nonce(NA)))))
#t) : BilateralKeyExchange"
| rule_13: "[| t :BilateralKeyExchange;
State(rB, [Agent(B), Step(1), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), SID(sid)] ) : (set t);
Iknows(pk(Agent(B))) : (set t);
Iknows(f(Nonce(NB))) : (set t);
Iknows(Nonce(NA)) : (set t);
Iknows(Agent(A)) : (set t);
Iknows(SymKey(K)) : (set t)|]
==>
((Request(Agent(B), Agent(A), Purpose(purposeK), SymKey(K), SID(sid)))
#(State(rB, [Agent(B), Step(2), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), SymKey(K), Nonce(NA), f(Nonce(NB)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ))
#(Iknows(scrypt(SymKey(K), f(Nonce(NA)))))
#t) : BilateralKeyExchange"
| rule_14: "[| t :BilateralKeyExchange;
State(rB, [Agent(B), Step(1), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), SID(sid)] ) : (set t);
Iknows(pk(Agent(B))) : (set t);
Iknows(Nonce(NB)) : (set t);
Iknows(Nonce(NA)) : (set t);
Iknows(Agent(A)) : (set t);
Iknows(SymKey(K)) : (set t)|]
==>
((Request(Agent(B), Agent(A), Purpose(purposeK), SymKey(K), SID(sid)))
#(State(rB, [Agent(B), Step(2), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), SymKey(K), Nonce(NA), f(Nonce(NB)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ))
#(Iknows(scrypt(SymKey(K), f(Nonce(NA)))))
#t) : BilateralKeyExchange"
| rule_15: "[| t :BilateralKeyExchange;
State(rB, [Agent(B), Step(1), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), SID(sid)] ) : (set t);
Iknows(Agent(B)) : (set t);
Iknows(f(Nonce(NB))) : (set t);
Iknows(Nonce(NA)) : (set t);
Iknows(Agent(A)) : (set t);
Iknows(SymKey(K)) : (set t)|]
==>
((Request(Agent(B), Agent(A), Purpose(purposeK), SymKey(K), SID(sid)))
#(State(rB, [Agent(B), Step(2), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), SymKey(K), Nonce(NA), f(Nonce(NB)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ))
#(Iknows(scrypt(SymKey(K), f(Nonce(NA)))))
#t) : BilateralKeyExchange"
| rule_16: "[| t :BilateralKeyExchange;
State(rB, [Agent(B), Step(1), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), SID(sid)] ) : (set t);
Iknows(Agent(B)) : (set t);
Iknows(Nonce(NB)) : (set t);
Iknows(Nonce(NA)) : (set t);
Iknows(Agent(A)) : (set t);
Iknows(SymKey(K)) : (set t)|]
==>
((Request(Agent(B), Agent(A), Purpose(purposeK), SymKey(K), SID(sid)))
#(State(rB, [Agent(B), Step(2), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), SymKey(K), Nonce(NA), f(Nonce(NB)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ))
#(Iknows(scrypt(SymKey(K), f(Nonce(NA)))))
#t) : BilateralKeyExchange"
| rule_17: "[| t :BilateralKeyExchange;
State(rA, [Agent(A), Step(1), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce(NA), SymKey(K), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), SID(sid)] ) : (set t);
Iknows(scrypt(SymKey(K), f(Nonce(NA)))) : (set t)|]
==>
((State(rA, [Agent(A), Step(2), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce(NA), SymKey(K), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ))
#t) : BilateralKeyExchange"
| rule_18: "[| t :BilateralKeyExchange;
State(rA, [Agent(A), Step(1), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce(NA), SymKey(K), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), SID(sid)] ) : (set t);
Iknows(SymKey(K)) : (set t);
Iknows(f(Nonce(NA))) : (set t)|]
==>
((State(rA, [Agent(A), Step(2), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce(NA), SymKey(K), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ))
#t) : BilateralKeyExchange"
| rule_19: "[| t :BilateralKeyExchange;
State(rA, [Agent(A), Step(1), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce(NA), SymKey(K), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), SID(sid)] ) : (set t);
Iknows(SymKey(K)) : (set t);
Iknows(Nonce(NA)) : (set t)|]
==>
((State(rA, [Agent(A), Step(2), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce(NA), SymKey(K), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ))
#t) : BilateralKeyExchange"
section {* Fixed-point Definition (BilateralKeyExchange) *}
definition
"BilateralKeyExchange_fp = {m. ( ? a32 a33 Abs_NB5 Abs_NB6 Abs_NB7 Abs_NB4 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 i14 i15 Abs_NA3 i3 Abs_NA4 Abs_NA5 Abs_NA6 Abs_NB1 Abs_NB2 Abs_NB3 a24 a25 a26 a27 a28 a29 a30 a31 a5 Abs_NI1 a6 a7 a8 Abs_NI2 a9 a10 a11 a12 a13 a14 Abs_NI3 a15 a16 a17 a18 a19 Abs_K1 a20 a21 Abs_K2 a22 a23 Abs_NA2 sid0 a4 Abs_NI0 Abs_NB0 a0 i0 Abs_NA0 a1 i1 Abs_NA1 a2 a3 i2 Abs_K0 .
(m = Iknows(Nonce((ni Abs_NI0))))
| (m = Iknows(Agent(dishonest(i0))))
| (m = State(rA, [Agent(honest(a0)), Step(0), inv(pk(Agent(honest(a1)))), pk(Agent(dishonest(i0))), pk(Agent(honest(a2))), Agent(dishonest(i1)), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(0), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(honest(a3))), Agent(honest(a4)), SID(sid0)] ))
| (m = Iknows(Step(0)))
| (m = Iknows(inv(pk(Agent(dishonest(i0))))))
| (m = Iknows(pk(Agent(dishonest(i0)))))
| (m = Iknows(SID(sid0)))
| (m = Iknows(pk(Agent(honest(a0)))))
| (m = Iknows(Agent(honest(a0))))
| (m = State(rB, [Agent(honest(a0)), Step(0), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(dishonest(i0))), Agent(dishonest(i1)), SID(sid0)] ))
| (m = State(rB, [Agent(honest(a0)), Step(0), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(honest(a3))), Agent(honest(a4)), SID(sid0)] ))
| (m = Iknows(pair(Agent(honest(a0)), crypt(pk(Agent(honest(a1))), pair(Nonce((absNB(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_NB0)), Agent(honest(a4)))))))
| (m = Iknows(pair(Agent(honest(a0)), crypt(pk(Agent(dishonest(i0))), pair(Nonce((absNB(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NB0)), Agent(honest(a2)))))))
| (m = State(rB, [Agent(honest(a0)), Step(1), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(dishonest(i0))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_NB0)), pair(Agent(honest(a4)), crypt(pk(Agent(dishonest(i3))), pair(Nonce((absNB(pair(Agent(honest(a5)), Agent(dishonest(i4)))) Abs_NB1)), Agent(honest(a6))))), SID(sid0)] ))
| (m = State(rB, [Agent(honest(a0)), Step(1), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(honest(a3))), Agent(honest(a4)), Nonce((absNB(pair(Agent(honest(a5)), Agent(honest(a6)))) Abs_NB0)), pair(Agent(honest(a7)), crypt(pk(Agent(honest(a8))), pair(Nonce((absNB(pair(Agent(honest(a9)), Agent(honest(a10)))) Abs_NB1)), Agent(honest(a11))))), SID(sid0)] ))
| (m = Secret(SymKey((absK(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_K0)), Agent(dishonest(i1))))
| (m = Witness(Agent(honest(a0)), Agent(dishonest(i0)), Purpose(purposeK), SymKey((absK(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_K0))))
| (m = State(rA, [Agent(honest(a0)), Step(1), inv(pk(Agent(honest(a1)))), pk(Agent(dishonest(i0))), pk(Agent(honest(a2))), Agent(dishonest(i1)), Nonce((ni Abs_NI0)), crypt(pk(Agent(honest(a3))), pair(Nonce((ni Abs_NI1)), Agent(dishonest(i2)))), pair(Agent(dishonest(i3)), crypt(pk(Agent(honest(a4))), pair(Nonce((ni Abs_NI2)), Agent(dishonest(i4))))), Nonce((absNA(pair(Agent(honest(a5)), Agent(dishonest(i5)))) Abs_NA0)), SymKey((absK(pair(Agent(honest(a6)), Agent(dishonest(i6)))) Abs_K0)), crypt(pk(Agent(dishonest(i7))), pair(f(Nonce((ni Abs_NI3))), pair(Nonce((absNA(pair(Agent(honest(a7)), Agent(dishonest(i8)))) Abs_NA1)), pair(Agent(honest(a8)), SymKey((absK(pair(Agent(honest(a9)), Agent(dishonest(i9)))) Abs_K1)))))), SID(sid0)] ))
| (m = Secret(SymKey((absK(pair(Agent(honest(a0)), Agent(honest(a1)))) Abs_K0)), Agent(honest(a2))))
| (m = Witness(Agent(honest(a0)), Agent(honest(a1)), Purpose(purposeK), SymKey((absK(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_K0))))
| (m = State(rA, [Agent(honest(a0)), Step(1), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(honest(a3))), Agent(honest(a4)), Nonce((ni Abs_NI0)), crypt(pk(Agent(honest(a5))), pair(Nonce((ni Abs_NI1)), Agent(honest(a6)))), pair(Agent(honest(a7)), crypt(pk(Agent(honest(a8))), pair(Nonce((ni Abs_NI2)), Agent(honest(a9))))), Nonce((absNA(pair(Agent(honest(a10)), Agent(honest(a11)))) Abs_NA0)), SymKey((absK(pair(Agent(honest(a12)), Agent(honest(a13)))) Abs_K0)), crypt(pk(Agent(honest(a14))), pair(f(Nonce((ni Abs_NI3))), pair(Nonce((absNA(pair(Agent(honest(a15)), Agent(honest(a16)))) Abs_NA1)), pair(Agent(honest(a17)), SymKey((absK(pair(Agent(honest(a18)), Agent(honest(a19)))) Abs_K1)))))), SID(sid0)] ))
| (m = Iknows(crypt(pk(Agent(honest(a0))), pair(f(Nonce((ni Abs_NI0))), pair(Nonce((absNA(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_NA0)), pair(Agent(honest(a3)), SymKey((absK(pair(Agent(honest(a4)), Agent(honest(a5)))) Abs_K0))))))))
| (m = Iknows(crypt(pk(Agent(dishonest(i0))), pair(f(Nonce((ni Abs_NI0))), pair(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i1)))) Abs_NA0)), pair(Agent(honest(a1)), SymKey((absK(pair(Agent(honest(a2)), Agent(dishonest(i2)))) Abs_K0))))))))
| (m = Iknows(crypt(pk(Agent(honest(a0))), pair(Nonce((absNB(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_NB0)), Agent(honest(a3))))))
| (m = Iknows(crypt(pk(Agent(dishonest(i0))), pair(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i1)))) Abs_NB0)), Agent(honest(a1))))))
| (m = Iknows(pair(Agent(honest(a0)), crypt(pk(Agent(honest(a1))), pair(Nonce((absNB(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_NB0)), Agent(honest(a4)))))))
| (m = Iknows(pair(Agent(honest(a0)), crypt(pk(Agent(dishonest(i0))), pair(Nonce((absNB(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NB0)), Agent(honest(a2)))))))
| (m = Iknows(pair(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NB0)), Agent(honest(a1)))))
| (m = Iknows(pair(Agent(honest(a0)), SymKey((absK(pair(Agent(honest(a1)), Agent(dishonest(i0)))) Abs_K0)))))
| (m = Iknows(pair(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NA0)), pair(Agent(honest(a1)), SymKey((absK(pair(Agent(honest(a2)), Agent(dishonest(i1)))) Abs_K0))))))
| (m = Iknows(pair(f(Nonce((ni Abs_NI0))), pair(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NA0)), pair(Agent(honest(a1)), SymKey((absK(pair(Agent(honest(a2)), Agent(dishonest(i1)))) Abs_K0)))))))
| (m = State(rA, [Agent(honest(a0)), Step(1), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(honest(a3))), Agent(honest(a4)), Nonce((absNB(pair(Agent(honest(a5)), Agent(honest(a6)))) Abs_NB0)), crypt(pk(Agent(honest(a7))), pair(Nonce((absNB(pair(Agent(honest(a8)), Agent(honest(a9)))) Abs_NB1)), Agent(honest(a10)))), pair(Agent(honest(a11)), crypt(pk(Agent(honest(a12))), pair(Nonce((absNB(pair(Agent(honest(a13)), Agent(honest(a14)))) Abs_NB2)), Agent(honest(a15))))), Nonce((absNA(pair(Agent(honest(a16)), Agent(honest(a17)))) Abs_NA0)), SymKey((absK(pair(Agent(honest(a18)), Agent(honest(a19)))) Abs_K0)), crypt(pk(Agent(honest(a20))), pair(f(Nonce((absNB(pair(Agent(honest(a21)), Agent(honest(a22)))) Abs_NB3))), pair(Nonce((absNA(pair(Agent(honest(a23)), Agent(honest(a24)))) Abs_NA1)), pair(Agent(honest(a25)), SymKey((absK(pair(Agent(honest(a26)), Agent(honest(a27)))) Abs_K1)))))), SID(sid0)] ))
| (m = Iknows(crypt(pk(Agent(honest(a0))), pair(f(Nonce((absNB(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_NB0))), pair(Nonce((absNA(pair(Agent(honest(a3)), Agent(honest(a4)))) Abs_NA0)), pair(Agent(honest(a5)), SymKey((absK(pair(Agent(honest(a6)), Agent(honest(a7)))) Abs_K0))))))))
| (m = Iknows(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NB0))))
| (m = Iknows(SymKey((absK(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_K0))))
| (m = Iknows(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NA0))))
| (m = Iknows(f(Nonce((ni Abs_NI0)))))
| (m = Iknows(pair(Agent(honest(a0)), crypt(pk(Agent(honest(a1))), pair(Nonce((absNB(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_NB0)), Agent(honest(a4)))))))
| (m = Iknows(pair(Agent(honest(a0)), crypt(pk(Agent(dishonest(i0))), pair(Nonce((absNB(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NB0)), Agent(honest(a2)))))))
| (m = Iknows(pair(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NB0)), Agent(honest(a1)))))
| (m = Iknows(pair(Agent(honest(a0)), SymKey((absK(pair(Agent(honest(a1)), Agent(dishonest(i0)))) Abs_K0)))))
| (m = Iknows(pair(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NA0)), pair(Agent(honest(a1)), SymKey((absK(pair(Agent(honest(a2)), Agent(dishonest(i1)))) Abs_K0))))))
| (m = Iknows(pair(f(Nonce((ni Abs_NI0))), pair(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NA0)), pair(Agent(honest(a1)), SymKey((absK(pair(Agent(honest(a2)), Agent(dishonest(i1)))) Abs_K0)))))))
| (m = State(rA, [Agent(honest(a0)), Step(1), inv(pk(Agent(honest(a1)))), pk(Agent(dishonest(i0))), pk(Agent(honest(a2))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_NB0)), crypt(pk(Agent(honest(a4))), pair(Nonce((absNB(pair(Agent(honest(a5)), Agent(dishonest(i3)))) Abs_NB1)), Agent(dishonest(i4)))), pair(Agent(dishonest(i5)), crypt(pk(Agent(honest(a6))), pair(Nonce((absNB(pair(Agent(honest(a7)), Agent(dishonest(i6)))) Abs_NB2)), Agent(dishonest(i7))))), Nonce((absNA(pair(Agent(honest(a8)), Agent(dishonest(i8)))) Abs_NA0)), SymKey((absK(pair(Agent(honest(a9)), Agent(dishonest(i9)))) Abs_K0)), crypt(pk(Agent(dishonest(i10))), pair(f(Nonce((absNB(pair(Agent(honest(a10)), Agent(dishonest(i11)))) Abs_NB3))), pair(Nonce((absNA(pair(Agent(honest(a11)), Agent(dishonest(i12)))) Abs_NA1)), pair(Agent(honest(a12)), SymKey((absK(pair(Agent(honest(a13)), Agent(dishonest(i13)))) Abs_K1)))))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(1), inv(pk(Agent(honest(a1)))), pk(Agent(dishonest(i0))), pk(Agent(honest(a2))), Agent(dishonest(i1)), Nonce((absNA(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_NA0)), crypt(pk(Agent(honest(a4))), pair(Nonce((absNA(pair(Agent(honest(a5)), Agent(dishonest(i3)))) Abs_NA1)), Agent(dishonest(i4)))), pair(Agent(dishonest(i5)), crypt(pk(Agent(honest(a6))), pair(Nonce((absNA(pair(Agent(honest(a7)), Agent(dishonest(i6)))) Abs_NA2)), Agent(dishonest(i7))))), Nonce((absNA(pair(Agent(honest(a8)), Agent(dishonest(i8)))) Abs_NA3)), SymKey((absK(pair(Agent(honest(a9)), Agent(dishonest(i9)))) Abs_K0)), crypt(pk(Agent(dishonest(i10))), pair(f(Nonce((absNA(pair(Agent(honest(a10)), Agent(dishonest(i11)))) Abs_NA4))), pair(Nonce((absNA(pair(Agent(honest(a11)), Agent(dishonest(i12)))) Abs_NA5)), pair(Agent(honest(a12)), SymKey((absK(pair(Agent(honest(a13)), Agent(dishonest(i13)))) Abs_K1)))))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(1), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(honest(a3))), Agent(honest(a4)), Nonce((absNB(pair(Agent(honest(a5)), Agent(dishonest(i0)))) Abs_NB0)), crypt(pk(Agent(honest(a6))), pair(Nonce((absNB(pair(Agent(honest(a7)), Agent(dishonest(i1)))) Abs_NB1)), Agent(honest(a8)))), pair(Agent(honest(a9)), crypt(pk(Agent(honest(a10))), pair(Nonce((absNB(pair(Agent(honest(a11)), Agent(dishonest(i2)))) Abs_NB2)), Agent(honest(a12))))), Nonce((absNA(pair(Agent(honest(a13)), Agent(honest(a14)))) Abs_NA0)), SymKey((absK(pair(Agent(honest(a15)), Agent(honest(a16)))) Abs_K0)), crypt(pk(Agent(honest(a17))), pair(f(Nonce((absNB(pair(Agent(honest(a18)), Agent(dishonest(i3)))) Abs_NB3))), pair(Nonce((absNA(pair(Agent(honest(a19)), Agent(honest(a20)))) Abs_NA1)), pair(Agent(honest(a21)), SymKey((absK(pair(Agent(honest(a22)), Agent(honest(a23)))) Abs_K1)))))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(1), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(honest(a3))), Agent(honest(a4)), Nonce((absNA(pair(Agent(honest(a5)), Agent(dishonest(i0)))) Abs_NA0)), crypt(pk(Agent(honest(a6))), pair(Nonce((absNA(pair(Agent(honest(a7)), Agent(dishonest(i1)))) Abs_NA1)), Agent(honest(a8)))), pair(Agent(honest(a9)), crypt(pk(Agent(honest(a10))), pair(Nonce((absNA(pair(Agent(honest(a11)), Agent(dishonest(i2)))) Abs_NA2)), Agent(honest(a12))))), Nonce((absNA(pair(Agent(honest(a13)), Agent(honest(a14)))) Abs_NA3)), SymKey((absK(pair(Agent(honest(a15)), Agent(honest(a16)))) Abs_K0)), crypt(pk(Agent(honest(a17))), pair(f(Nonce((absNA(pair(Agent(honest(a18)), Agent(dishonest(i3)))) Abs_NA4))), pair(Nonce((absNA(pair(Agent(honest(a19)), Agent(honest(a20)))) Abs_NA5)), pair(Agent(honest(a21)), SymKey((absK(pair(Agent(honest(a22)), Agent(honest(a23)))) Abs_K1)))))), SID(sid0)] ))
| (m = Request(Agent(honest(a0)), Agent(honest(a1)), Purpose(purposeK), SymKey((absK(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_K0)), SID(sid0)))
| (m = State(rB, [Agent(honest(a0)), Step(2), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(honest(a3))), Agent(honest(a4)), Nonce((absNB(pair(Agent(honest(a5)), Agent(honest(a6)))) Abs_NB0)), pair(Agent(honest(a7)), crypt(pk(Agent(honest(a8))), pair(Nonce((absNB(pair(Agent(honest(a9)), Agent(honest(a10)))) Abs_NB1)), Agent(honest(a11))))), crypt(pk(Agent(honest(a12))), pair(Nonce((absNB(pair(Agent(honest(a13)), Agent(honest(a14)))) Abs_NB2)), Agent(honest(a15)))), SymKey((absK(pair(Agent(honest(a16)), Agent(honest(a17)))) Abs_K0)), Nonce((absNA(pair(Agent(honest(a18)), Agent(honest(a19)))) Abs_NA0)), f(Nonce((absNB(pair(Agent(honest(a20)), Agent(honest(a21)))) Abs_NB3))), crypt(pk(Agent(honest(a22))), pair(f(Nonce((absNB(pair(Agent(honest(a23)), Agent(honest(a24)))) Abs_NB4))), pair(Nonce((absNA(pair(Agent(honest(a25)), Agent(honest(a26)))) Abs_NA1)), pair(Agent(honest(a27)), SymKey((absK(pair(Agent(honest(a28)), Agent(honest(a29)))) Abs_K1)))))), scrypt(SymKey((absK(pair(Agent(honest(a30)), Agent(honest(a31)))) Abs_K2)), f(Nonce((absNA(pair(Agent(honest(a32)), Agent(honest(a33)))) Abs_NA2)))), SID(sid0)] ))
| (m = Request(Agent(honest(a0)), Agent(dishonest(i0)), Purpose(purposeK), SymKey((absK(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_K0)), SID(sid0)))
| (m = State(rB, [Agent(honest(a0)), Step(2), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(dishonest(i0))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_NB0)), pair(Agent(honest(a4)), crypt(pk(Agent(dishonest(i3))), pair(Nonce((absNB(pair(Agent(honest(a5)), Agent(dishonest(i4)))) Abs_NB1)), Agent(honest(a6))))), crypt(pk(Agent(dishonest(i5))), pair(Nonce((absNB(pair(Agent(honest(a7)), Agent(dishonest(i6)))) Abs_NB2)), Agent(honest(a8)))), SymKey((absK(pair(Agent(honest(a9)), Agent(dishonest(i7)))) Abs_K0)), Nonce((absNB(pair(Agent(honest(a10)), Agent(dishonest(i8)))) Abs_NB3)), f(Nonce((absNB(pair(Agent(honest(a11)), Agent(dishonest(i9)))) Abs_NB4))), crypt(pk(Agent(honest(a12))), pair(f(Nonce((absNB(pair(Agent(honest(a13)), Agent(dishonest(i10)))) Abs_NB5))), pair(Nonce((absNB(pair(Agent(honest(a14)), Agent(dishonest(i11)))) Abs_NB6)), pair(Agent(dishonest(i12)), SymKey((absK(pair(Agent(honest(a15)), Agent(dishonest(i13)))) Abs_K1)))))), scrypt(SymKey((absK(pair(Agent(honest(a16)), Agent(dishonest(i14)))) Abs_K2)), f(Nonce((absNB(pair(Agent(honest(a17)), Agent(dishonest(i15)))) Abs_NB7)))), SID(sid0)] ))
| (m = State(rB, [Agent(honest(a0)), Step(2), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(dishonest(i0))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_NB0)), pair(Agent(honest(a4)), crypt(pk(Agent(dishonest(i3))), pair(Nonce((absNB(pair(Agent(honest(a5)), Agent(dishonest(i4)))) Abs_NB1)), Agent(honest(a6))))), crypt(pk(Agent(dishonest(i5))), pair(Nonce((absNB(pair(Agent(honest(a7)), Agent(dishonest(i6)))) Abs_NB2)), Agent(honest(a8)))), SymKey((absK(pair(Agent(honest(a9)), Agent(dishonest(i7)))) Abs_K0)), Nonce((absNA(pair(Agent(honest(a10)), Agent(dishonest(i8)))) Abs_NA0)), f(Nonce((absNB(pair(Agent(honest(a11)), Agent(dishonest(i9)))) Abs_NB3))), crypt(pk(Agent(honest(a12))), pair(f(Nonce((absNB(pair(Agent(honest(a13)), Agent(dishonest(i10)))) Abs_NB4))), pair(Nonce((absNA(pair(Agent(honest(a14)), Agent(dishonest(i11)))) Abs_NA1)), pair(Agent(dishonest(i12)), SymKey((absK(pair(Agent(honest(a15)), Agent(dishonest(i13)))) Abs_K1)))))), scrypt(SymKey((absK(pair(Agent(honest(a16)), Agent(dishonest(i14)))) Abs_K2)), f(Nonce((absNA(pair(Agent(honest(a17)), Agent(dishonest(i15)))) Abs_NA2)))), SID(sid0)] ))
| (m = State(rB, [Agent(honest(a0)), Step(2), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(dishonest(i0))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_NB0)), pair(Agent(honest(a4)), crypt(pk(Agent(dishonest(i3))), pair(Nonce((absNB(pair(Agent(honest(a5)), Agent(dishonest(i4)))) Abs_NB1)), Agent(honest(a6))))), crypt(pk(Agent(dishonest(i5))), pair(Nonce((absNB(pair(Agent(honest(a7)), Agent(dishonest(i6)))) Abs_NB2)), Agent(honest(a8)))), SymKey((absK(pair(Agent(honest(a9)), Agent(dishonest(i7)))) Abs_K0)), Nonce((ni Abs_NI0)), f(Nonce((absNB(pair(Agent(honest(a10)), Agent(dishonest(i8)))) Abs_NB3))), crypt(pk(Agent(honest(a11))), pair(f(Nonce((absNB(pair(Agent(honest(a12)), Agent(dishonest(i9)))) Abs_NB4))), pair(Nonce((ni Abs_NI1)), pair(Agent(dishonest(i10)), SymKey((absK(pair(Agent(honest(a13)), Agent(dishonest(i11)))) Abs_K1)))))), scrypt(SymKey((absK(pair(Agent(honest(a14)), Agent(dishonest(i12)))) Abs_K2)), f(Nonce((ni Abs_NI2)))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(2), inv(pk(Agent(honest(a1)))), pk(Agent(dishonest(i0))), pk(Agent(honest(a2))), Agent(dishonest(i1)), Nonce((ni Abs_NI0)), crypt(pk(Agent(honest(a3))), pair(Nonce((ni Abs_NI1)), Agent(dishonest(i2)))), pair(Agent(dishonest(i3)), crypt(pk(Agent(honest(a4))), pair(Nonce((ni Abs_NI2)), Agent(dishonest(i4))))), Nonce((absNA(pair(Agent(honest(a5)), Agent(dishonest(i5)))) Abs_NA0)), SymKey((absK(pair(Agent(honest(a6)), Agent(dishonest(i6)))) Abs_K0)), crypt(pk(Agent(dishonest(i7))), pair(f(Nonce((ni Abs_NI3))), pair(Nonce((absNA(pair(Agent(honest(a7)), Agent(dishonest(i8)))) Abs_NA1)), pair(Agent(honest(a8)), SymKey((absK(pair(Agent(honest(a9)), Agent(dishonest(i9)))) Abs_K1)))))), scrypt(SymKey((absK(pair(Agent(honest(a10)), Agent(dishonest(i10)))) Abs_K2)), f(Nonce((absNA(pair(Agent(honest(a11)), Agent(dishonest(i11)))) Abs_NA2)))), SID(sid0)] ))
| (m = Iknows(scrypt(SymKey((absK(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_K0)), f(Nonce((ni Abs_NI0))))))
| (m = Iknows(scrypt(SymKey((absK(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_K0)), f(Nonce((absNA(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NA0))))))
| (m = Iknows(scrypt(SymKey((absK(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_K0)), f(Nonce((absNB(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NB0))))))
| (m = Iknows(scrypt(SymKey((absK(pair(Agent(honest(a0)), Agent(honest(a1)))) Abs_K0)), f(Nonce((absNA(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_NA0))))))
| (m = Iknows(crypt(pk(Agent(honest(a0))), pair(f(Nonce((absNA(pair(Agent(honest(a1)), Agent(dishonest(i0)))) Abs_NA0))), pair(Nonce((absNA(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_NA1)), pair(Agent(honest(a4)), SymKey((absK(pair(Agent(honest(a5)), Agent(honest(a6)))) Abs_K0))))))))
| (m = Iknows(crypt(pk(Agent(honest(a0))), pair(f(Nonce((absNB(pair(Agent(honest(a1)), Agent(dishonest(i0)))) Abs_NB0))), pair(Nonce((absNA(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_NA0)), pair(Agent(honest(a4)), SymKey((absK(pair(Agent(honest(a5)), Agent(honest(a6)))) Abs_K0))))))))
| (m = Iknows(crypt(pk(Agent(dishonest(i0))), pair(f(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i1)))) Abs_NA0))), pair(Nonce((absNA(pair(Agent(honest(a1)), Agent(dishonest(i2)))) Abs_NA1)), pair(Agent(honest(a2)), SymKey((absK(pair(Agent(honest(a3)), Agent(dishonest(i3)))) Abs_K0))))))))
| (m = Iknows(crypt(pk(Agent(dishonest(i0))), pair(f(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i1)))) Abs_NB0))), pair(Nonce((absNA(pair(Agent(honest(a1)), Agent(dishonest(i2)))) Abs_NA0)), pair(Agent(honest(a2)), SymKey((absK(pair(Agent(honest(a3)), Agent(dishonest(i3)))) Abs_K0))))))))
| (m = Iknows(pair(Agent(honest(a0)), crypt(pk(Agent(honest(a1))), pair(Nonce((absNB(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_NB0)), Agent(honest(a4)))))))
| (m = Iknows(pair(Agent(honest(a0)), crypt(pk(Agent(dishonest(i0))), pair(Nonce((absNB(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NB0)), Agent(honest(a2)))))))
| (m = Iknows(pair(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NB0)), Agent(honest(a1)))))
| (m = Iknows(pair(Agent(honest(a0)), SymKey((absK(pair(Agent(honest(a1)), Agent(dishonest(i0)))) Abs_K0)))))
| (m = Iknows(pair(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NA0)), pair(Agent(honest(a1)), SymKey((absK(pair(Agent(honest(a2)), Agent(dishonest(i1)))) Abs_K0))))))
| (m = Iknows(pair(f(Nonce((ni Abs_NI0))), pair(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NA0)), pair(Agent(honest(a1)), SymKey((absK(pair(Agent(honest(a2)), Agent(dishonest(i1)))) Abs_K0)))))))
| (m = Iknows(pair(f(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NB0))), pair(Nonce((absNA(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NA0)), pair(Agent(honest(a2)), SymKey((absK(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_K0)))))))
| (m = Iknows(pair(f(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NA0))), pair(Nonce((absNA(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NA1)), pair(Agent(honest(a2)), SymKey((absK(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_K0)))))))
| (m = State(rA, [Agent(honest(a0)), Step(2), inv(pk(Agent(honest(a1)))), pk(Agent(dishonest(i0))), pk(Agent(honest(a2))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_NB0)), crypt(pk(Agent(honest(a4))), pair(Nonce((absNB(pair(Agent(honest(a5)), Agent(dishonest(i3)))) Abs_NB1)), Agent(dishonest(i4)))), pair(Agent(dishonest(i5)), crypt(pk(Agent(honest(a6))), pair(Nonce((absNB(pair(Agent(honest(a7)), Agent(dishonest(i6)))) Abs_NB2)), Agent(dishonest(i7))))), Nonce((absNA(pair(Agent(honest(a8)), Agent(dishonest(i8)))) Abs_NA0)), SymKey((absK(pair(Agent(honest(a9)), Agent(dishonest(i9)))) Abs_K0)), crypt(pk(Agent(dishonest(i10))), pair(f(Nonce((absNB(pair(Agent(honest(a10)), Agent(dishonest(i11)))) Abs_NB3))), pair(Nonce((absNA(pair(Agent(honest(a11)), Agent(dishonest(i12)))) Abs_NA1)), pair(Agent(honest(a12)), SymKey((absK(pair(Agent(honest(a13)), Agent(dishonest(i13)))) Abs_K1)))))), scrypt(SymKey((absK(pair(Agent(honest(a14)), Agent(dishonest(i14)))) Abs_K2)), f(Nonce((absNA(pair(Agent(honest(a15)), Agent(dishonest(i15)))) Abs_NA2)))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(2), inv(pk(Agent(honest(a1)))), pk(Agent(dishonest(i0))), pk(Agent(honest(a2))), Agent(dishonest(i1)), Nonce((absNA(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_NA0)), crypt(pk(Agent(honest(a4))), pair(Nonce((absNA(pair(Agent(honest(a5)), Agent(dishonest(i3)))) Abs_NA1)), Agent(dishonest(i4)))), pair(Agent(dishonest(i5)), crypt(pk(Agent(honest(a6))), pair(Nonce((absNA(pair(Agent(honest(a7)), Agent(dishonest(i6)))) Abs_NA2)), Agent(dishonest(i7))))), Nonce((absNA(pair(Agent(honest(a8)), Agent(dishonest(i8)))) Abs_NA3)), SymKey((absK(pair(Agent(honest(a9)), Agent(dishonest(i9)))) Abs_K0)), crypt(pk(Agent(dishonest(i10))), pair(f(Nonce((absNA(pair(Agent(honest(a10)), Agent(dishonest(i11)))) Abs_NA4))), pair(Nonce((absNA(pair(Agent(honest(a11)), Agent(dishonest(i12)))) Abs_NA5)), pair(Agent(honest(a12)), SymKey((absK(pair(Agent(honest(a13)), Agent(dishonest(i13)))) Abs_K1)))))), scrypt(SymKey((absK(pair(Agent(honest(a14)), Agent(dishonest(i14)))) Abs_K2)), f(Nonce((absNA(pair(Agent(honest(a15)), Agent(dishonest(i15)))) Abs_NA6)))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(2), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(honest(a3))), Agent(honest(a4)), Nonce((absNB(pair(Agent(honest(a5)), Agent(dishonest(i0)))) Abs_NB0)), crypt(pk(Agent(honest(a6))), pair(Nonce((absNB(pair(Agent(honest(a7)), Agent(dishonest(i1)))) Abs_NB1)), Agent(honest(a8)))), pair(Agent(honest(a9)), crypt(pk(Agent(honest(a10))), pair(Nonce((absNB(pair(Agent(honest(a11)), Agent(dishonest(i2)))) Abs_NB2)), Agent(honest(a12))))), Nonce((absNA(pair(Agent(honest(a13)), Agent(honest(a14)))) Abs_NA0)), SymKey((absK(pair(Agent(honest(a15)), Agent(honest(a16)))) Abs_K0)), crypt(pk(Agent(honest(a17))), pair(f(Nonce((absNB(pair(Agent(honest(a18)), Agent(dishonest(i3)))) Abs_NB3))), pair(Nonce((absNA(pair(Agent(honest(a19)), Agent(honest(a20)))) Abs_NA1)), pair(Agent(honest(a21)), SymKey((absK(pair(Agent(honest(a22)), Agent(honest(a23)))) Abs_K1)))))), scrypt(SymKey((absK(pair(Agent(honest(a24)), Agent(honest(a25)))) Abs_K2)), f(Nonce((absNA(pair(Agent(honest(a26)), Agent(honest(a27)))) Abs_NA2)))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(2), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(honest(a3))), Agent(honest(a4)), Nonce((absNA(pair(Agent(honest(a5)), Agent(dishonest(i0)))) Abs_NA0)), crypt(pk(Agent(honest(a6))), pair(Nonce((absNA(pair(Agent(honest(a7)), Agent(dishonest(i1)))) Abs_NA1)), Agent(honest(a8)))), pair(Agent(honest(a9)), crypt(pk(Agent(honest(a10))), pair(Nonce((absNA(pair(Agent(honest(a11)), Agent(dishonest(i2)))) Abs_NA2)), Agent(honest(a12))))), Nonce((absNA(pair(Agent(honest(a13)), Agent(honest(a14)))) Abs_NA3)), SymKey((absK(pair(Agent(honest(a15)), Agent(honest(a16)))) Abs_K0)), crypt(pk(Agent(honest(a17))), pair(f(Nonce((absNA(pair(Agent(honest(a18)), Agent(dishonest(i3)))) Abs_NA4))), pair(Nonce((absNA(pair(Agent(honest(a19)), Agent(honest(a20)))) Abs_NA5)), pair(Agent(honest(a21)), SymKey((absK(pair(Agent(honest(a22)), Agent(honest(a23)))) Abs_K1)))))), scrypt(SymKey((absK(pair(Agent(honest(a24)), Agent(honest(a25)))) Abs_K2)), f(Nonce((absNA(pair(Agent(honest(a26)), Agent(honest(a27)))) Abs_NA6)))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(2), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(honest(a3))), Agent(honest(a4)), Nonce((absNB(pair(Agent(honest(a5)), Agent(honest(a6)))) Abs_NB0)), crypt(pk(Agent(honest(a7))), pair(Nonce((absNB(pair(Agent(honest(a8)), Agent(honest(a9)))) Abs_NB1)), Agent(honest(a10)))), pair(Agent(honest(a11)), crypt(pk(Agent(honest(a12))), pair(Nonce((absNB(pair(Agent(honest(a13)), Agent(honest(a14)))) Abs_NB2)), Agent(honest(a15))))), Nonce((absNA(pair(Agent(honest(a16)), Agent(honest(a17)))) Abs_NA0)), SymKey((absK(pair(Agent(honest(a18)), Agent(honest(a19)))) Abs_K0)), crypt(pk(Agent(honest(a20))), pair(f(Nonce((absNB(pair(Agent(honest(a21)), Agent(honest(a22)))) Abs_NB3))), pair(Nonce((absNA(pair(Agent(honest(a23)), Agent(honest(a24)))) Abs_NA1)), pair(Agent(honest(a25)), SymKey((absK(pair(Agent(honest(a26)), Agent(honest(a27)))) Abs_K1)))))), scrypt(SymKey((absK(pair(Agent(honest(a28)), Agent(honest(a29)))) Abs_K2)), f(Nonce((absNA(pair(Agent(honest(a30)), Agent(honest(a31)))) Abs_NA2)))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(2), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), pk(Agent(honest(a3))), Agent(honest(a4)), Nonce((ni Abs_NI0)), crypt(pk(Agent(honest(a5))), pair(Nonce((ni Abs_NI1)), Agent(honest(a6)))), pair(Agent(honest(a7)), crypt(pk(Agent(honest(a8))), pair(Nonce((ni Abs_NI2)), Agent(honest(a9))))), Nonce((absNA(pair(Agent(honest(a10)), Agent(honest(a11)))) Abs_NA0)), SymKey((absK(pair(Agent(honest(a12)), Agent(honest(a13)))) Abs_K0)), crypt(pk(Agent(honest(a14))), pair(f(Nonce((ni Abs_NI3))), pair(Nonce((absNA(pair(Agent(honest(a15)), Agent(honest(a16)))) Abs_NA1)), pair(Agent(honest(a17)), SymKey((absK(pair(Agent(honest(a18)), Agent(honest(a19)))) Abs_K1)))))), scrypt(SymKey((absK(pair(Agent(honest(a20)), Agent(honest(a21)))) Abs_K2)), f(Nonce((absNA(pair(Agent(honest(a22)), Agent(honest(a23)))) Abs_NA2)))), SID(sid0)] ))
| (m = Iknows(f(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NB0)))))
| (m = Iknows(f(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NA0)))))
| (m = Iknows(pair(Agent(honest(a0)), crypt(pk(Agent(honest(a1))), pair(Nonce((absNB(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_NB0)), Agent(honest(a4)))))))
| (m = Iknows(pair(Agent(honest(a0)), crypt(pk(Agent(dishonest(i0))), pair(Nonce((absNB(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NB0)), Agent(honest(a2)))))))
| (m = Iknows(pair(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NB0)), Agent(honest(a1)))))
| (m = Iknows(pair(Agent(honest(a0)), SymKey((absK(pair(Agent(honest(a1)), Agent(dishonest(i0)))) Abs_K0)))))
| (m = Iknows(pair(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NA0)), pair(Agent(honest(a1)), SymKey((absK(pair(Agent(honest(a2)), Agent(dishonest(i1)))) Abs_K0))))))
| (m = Iknows(pair(f(Nonce((ni Abs_NI0))), pair(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NA0)), pair(Agent(honest(a1)), SymKey((absK(pair(Agent(honest(a2)), Agent(dishonest(i1)))) Abs_K0)))))))
| (m = Iknows(pair(f(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NB0))), pair(Nonce((absNA(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NA0)), pair(Agent(honest(a2)), SymKey((absK(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_K0)))))))
| (m = Iknows(pair(f(Nonce((absNA(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NA0))), pair(Nonce((absNA(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NA1)), pair(Agent(honest(a2)), SymKey((absK(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_K0)))))))
)}"
section {* Checking Fixed-point (BilateralKeyExchange) *}
lemma fp_attack_free: "~ (Attack m : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma init_0: "Iknows(Nonce((ni Abs_NI))) : BilateralKeyExchange_fp"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma init_1: "Iknows(Agent(dishonest(i))) : BilateralKeyExchange_fp"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma init_2: "State(rA, [Agent(honest(a)), Step(0), inv(pk(Agent(honest(a)))), pk(Agent(dishonest(i))), pk(Agent(honest(a))), Agent(dishonest(i)), SID(sid)] ) : BilateralKeyExchange_fp"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma init_3: "State(rA, [Agent(honest(a)), Step(0), inv(pk(Agent(honest(a)))), pk(Agent(honest(a))), pk(Agent(honest(a))), Agent(honest(a)), SID(sid)] ) : BilateralKeyExchange_fp"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma init_4: "Iknows(Step(0)) : BilateralKeyExchange_fp"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma init_5: "Iknows(inv(pk(Agent(dishonest(i))))) : BilateralKeyExchange_fp"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma init_6: "Iknows(pk(Agent(dishonest(i)))) : BilateralKeyExchange_fp"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma init_7: "Iknows(SID(sid)) : BilateralKeyExchange_fp"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma init_8: "Iknows(pk(Agent(honest(a)))) : BilateralKeyExchange_fp"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma init_9: "Iknows(Agent(honest(a))) : BilateralKeyExchange_fp"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma init_10: "State(rB, [Agent(honest(a)), Step(0), inv(pk(Agent(honest(a)))), pk(Agent(honest(a))), pk(Agent(dishonest(i))), Agent(dishonest(i)), SID(sid)] ) : BilateralKeyExchange_fp"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma init_11: "State(rB, [Agent(honest(a)), Step(0), inv(pk(Agent(honest(a)))), pk(Agent(honest(a))), pk(Agent(honest(a))), Agent(honest(a)), SID(sid)] ) : BilateralKeyExchange_fp"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_0: "[|
Iknows(crypt(K, M)) : BilateralKeyExchange_fp;
Iknows(inv(K)) : BilateralKeyExchange_fp|]
==>
(Iknows(M) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_1: "[|
Iknows(crypt(inv(K), M)) : BilateralKeyExchange_fp;
Iknows(K) : BilateralKeyExchange_fp|]
==>
(Iknows(M) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_2: "[|
Iknows(scrypt(K, M)) : BilateralKeyExchange_fp;
Iknows(K) : BilateralKeyExchange_fp|]
==>
(Iknows(M) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_3: "[|
Iknows(pair(M1, M2)) : BilateralKeyExchange_fp|]
==>
(Iknows(M1) : BilateralKeyExchange_fp) &
(Iknows(M2) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_4: "[|
Secret(M, Agent(honest(a))) : BilateralKeyExchange_fp;
Iknows(M) : BilateralKeyExchange_fp|]
==>
(Attack(pair(secrecy, M)) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_5: "[|
Request(A, B, Purpose(purposeNB), M, SID(sid)) : BilateralKeyExchange_fp;
~ ( ? i .
B = Agent(dishonest(i)));
~ ( ? B A Abs_NB .
M = Nonce((absNB(pair(B, A)) Abs_NB)))|]
==>
(Attack(pair(authentication, pair(A, pair(B, M)))) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_6: "[|
Request(A, B, Purpose(purposeNA), M, SID(sid)) : BilateralKeyExchange_fp;
~ ( ? i .
B = Agent(dishonest(i)));
~ ( ? B A Abs_NA .
M = Nonce((absNA(pair(B, A)) Abs_NA)))|]
==>
(Attack(pair(authentication, pair(A, pair(B, M)))) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_7: "[|
Request(A, B, Purpose(purposeK), M, SID(sid)) : BilateralKeyExchange_fp;
~ ( ? i .
B = Agent(dishonest(i)));
~ ( ? B A Abs_K .
M = SymKey((absK(pair(B, A)) Abs_K)))|]
==>
(Attack(pair(authentication, pair(A, pair(B, M)))) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_8: "[|
State(rB, [Agent(B), Step(0), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), SID(sid)] ) : BilateralKeyExchange_fp|]
==>
(State(rB, [Agent(B), Step(1), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce((absNB(pair(Agent(B), Agent(A))) Abs_NB)), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce((absNB(pair(Agent(B), Agent(A))) Abs_NB)), Agent(B)))), SID(sid)] ) : BilateralKeyExchange_fp) &
(Iknows(pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce((absNB(pair(Agent(B), Agent(A))) Abs_NB)), Agent(B))))) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_9: "[|
State(rA, [Agent(A), Step(0), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), SID(sid)] ) : BilateralKeyExchange_fp;
Iknows(Agent(B)) : BilateralKeyExchange_fp;
Iknows(crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))) : BilateralKeyExchange_fp|]
==>
(Secret(SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)), Agent(B)) : BilateralKeyExchange_fp) &
(Witness(Agent(A), Agent(B), Purpose(purposeK), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K))) : BilateralKeyExchange_fp) &
(State(rA, [Agent(A), Step(1), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), pair(Agent(A), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)))))), SID(sid)] ) : BilateralKeyExchange_fp) &
(Iknows(crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), pair(Agent(A), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K))))))) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_10: "[|
State(rA, [Agent(A), Step(0), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), SID(sid)] ) : BilateralKeyExchange_fp;
Iknows(Agent(B)) : BilateralKeyExchange_fp;
Iknows(pk(Agent(A))) : BilateralKeyExchange_fp;
Iknows(Nonce(NB)) : BilateralKeyExchange_fp|]
==>
(Secret(SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)), Agent(B)) : BilateralKeyExchange_fp) &
(Witness(Agent(A), Agent(B), Purpose(purposeK), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K))) : BilateralKeyExchange_fp) &
(State(rA, [Agent(A), Step(1), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), pair(Agent(A), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)))))), SID(sid)] ) : BilateralKeyExchange_fp) &
(Iknows(crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), pair(Agent(A), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K))))))) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_11: "[|
State(rA, [Agent(A), Step(0), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), SID(sid)] ) : BilateralKeyExchange_fp;
Iknows(Agent(B)) : BilateralKeyExchange_fp;
Iknows(Agent(A)) : BilateralKeyExchange_fp;
Iknows(Nonce(NB)) : BilateralKeyExchange_fp|]
==>
(Secret(SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)), Agent(B)) : BilateralKeyExchange_fp) &
(Witness(Agent(A), Agent(B), Purpose(purposeK), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K))) : BilateralKeyExchange_fp) &
(State(rA, [Agent(A), Step(1), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), pair(Agent(A), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K)))))), SID(sid)] ) : BilateralKeyExchange_fp) &
(Iknows(crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce((absNA(pair(Agent(A), Agent(B))) Abs_NA)), pair(Agent(A), SymKey((absK(pair(Agent(A), Agent(B))) Abs_K))))))) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_12: "[|
State(rB, [Agent(B), Step(1), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), SID(sid)] ) : BilateralKeyExchange_fp;
Iknows(crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K)))))) : BilateralKeyExchange_fp|]
==>
(Request(Agent(B), Agent(A), Purpose(purposeK), SymKey(K), SID(sid)) : BilateralKeyExchange_fp) &
(State(rB, [Agent(B), Step(2), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), SymKey(K), Nonce(NA), f(Nonce(NB)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ) : BilateralKeyExchange_fp) &
(Iknows(scrypt(SymKey(K), f(Nonce(NA)))) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_13: "[|
State(rB, [Agent(B), Step(1), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), SID(sid)] ) : BilateralKeyExchange_fp;
Iknows(pk(Agent(B))) : BilateralKeyExchange_fp;
Iknows(f(Nonce(NB))) : BilateralKeyExchange_fp;
Iknows(Nonce(NA)) : BilateralKeyExchange_fp;
Iknows(Agent(A)) : BilateralKeyExchange_fp;
Iknows(SymKey(K)) : BilateralKeyExchange_fp|]
==>
(Request(Agent(B), Agent(A), Purpose(purposeK), SymKey(K), SID(sid)) : BilateralKeyExchange_fp) &
(State(rB, [Agent(B), Step(2), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), SymKey(K), Nonce(NA), f(Nonce(NB)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ) : BilateralKeyExchange_fp) &
(Iknows(scrypt(SymKey(K), f(Nonce(NA)))) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_14: "[|
State(rB, [Agent(B), Step(1), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), SID(sid)] ) : BilateralKeyExchange_fp;
Iknows(pk(Agent(B))) : BilateralKeyExchange_fp;
Iknows(Nonce(NB)) : BilateralKeyExchange_fp;
Iknows(Nonce(NA)) : BilateralKeyExchange_fp;
Iknows(Agent(A)) : BilateralKeyExchange_fp;
Iknows(SymKey(K)) : BilateralKeyExchange_fp|]
==>
(Request(Agent(B), Agent(A), Purpose(purposeK), SymKey(K), SID(sid)) : BilateralKeyExchange_fp) &
(State(rB, [Agent(B), Step(2), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), SymKey(K), Nonce(NA), f(Nonce(NB)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ) : BilateralKeyExchange_fp) &
(Iknows(scrypt(SymKey(K), f(Nonce(NA)))) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_15: "[|
State(rB, [Agent(B), Step(1), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), SID(sid)] ) : BilateralKeyExchange_fp;
Iknows(Agent(B)) : BilateralKeyExchange_fp;
Iknows(f(Nonce(NB))) : BilateralKeyExchange_fp;
Iknows(Nonce(NA)) : BilateralKeyExchange_fp;
Iknows(Agent(A)) : BilateralKeyExchange_fp;
Iknows(SymKey(K)) : BilateralKeyExchange_fp|]
==>
(Request(Agent(B), Agent(A), Purpose(purposeK), SymKey(K), SID(sid)) : BilateralKeyExchange_fp) &
(State(rB, [Agent(B), Step(2), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), SymKey(K), Nonce(NA), f(Nonce(NB)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ) : BilateralKeyExchange_fp) &
(Iknows(scrypt(SymKey(K), f(Nonce(NA)))) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_16: "[|
State(rB, [Agent(B), Step(1), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), SID(sid)] ) : BilateralKeyExchange_fp;
Iknows(Agent(B)) : BilateralKeyExchange_fp;
Iknows(Nonce(NB)) : BilateralKeyExchange_fp;
Iknows(Nonce(NA)) : BilateralKeyExchange_fp;
Iknows(Agent(A)) : BilateralKeyExchange_fp;
Iknows(SymKey(K)) : BilateralKeyExchange_fp|]
==>
(Request(Agent(B), Agent(A), Purpose(purposeK), SymKey(K), SID(sid)) : BilateralKeyExchange_fp) &
(State(rB, [Agent(B), Step(2), inv(pk(Agent(B))), pk(Agent(B)), pk(Agent(A)), Agent(A), Nonce(NB), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), SymKey(K), Nonce(NA), f(Nonce(NB)), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ) : BilateralKeyExchange_fp) &
(Iknows(scrypt(SymKey(K), f(Nonce(NA)))) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_17: "[|
State(rA, [Agent(A), Step(1), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce(NA), SymKey(K), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), SID(sid)] ) : BilateralKeyExchange_fp;
Iknows(scrypt(SymKey(K), f(Nonce(NA)))) : BilateralKeyExchange_fp|]
==>
(State(rA, [Agent(A), Step(2), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce(NA), SymKey(K), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_18: "[|
State(rA, [Agent(A), Step(1), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce(NA), SymKey(K), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), SID(sid)] ) : BilateralKeyExchange_fp;
Iknows(SymKey(K)) : BilateralKeyExchange_fp;
Iknows(f(Nonce(NA))) : BilateralKeyExchange_fp|]
==>
(State(rA, [Agent(A), Step(2), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce(NA), SymKey(K), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_19: "[|
State(rA, [Agent(A), Step(1), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce(NA), SymKey(K), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), SID(sid)] ) : BilateralKeyExchange_fp;
Iknows(SymKey(K)) : BilateralKeyExchange_fp;
Iknows(Nonce(NA)) : BilateralKeyExchange_fp|]
==>
(State(rA, [Agent(A), Step(2), inv(pk(Agent(A))), pk(Agent(B)), pk(Agent(A)), Agent(B), Nonce(NB), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B))), pair(Agent(B), crypt(pk(Agent(A)), pair(Nonce(NB), Agent(B)))), Nonce(NA), SymKey(K), crypt(pk(Agent(B)), pair(f(Nonce(NB)), pair(Nonce(NA), pair(Agent(A), SymKey(K))))), scrypt(SymKey(K), f(Nonce(NA))), SID(sid)] ) : BilateralKeyExchange_fp)"
by(simp only: BilateralKeyExchange_fp_def, simp only: set2pred, simp, auto?)+
section {* Security Proof(s) (BilateralKeyExchange) *}
lemma over_approx: "t : BilateralKeyExchange ==> (set t) <= BilateralKeyExchange_fp"
apply(rule BilateralKeyExchange.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 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)+)
apply(propagate_fp, cut_tac rule_15, (assumption | simp)+)
apply(propagate_fp, cut_tac rule_16, (assumption | simp)+)
apply(propagate_fp, cut_tac rule_17, (assumption | simp)+)
apply(propagate_fp, cut_tac rule_18, (assumption | simp)+)
apply(propagate_fp, cut_tac rule_19, (assumption | simp)+)
done
end (* theory *)