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/ISOsymKeyTwoPassUnilateralA...

378 lines
28 KiB
Plaintext

chapter {* Analysing ISO_twopass_symm *}
(* ***********************************
This file is automatically generated from the AnB file "AnB/ISOsymKeyTwoPassUnilateralAuthProt.AnB".
Backend: Open Source Fixedpoint Model Checker version 2009c
************************************ *)
theory
"ISOsymKeyTwoPassUnilateralAuthProt"
imports
"../src/ofmc"
begin
section {* Protocol Model (ISO_twopass_symm) *}
datatype Role = rA | rB
datatype Purpose = purposeNI | purposeNB | purposeText1 | purposeText2 | purposeText3
datatype Agent = honest nat
| dishonest nat
datatype Nonce = "ni" "nat"
| "absNB" "Msg" "nat"
| "absText2" "Msg" "nat"
| "NI"
| "NB"
| "Text1"
| "Text2"
| "Text3"
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"
(* Functions *)
| "sk" "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 (ISO_twopass_symm) *}
inductive_set
ISO_twopass_symm::"Fact list set"
where
init_0: "[ Iknows(Nonce((ni Abs_NI)))] : ISO_twopass_symm"
| init_1: "[ Iknows(Agent(dishonest(i)))] : ISO_twopass_symm"
| init_2: "[ State(rA, [Agent(honest(a)), Step(0), SymKey(sk(pair(Agent(honest(a)), Agent(dishonest(i))))), Agent(dishonest(i)), SID(sid)] )] : ISO_twopass_symm"
| init_3: "[ State(rA, [Agent(honest(a)), Step(0), SymKey(sk(pair(Agent(honest(a)), Agent(honest(a))))), Agent(honest(a)), SID(sid)] )] : ISO_twopass_symm"
| init_4: "[ Iknows(Step(0))] : ISO_twopass_symm"
| init_5: "[ Iknows(SymKey(sk(pair(Agent(dishonest(i)), Agent(dishonest(i))))))] : ISO_twopass_symm"
| init_6: "[ Iknows(SID(sid))] : ISO_twopass_symm"
| init_7: "[ Iknows(SymKey(sk(pair(Agent(dishonest(i)), Agent(honest(a))))))] : ISO_twopass_symm"
| init_8: "[ Iknows(Agent(honest(a)))] : ISO_twopass_symm"
| init_9: "[ State(rB, [Agent(honest(a)), Step(0), SymKey(sk(pair(Agent(dishonest(i)), Agent(honest(a))))), Agent(dishonest(i)), SID(sid)] )] : ISO_twopass_symm"
| init_10: "[ State(rB, [Agent(honest(a)), Step(0), SymKey(sk(pair(Agent(honest(a)), Agent(honest(a))))), Agent(honest(a)), SID(sid)] )] : ISO_twopass_symm"
| init_11: "[ Iknows(SymKey(sk(pair(Agent(honest(a)), Agent(dishonest(i))))))] : ISO_twopass_symm"
| rule_0: "[| t :ISO_twopass_symm;
Iknows(crypt(K, M)) : (set t);
Iknows(inv(K)) : (set t)|]
==>
((Iknows(M))
#t) : ISO_twopass_symm"
| rule_1: "[| t :ISO_twopass_symm;
Iknows(crypt(inv(K), M)) : (set t);
Iknows(K) : (set t)|]
==>
((Iknows(M))
#t) : ISO_twopass_symm"
| rule_2: "[| t :ISO_twopass_symm;
Iknows(scrypt(K, M)) : (set t);
Iknows(K) : (set t)|]
==>
((Iknows(M))
#t) : ISO_twopass_symm"
| rule_3: "[| t :ISO_twopass_symm;
Iknows(pair(M1, M2)) : (set t)|]
==>
((Iknows(M1))
#(Iknows(M2))
#t) : ISO_twopass_symm"
| rule_4: "[| t :ISO_twopass_symm;
Secret(M, Agent(honest(a))) : (set t);
Iknows(M) : (set t)|]
==>
((Attack(pair(secrecy, M)))
#t) : ISO_twopass_symm"
| rule_5: "[| t :ISO_twopass_symm;
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) : ISO_twopass_symm"
| rule_6: "[| t :ISO_twopass_symm;
Request(A, B, Purpose(purposeText2), M, SID(sid)) : (set t);
~ ( ? i .
B = Agent(dishonest(i)));
~ ( ? B A Abs_Text2 .
M = Nonce((absText2(pair(B, A)) Abs_Text2)))|]
==>
((Attack(pair(authentication, pair(A, pair(B, M)))))
#t) : ISO_twopass_symm"
| rule_7: "[| t :ISO_twopass_symm;
State(rB, [Agent(B), Step(0), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(A), SID(sid)] ) : (set t)|]
==>
((State(rB, [Agent(B), Step(1), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(A), Nonce((absNB(pair(Agent(B), Agent(A))) Abs_NB)), SID(sid)] ))
#(Iknows(Nonce((absNB(pair(Agent(B), Agent(A))) Abs_NB))))
#t) : ISO_twopass_symm"
| rule_8: "[| t :ISO_twopass_symm;
State(rA, [Agent(A), Step(0), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(B), SID(sid)] ) : (set t);
Iknows(Nonce(NB)) : (set t)|]
==>
((Witness(Agent(A), Agent(B), Purpose(purposeText2), Nonce((absText2(pair(Agent(A), Agent(B))) Abs_Text2))))
#(State(rA, [Agent(A), Step(1), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(B), Nonce(NB), Nonce((absText2(pair(Agent(A), Agent(B))) Abs_Text2)), scrypt(SymKey(sk(pair(Agent(A), Agent(B)))), pair(Nonce(NB), pair(Agent(B), Nonce((absText2(pair(Agent(A), Agent(B))) Abs_Text2))))), SID(sid)] ))
#(Iknows(scrypt(SymKey(sk(pair(Agent(A), Agent(B)))), pair(Nonce(NB), pair(Agent(B), Nonce((absText2(pair(Agent(A), Agent(B))) Abs_Text2)))))))
#t) : ISO_twopass_symm"
| rule_9: "[| t :ISO_twopass_symm;
State(rB, [Agent(B), Step(1), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(A), Nonce(NB), SID(sid)] ) : (set t);
Iknows(scrypt(SymKey(sk(pair(Agent(A), Agent(B)))), pair(Nonce(NB), pair(Agent(B), Nonce(Text2))))) : (set t)|]
==>
((Request(Agent(B), Agent(A), Purpose(purposeText2), Nonce(Text2), SID(sid)))
#(State(rB, [Agent(B), Step(2), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(A), Nonce(NB), Nonce(Text2), scrypt(SymKey(sk(pair(Agent(A), Agent(B)))), pair(Nonce(NB), pair(Agent(B), Nonce(Text2)))), SID(sid)] ))
#t) : ISO_twopass_symm"
| rule_10: "[| t :ISO_twopass_symm;
State(rB, [Agent(B), Step(1), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(A), Nonce(NB), SID(sid)] ) : (set t);
Iknows(SymKey(sk(pair(Agent(A), Agent(B))))) : (set t);
Iknows(Nonce(NB)) : (set t);
Iknows(Agent(B)) : (set t);
Iknows(Nonce(Text2)) : (set t)|]
==>
((Request(Agent(B), Agent(A), Purpose(purposeText2), Nonce(Text2), SID(sid)))
#(State(rB, [Agent(B), Step(2), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(A), Nonce(NB), Nonce(Text2), scrypt(SymKey(sk(pair(Agent(A), Agent(B)))), pair(Nonce(NB), pair(Agent(B), Nonce(Text2)))), SID(sid)] ))
#t) : ISO_twopass_symm"
section {* Fixed-point Definition (ISO_twopass_symm) *}
definition
"ISO_twopass_symm_fp = {m. ( ? Abs_NB2 Abs_NB3 Abs_NI1 i7 Abs_Text22 Abs_Text23 a8 a9 a10 a11 a12 a13 a14 i4 i5 Abs_NB1 a6 a7 i6 sid0 a3 a4 a5 i3 Abs_NI0 Abs_NB0 a2 a0 i0 Abs_Text20 i1 a1 i2 Abs_Text21 .
(m = Iknows(Nonce((ni Abs_NI0))))
| (m = Iknows(Agent(dishonest(i0))))
| (m = State(rA, [Agent(honest(a0)), Step(0), SymKey(sk(pair(Agent(honest(a1)), Agent(dishonest(i0))))), Agent(dishonest(i1)), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(0), SymKey(sk(pair(Agent(honest(a1)), Agent(honest(a2))))), Agent(honest(a3)), SID(sid0)] ))
| (m = Iknows(Step(0)))
| (m = Iknows(SymKey(sk(pair(Agent(dishonest(i0)), Agent(dishonest(i1)))))))
| (m = Iknows(SID(sid0)))
| (m = Iknows(SymKey(sk(pair(Agent(dishonest(i0)), Agent(honest(a0)))))))
| (m = Iknows(Agent(honest(a0))))
| (m = State(rB, [Agent(honest(a0)), Step(0), SymKey(sk(pair(Agent(dishonest(i0)), Agent(honest(a1))))), Agent(dishonest(i1)), SID(sid0)] ))
| (m = State(rB, [Agent(honest(a0)), Step(0), SymKey(sk(pair(Agent(honest(a1)), Agent(honest(a2))))), Agent(honest(a3)), SID(sid0)] ))
| (m = Iknows(SymKey(sk(pair(Agent(honest(a0)), Agent(dishonest(i0)))))))
| (m = State(rB, [Agent(honest(a0)), Step(1), SymKey(sk(pair(Agent(honest(a1)), Agent(honest(a2))))), Agent(honest(a3)), Nonce((absNB(pair(Agent(honest(a4)), Agent(honest(a5)))) Abs_NB0)), SID(sid0)] ))
| (m = State(rB, [Agent(honest(a0)), Step(1), SymKey(sk(pair(Agent(dishonest(i0)), Agent(honest(a1))))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a2)), Agent(dishonest(i2)))) Abs_NB0)), SID(sid0)] ))
| (m = Witness(Agent(honest(a0)), Agent(dishonest(i0)), Purpose(purposeText2), Nonce((absText2(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_Text20))))
| (m = State(rA, [Agent(honest(a0)), Step(1), SymKey(sk(pair(Agent(honest(a1)), Agent(dishonest(i0))))), Agent(dishonest(i1)), Nonce((ni Abs_NI0)), Nonce((absText2(pair(Agent(honest(a2)), Agent(dishonest(i2)))) Abs_Text20)), scrypt(SymKey(sk(pair(Agent(honest(a3)), Agent(dishonest(i3))))), pair(Nonce((ni Abs_NI1)), pair(Agent(dishonest(i4)), Nonce((absText2(pair(Agent(honest(a4)), Agent(dishonest(i5)))) Abs_Text21))))), SID(sid0)] ))
| (m = Witness(Agent(honest(a0)), Agent(honest(a1)), Purpose(purposeText2), Nonce((absText2(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_Text20))))
| (m = State(rA, [Agent(honest(a0)), Step(1), SymKey(sk(pair(Agent(honest(a1)), Agent(honest(a2))))), Agent(honest(a3)), Nonce((ni Abs_NI0)), Nonce((absText2(pair(Agent(honest(a4)), Agent(honest(a5)))) Abs_Text20)), scrypt(SymKey(sk(pair(Agent(honest(a6)), Agent(honest(a7))))), pair(Nonce((ni Abs_NI1)), pair(Agent(honest(a8)), Nonce((absText2(pair(Agent(honest(a9)), Agent(honest(a10)))) Abs_Text21))))), SID(sid0)] ))
| (m = Iknows(scrypt(SymKey(sk(pair(Agent(honest(a0)), Agent(honest(a1))))), pair(Nonce((ni Abs_NI0)), pair(Agent(honest(a2)), Nonce((absText2(pair(Agent(honest(a3)), Agent(honest(a4)))) Abs_Text20)))))))
| (m = Iknows(scrypt(SymKey(sk(pair(Agent(honest(a0)), Agent(dishonest(i0))))), pair(Nonce((ni Abs_NI0)), pair(Agent(dishonest(i1)), Nonce((absText2(pair(Agent(honest(a1)), Agent(dishonest(i2)))) Abs_Text20)))))))
| (m = Iknows(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NB0))))
| (m = Iknows(Nonce((absNB(pair(Agent(honest(a0)), Agent(honest(a1)))) Abs_NB0))))
| (m = Iknows(pair(Agent(dishonest(i0)), Nonce((absText2(pair(Agent(honest(a0)), Agent(dishonest(i1)))) Abs_Text20)))))
| (m = Iknows(pair(Nonce((ni Abs_NI0)), pair(Agent(dishonest(i0)), Nonce((absText2(pair(Agent(honest(a0)), Agent(dishonest(i1)))) Abs_Text20))))))
| (m = State(rA, [Agent(honest(a0)), Step(1), SymKey(sk(pair(Agent(honest(a1)), Agent(dishonest(i0))))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a2)), Agent(dishonest(i2)))) Abs_NB0)), Nonce((absText2(pair(Agent(honest(a3)), Agent(dishonest(i3)))) Abs_Text20)), scrypt(SymKey(sk(pair(Agent(honest(a4)), Agent(dishonest(i4))))), pair(Nonce((absNB(pair(Agent(honest(a5)), Agent(dishonest(i5)))) Abs_NB1)), pair(Agent(dishonest(i6)), Nonce((absText2(pair(Agent(honest(a6)), Agent(dishonest(i7)))) Abs_Text21))))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(1), SymKey(sk(pair(Agent(honest(a1)), Agent(dishonest(i0))))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_NB0)), Nonce((absText2(pair(Agent(honest(a4)), Agent(dishonest(i2)))) Abs_Text20)), scrypt(SymKey(sk(pair(Agent(honest(a5)), Agent(dishonest(i3))))), pair(Nonce((absNB(pair(Agent(honest(a6)), Agent(honest(a7)))) Abs_NB1)), pair(Agent(dishonest(i4)), Nonce((absText2(pair(Agent(honest(a8)), Agent(dishonest(i5)))) Abs_Text21))))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(1), SymKey(sk(pair(Agent(honest(a1)), Agent(honest(a2))))), Agent(honest(a3)), Nonce((absNB(pair(Agent(honest(a4)), Agent(dishonest(i0)))) Abs_NB0)), Nonce((absText2(pair(Agent(honest(a5)), Agent(honest(a6)))) Abs_Text20)), scrypt(SymKey(sk(pair(Agent(honest(a7)), Agent(honest(a8))))), pair(Nonce((absNB(pair(Agent(honest(a9)), Agent(dishonest(i1)))) Abs_NB1)), pair(Agent(honest(a10)), Nonce((absText2(pair(Agent(honest(a11)), Agent(honest(a12)))) Abs_Text21))))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(1), SymKey(sk(pair(Agent(honest(a1)), Agent(honest(a2))))), Agent(honest(a3)), Nonce((absNB(pair(Agent(honest(a4)), Agent(honest(a5)))) Abs_NB0)), Nonce((absText2(pair(Agent(honest(a6)), Agent(honest(a7)))) Abs_Text20)), scrypt(SymKey(sk(pair(Agent(honest(a8)), Agent(honest(a9))))), pair(Nonce((absNB(pair(Agent(honest(a10)), Agent(honest(a11)))) Abs_NB1)), pair(Agent(honest(a12)), Nonce((absText2(pair(Agent(honest(a13)), Agent(honest(a14)))) Abs_Text21))))), SID(sid0)] ))
| (m = Request(Agent(honest(a0)), Agent(dishonest(i0)), Purpose(purposeText2), Nonce((absNB(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NB0)), SID(sid0)))
| (m = State(rB, [Agent(honest(a0)), Step(2), SymKey(sk(pair(Agent(dishonest(i0)), Agent(honest(a1))))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a2)), Agent(dishonest(i2)))) Abs_NB0)), Nonce((absNB(pair(Agent(honest(a3)), Agent(dishonest(i3)))) Abs_NB1)), scrypt(SymKey(sk(pair(Agent(dishonest(i4)), Agent(honest(a4))))), pair(Nonce((absNB(pair(Agent(honest(a5)), Agent(dishonest(i5)))) Abs_NB2)), pair(Agent(honest(a6)), Nonce((absNB(pair(Agent(honest(a7)), Agent(dishonest(i6)))) Abs_NB3))))), SID(sid0)] ))
| (m = Request(Agent(honest(a0)), Agent(dishonest(i0)), Purpose(purposeText2), Nonce((absNB(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_NB0)), SID(sid0)))
| (m = State(rB, [Agent(honest(a0)), Step(2), SymKey(sk(pair(Agent(dishonest(i0)), Agent(honest(a1))))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a2)), Agent(dishonest(i2)))) Abs_NB0)), Nonce((absNB(pair(Agent(honest(a3)), Agent(honest(a4)))) Abs_NB1)), scrypt(SymKey(sk(pair(Agent(dishonest(i3)), Agent(honest(a5))))), pair(Nonce((absNB(pair(Agent(honest(a6)), Agent(dishonest(i4)))) Abs_NB2)), pair(Agent(honest(a7)), Nonce((absNB(pair(Agent(honest(a8)), Agent(honest(a9)))) Abs_NB3))))), SID(sid0)] ))
| (m = Request(Agent(honest(a0)), Agent(dishonest(i0)), Purpose(purposeText2), Nonce((ni Abs_NI0)), SID(sid0)))
| (m = State(rB, [Agent(honest(a0)), Step(2), SymKey(sk(pair(Agent(dishonest(i0)), Agent(honest(a1))))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a2)), Agent(dishonest(i2)))) Abs_NB0)), Nonce((ni Abs_NI0)), scrypt(SymKey(sk(pair(Agent(dishonest(i3)), Agent(honest(a3))))), pair(Nonce((absNB(pair(Agent(honest(a4)), Agent(dishonest(i4)))) Abs_NB1)), pair(Agent(honest(a5)), Nonce((ni Abs_NI1))))), SID(sid0)] ))
| (m = Iknows(scrypt(SymKey(sk(pair(Agent(honest(a0)), Agent(honest(a1))))), pair(Nonce((absNB(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_NB0)), pair(Agent(honest(a4)), Nonce((absText2(pair(Agent(honest(a5)), Agent(honest(a6)))) Abs_Text20)))))))
| (m = Iknows(scrypt(SymKey(sk(pair(Agent(honest(a0)), Agent(honest(a1))))), pair(Nonce((absNB(pair(Agent(honest(a2)), Agent(dishonest(i0)))) Abs_NB0)), pair(Agent(honest(a3)), Nonce((absText2(pair(Agent(honest(a4)), Agent(honest(a5)))) Abs_Text20)))))))
| (m = Iknows(scrypt(SymKey(sk(pair(Agent(honest(a0)), Agent(dishonest(i0))))), pair(Nonce((absNB(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_NB0)), pair(Agent(dishonest(i1)), Nonce((absText2(pair(Agent(honest(a3)), Agent(dishonest(i2)))) Abs_Text20)))))))
| (m = Iknows(scrypt(SymKey(sk(pair(Agent(honest(a0)), Agent(dishonest(i0))))), pair(Nonce((absNB(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_NB0)), pair(Agent(dishonest(i2)), Nonce((absText2(pair(Agent(honest(a2)), Agent(dishonest(i3)))) Abs_Text20)))))))
| (m = Iknows(Nonce((absText2(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_Text20))))
| (m = Iknows(pair(Agent(dishonest(i0)), Nonce((absText2(pair(Agent(honest(a0)), Agent(dishonest(i1)))) Abs_Text20)))))
| (m = Iknows(pair(Nonce((ni Abs_NI0)), pair(Agent(dishonest(i0)), Nonce((absText2(pair(Agent(honest(a0)), Agent(dishonest(i1)))) Abs_Text20))))))
| (m = Iknows(pair(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NB0)), pair(Agent(dishonest(i1)), Nonce((absText2(pair(Agent(honest(a1)), Agent(dishonest(i2)))) Abs_Text20))))))
| (m = Iknows(pair(Nonce((absNB(pair(Agent(honest(a0)), Agent(honest(a1)))) Abs_NB0)), pair(Agent(dishonest(i0)), Nonce((absText2(pair(Agent(honest(a2)), Agent(dishonest(i1)))) Abs_Text20))))))
| (m = State(rA, [Agent(honest(a0)), Step(1), SymKey(sk(pair(Agent(honest(a1)), Agent(dishonest(i0))))), Agent(dishonest(i1)), Nonce((absText2(pair(Agent(honest(a2)), Agent(dishonest(i2)))) Abs_Text20)), Nonce((absText2(pair(Agent(honest(a3)), Agent(dishonest(i3)))) Abs_Text21)), scrypt(SymKey(sk(pair(Agent(honest(a4)), Agent(dishonest(i4))))), pair(Nonce((absText2(pair(Agent(honest(a5)), Agent(dishonest(i5)))) Abs_Text22)), pair(Agent(dishonest(i6)), Nonce((absText2(pair(Agent(honest(a6)), Agent(dishonest(i7)))) Abs_Text23))))), SID(sid0)] ))
| (m = State(rA, [Agent(honest(a0)), Step(1), SymKey(sk(pair(Agent(honest(a1)), Agent(honest(a2))))), Agent(honest(a3)), Nonce((absText2(pair(Agent(honest(a4)), Agent(dishonest(i0)))) Abs_Text20)), Nonce((absText2(pair(Agent(honest(a5)), Agent(honest(a6)))) Abs_Text21)), scrypt(SymKey(sk(pair(Agent(honest(a7)), Agent(honest(a8))))), pair(Nonce((absText2(pair(Agent(honest(a9)), Agent(dishonest(i1)))) Abs_Text22)), pair(Agent(honest(a10)), Nonce((absText2(pair(Agent(honest(a11)), Agent(honest(a12)))) Abs_Text23))))), SID(sid0)] ))
| (m = Request(Agent(honest(a0)), Agent(honest(a1)), Purpose(purposeText2), Nonce((absText2(pair(Agent(honest(a2)), Agent(honest(a3)))) Abs_Text20)), SID(sid0)))
| (m = State(rB, [Agent(honest(a0)), Step(2), SymKey(sk(pair(Agent(honest(a1)), Agent(honest(a2))))), Agent(honest(a3)), Nonce((absNB(pair(Agent(honest(a4)), Agent(honest(a5)))) Abs_NB0)), Nonce((absText2(pair(Agent(honest(a6)), Agent(honest(a7)))) Abs_Text20)), scrypt(SymKey(sk(pair(Agent(honest(a8)), Agent(honest(a9))))), pair(Nonce((absNB(pair(Agent(honest(a10)), Agent(honest(a11)))) Abs_NB1)), pair(Agent(honest(a12)), Nonce((absText2(pair(Agent(honest(a13)), Agent(honest(a14)))) Abs_Text21))))), SID(sid0)] ))
| (m = Request(Agent(honest(a0)), Agent(dishonest(i0)), Purpose(purposeText2), Nonce((absText2(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_Text20)), SID(sid0)))
| (m = State(rB, [Agent(honest(a0)), Step(2), SymKey(sk(pair(Agent(dishonest(i0)), Agent(honest(a1))))), Agent(dishonest(i1)), Nonce((absNB(pair(Agent(honest(a2)), Agent(dishonest(i2)))) Abs_NB0)), Nonce((absText2(pair(Agent(honest(a3)), Agent(dishonest(i3)))) Abs_Text20)), scrypt(SymKey(sk(pair(Agent(dishonest(i4)), Agent(honest(a4))))), pair(Nonce((absNB(pair(Agent(honest(a5)), Agent(dishonest(i5)))) Abs_NB1)), pair(Agent(honest(a6)), Nonce((absText2(pair(Agent(honest(a7)), Agent(dishonest(i6)))) Abs_Text21))))), SID(sid0)] ))
| (m = Iknows(scrypt(SymKey(sk(pair(Agent(honest(a0)), Agent(honest(a1))))), pair(Nonce((absText2(pair(Agent(honest(a2)), Agent(dishonest(i0)))) Abs_Text20)), pair(Agent(honest(a3)), Nonce((absText2(pair(Agent(honest(a4)), Agent(honest(a5)))) Abs_Text21)))))))
| (m = Iknows(scrypt(SymKey(sk(pair(Agent(honest(a0)), Agent(dishonest(i0))))), pair(Nonce((absText2(pair(Agent(honest(a1)), Agent(dishonest(i1)))) Abs_Text20)), pair(Agent(dishonest(i2)), Nonce((absText2(pair(Agent(honest(a2)), Agent(dishonest(i3)))) Abs_Text21)))))))
| (m = Iknows(pair(Agent(dishonest(i0)), Nonce((absText2(pair(Agent(honest(a0)), Agent(dishonest(i1)))) Abs_Text20)))))
| (m = Iknows(pair(Nonce((ni Abs_NI0)), pair(Agent(dishonest(i0)), Nonce((absText2(pair(Agent(honest(a0)), Agent(dishonest(i1)))) Abs_Text20))))))
| (m = Iknows(pair(Nonce((absNB(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_NB0)), pair(Agent(dishonest(i1)), Nonce((absText2(pair(Agent(honest(a1)), Agent(dishonest(i2)))) Abs_Text20))))))
| (m = Iknows(pair(Nonce((absNB(pair(Agent(honest(a0)), Agent(honest(a1)))) Abs_NB0)), pair(Agent(dishonest(i0)), Nonce((absText2(pair(Agent(honest(a2)), Agent(dishonest(i1)))) Abs_Text20))))))
| (m = Iknows(pair(Nonce((absText2(pair(Agent(honest(a0)), Agent(dishonest(i0)))) Abs_Text20)), pair(Agent(dishonest(i1)), Nonce((absText2(pair(Agent(honest(a1)), Agent(dishonest(i2)))) Abs_Text21))))))
)}"
section {* Checking Fixed-point (ISO_twopass_symm) *}
lemma fp_attack_free: "~ (Attack m : ISO_twopass_symm_fp)"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma init_0: "Iknows(Nonce((ni Abs_NI))) : ISO_twopass_symm_fp"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma init_1: "Iknows(Agent(dishonest(i))) : ISO_twopass_symm_fp"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma init_2: "State(rA, [Agent(honest(a)), Step(0), SymKey(sk(pair(Agent(honest(a)), Agent(dishonest(i))))), Agent(dishonest(i)), SID(sid)] ) : ISO_twopass_symm_fp"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma init_3: "State(rA, [Agent(honest(a)), Step(0), SymKey(sk(pair(Agent(honest(a)), Agent(honest(a))))), Agent(honest(a)), SID(sid)] ) : ISO_twopass_symm_fp"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma init_4: "Iknows(Step(0)) : ISO_twopass_symm_fp"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma init_5: "Iknows(SymKey(sk(pair(Agent(dishonest(i)), Agent(dishonest(i)))))) : ISO_twopass_symm_fp"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma init_6: "Iknows(SID(sid)) : ISO_twopass_symm_fp"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma init_7: "Iknows(SymKey(sk(pair(Agent(dishonest(i)), Agent(honest(a)))))) : ISO_twopass_symm_fp"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma init_8: "Iknows(Agent(honest(a))) : ISO_twopass_symm_fp"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma init_9: "State(rB, [Agent(honest(a)), Step(0), SymKey(sk(pair(Agent(dishonest(i)), Agent(honest(a))))), Agent(dishonest(i)), SID(sid)] ) : ISO_twopass_symm_fp"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma init_10: "State(rB, [Agent(honest(a)), Step(0), SymKey(sk(pair(Agent(honest(a)), Agent(honest(a))))), Agent(honest(a)), SID(sid)] ) : ISO_twopass_symm_fp"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma init_11: "Iknows(SymKey(sk(pair(Agent(honest(a)), Agent(dishonest(i)))))) : ISO_twopass_symm_fp"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_0: "[|
Iknows(crypt(K, M)) : ISO_twopass_symm_fp;
Iknows(inv(K)) : ISO_twopass_symm_fp|]
==>
(Iknows(M) : ISO_twopass_symm_fp)"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_1: "[|
Iknows(crypt(inv(K), M)) : ISO_twopass_symm_fp;
Iknows(K) : ISO_twopass_symm_fp|]
==>
(Iknows(M) : ISO_twopass_symm_fp)"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_2: "[|
Iknows(scrypt(K, M)) : ISO_twopass_symm_fp;
Iknows(K) : ISO_twopass_symm_fp|]
==>
(Iknows(M) : ISO_twopass_symm_fp)"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_3: "[|
Iknows(pair(M1, M2)) : ISO_twopass_symm_fp|]
==>
(Iknows(M1) : ISO_twopass_symm_fp) &
(Iknows(M2) : ISO_twopass_symm_fp)"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_4: "[|
Secret(M, Agent(honest(a))) : ISO_twopass_symm_fp;
Iknows(M) : ISO_twopass_symm_fp|]
==>
(Attack(pair(secrecy, M)) : ISO_twopass_symm_fp)"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_5: "[|
Request(A, B, Purpose(purposeNB), M, SID(sid)) : ISO_twopass_symm_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)))) : ISO_twopass_symm_fp)"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_6: "[|
Request(A, B, Purpose(purposeText2), M, SID(sid)) : ISO_twopass_symm_fp;
~ ( ? i .
B = Agent(dishonest(i)));
~ ( ? B A Abs_Text2 .
M = Nonce((absText2(pair(B, A)) Abs_Text2)))|]
==>
(Attack(pair(authentication, pair(A, pair(B, M)))) : ISO_twopass_symm_fp)"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_7: "[|
State(rB, [Agent(B), Step(0), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(A), SID(sid)] ) : ISO_twopass_symm_fp|]
==>
(State(rB, [Agent(B), Step(1), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(A), Nonce((absNB(pair(Agent(B), Agent(A))) Abs_NB)), SID(sid)] ) : ISO_twopass_symm_fp) &
(Iknows(Nonce((absNB(pair(Agent(B), Agent(A))) Abs_NB))) : ISO_twopass_symm_fp)"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_8: "[|
State(rA, [Agent(A), Step(0), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(B), SID(sid)] ) : ISO_twopass_symm_fp;
Iknows(Nonce(NB)) : ISO_twopass_symm_fp|]
==>
(Witness(Agent(A), Agent(B), Purpose(purposeText2), Nonce((absText2(pair(Agent(A), Agent(B))) Abs_Text2))) : ISO_twopass_symm_fp) &
(State(rA, [Agent(A), Step(1), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(B), Nonce(NB), Nonce((absText2(pair(Agent(A), Agent(B))) Abs_Text2)), scrypt(SymKey(sk(pair(Agent(A), Agent(B)))), pair(Nonce(NB), pair(Agent(B), Nonce((absText2(pair(Agent(A), Agent(B))) Abs_Text2))))), SID(sid)] ) : ISO_twopass_symm_fp) &
(Iknows(scrypt(SymKey(sk(pair(Agent(A), Agent(B)))), pair(Nonce(NB), pair(Agent(B), Nonce((absText2(pair(Agent(A), Agent(B))) Abs_Text2)))))) : ISO_twopass_symm_fp)"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_9: "[|
State(rB, [Agent(B), Step(1), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(A), Nonce(NB), SID(sid)] ) : ISO_twopass_symm_fp;
Iknows(scrypt(SymKey(sk(pair(Agent(A), Agent(B)))), pair(Nonce(NB), pair(Agent(B), Nonce(Text2))))) : ISO_twopass_symm_fp|]
==>
(Request(Agent(B), Agent(A), Purpose(purposeText2), Nonce(Text2), SID(sid)) : ISO_twopass_symm_fp) &
(State(rB, [Agent(B), Step(2), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(A), Nonce(NB), Nonce(Text2), scrypt(SymKey(sk(pair(Agent(A), Agent(B)))), pair(Nonce(NB), pair(Agent(B), Nonce(Text2)))), SID(sid)] ) : ISO_twopass_symm_fp)"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
lemma rule_10: "[|
State(rB, [Agent(B), Step(1), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(A), Nonce(NB), SID(sid)] ) : ISO_twopass_symm_fp;
Iknows(SymKey(sk(pair(Agent(A), Agent(B))))) : ISO_twopass_symm_fp;
Iknows(Nonce(NB)) : ISO_twopass_symm_fp;
Iknows(Agent(B)) : ISO_twopass_symm_fp;
Iknows(Nonce(Text2)) : ISO_twopass_symm_fp|]
==>
(Request(Agent(B), Agent(A), Purpose(purposeText2), Nonce(Text2), SID(sid)) : ISO_twopass_symm_fp) &
(State(rB, [Agent(B), Step(2), SymKey(sk(pair(Agent(A), Agent(B)))), Agent(A), Nonce(NB), Nonce(Text2), scrypt(SymKey(sk(pair(Agent(A), Agent(B)))), pair(Nonce(NB), pair(Agent(B), Nonce(Text2)))), SID(sid)] ) : ISO_twopass_symm_fp)"
by(simp only: ISO_twopass_symm_fp_def, simp only: set2pred, simp, auto?)+
section {* Security Proof(s) (ISO_twopass_symm) *}
lemma over_approx: "t : ISO_twopass_symm ==> (set t) <= ISO_twopass_symm_fp"
apply(rule ISO_twopass_symm.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)+)
done
end (* theory *)