Theory Protocol
section "Protocol modeling and verification"
theory Protocol
imports Propaedeutics
begin
subsection "Protocol modeling"
text ‹
The protocol under consideration can be formalized by means of the following inductive definition.
\null
›
inductive_set protocol :: "(event list × state × msg set × msg set) set" where
Nil: "([], start_S, start_A, start_U) ∈ protocol" |
R1: "⟦(evsR1, S, A, U) ∈ protocol; Pri_AgrK s ∉ U; s ≠ 0;
NonceS (S (Card n, n, run)) = None⟧
⟹ (Says n run 1 (Card n) (User m) (Crypt (symK n) (Pri_AgrK s)) # evsR1,
S ((Card n, n, run) := S (Card n, n, run) ⦇NonceS := Some s⦈),
if n ∈ bad then insert (Pri_AgrK s) A else A,
insert (Pri_AgrK s) U) ∈ protocol" |
FR1: "⟦(evsFR1, S, A, U) ∈ protocol; User m ≠ Spy; s ≠ 0;
Crypt (symK m) (Pri_AgrK s) ∈ synth (analz (A ∪ spies evsFR1))⟧
⟹ (Says n run 1 Spy (User m) (Crypt (symK m) (Pri_AgrK s)) # evsFR1,
S, A, U) ∈ protocol" |
C2: "⟦(evsC2, S, A, U) ∈ protocol; Pri_AgrK a ∉ U;
NonceS (S (User m, n, run)) = None;
Says n run 1 X (User m) (Crypt (symK n') (Pri_AgrK s)) ∈ set evsC2;
s' = (if symK n' = symK m then s else 0)⟧
⟹ (Says n run 2 (User m) (Card n) (pubAK a) # evsC2,
S ((User m, n, run) := S (User m, n, run)
⦇NonceS := Some s', IntMapK := Some a⦈),
if User m = Spy then insert (Pri_AgrK a) A else A,
insert (Pri_AgrK a) U) ∈ protocol" |
FC2: "⟦(evsFC2, S, A, U) ∈ protocol;
Pri_AgrK a ∈ analz (A ∪ spies evsFC2)⟧
⟹ (Says n run 2 Spy (Card n) (pubAK a) # evsFC2,
S, A, U) ∈ protocol" |
R2: "⟦(evsR2, S, A, U) ∈ protocol; Pri_AgrK b ∉ U;
NonceS (S (Card n, n, run)) ≠ None;
IntMapK (S (Card n, n, run)) = None;
Says n run 2 X (Card n) (pubAK a) ∈ set evsR2⟧
⟹ (Says n run 2 (Card n) X (pubAK b) # evsR2,
S ((Card n, n, run) := S (Card n, n, run)
⦇IntMapK := Some b, ExtMapK := Some a⦈),
A, insert (Pri_AgrK b) U) ∈ protocol" |
FR2: "⟦(evsFR2, S, A, U) ∈ protocol; User m ≠ Spy;
Pri_AgrK b ∈ analz (A ∪ spies evsFR2)⟧
⟹ (Says n run 2 Spy (User m) (pubAK b) # evsFR2,
S, A, U) ∈ protocol" |
C3: "⟦(evsC3, S, A, U) ∈ protocol; Pri_AgrK c ∉ U;
NonceS (S (User m, n, run)) = Some s;
IntMapK (S (User m, n, run)) = Some a;
ExtMapK (S (User m, n, run)) = None;
Says n run 2 X (User m) (pubAK b) ∈ set evsC3;
c * (s + a * b) ≠ 0⟧
⟹ (Says n run 3 (User m) (Card n) (pubAK (c * (s + a * b))) # evsC3,
S ((User m, n, run) := S (User m, n, run)
⦇ExtMapK := Some b, IntAgrK := Some c⦈),
if User m = Spy then insert (Pri_AgrK c) A else A,
insert (Pri_AgrK c) U) ∈ protocol" |
FC3: "⟦(evsFC3, S, A, U) ∈ protocol;
NonceS (S (Card n, n, run)) = Some s;
IntMapK (S (Card n, n, run)) = Some b;
ExtMapK (S (Card n, n, run)) = Some a;
{Pri_AgrK s, Pri_AgrK a, Pri_AgrK c} ⊆ analz (A ∪ spies evsFC3)⟧
⟹ (Says n run 3 Spy (Card n) (pubAK (c * (s + a * b))) # evsFC3,
S, A, U) ∈ protocol" |
R3: "⟦(evsR3, S, A, U) ∈ protocol; Pri_AgrK d ∉ U;
NonceS (S (Card n, n, run)) = Some s;
IntMapK (S (Card n, n, run)) = Some b;
ExtMapK (S (Card n, n, run)) = Some a;
IntAgrK (S (Card n, n, run)) = None;
Says n run 3 X (Card n) (pubAK (c * (s' + a * b))) ∈ set evsR3;
Key (sesK (c * d * (s' + a * b))) ∉ U;
Key (sesK (c * d * (s + a * b))) ∉ U;
d * (s + a * b) ≠ 0⟧
⟹ (Says n run 3 (Card n) X (pubAK (d * (s + a * b))) # evsR3,
S ((Card n, n, run) := S (Card n, n, run)
⦇IntAgrK := Some d, ExtAgrK := Some (c * (s' + a * b))⦈),
if s' = s ∧ Pri_AgrK c ∈ analz (A ∪ spies evsR3)
then insert (Key (sesK (c * d * (s + a * b)))) A else A,
{Pri_AgrK d,
Key (sesK (c * d * (s' + a * b))), Key (sesK (c * d * (s + a * b))),
⦃Key (sesK (c * d * (s + a * b))), Agent X, Number n, Number run⦄} ∪ U) ∈ protocol" |
FR3: "⟦(evsFR3, S, A, U) ∈ protocol; User m ≠ Spy;
NonceS (S (User m, n, run)) = Some s;
IntMapK (S (User m, n, run)) = Some a;
ExtMapK (S (User m, n, run)) = Some b;
IntAgrK (S (User m, n, run)) = Some c;
{Pri_AgrK s, Pri_AgrK b, Pri_AgrK d} ⊆ analz (A ∪ spies evsFR3);
Key (sesK (c * d * (s + a * b))) ∉ U⟧
⟹ (Says n run 3 Spy (User m) (pubAK (d * (s + a * b))) # evsFR3, S,
insert (Key (sesK (c * d * (s + a * b)))) A,
{Key (sesK (c * d * (s + a * b))),
⦃Key (sesK (c * d * (s + a * b))), Agent (User m), Number n, Number run⦄} ∪ U) ∈ protocol" |
C4: "⟦(evsC4, S, A, U) ∈ protocol;
IntAgrK (S (User m, n, run)) = Some c;
ExtAgrK (S (User m, n, run)) = None;
Says n run 3 X (User m) (pubAK f) ∈ set evsC4;
⦃Key (sesK (c * f)), Agent (User m), Number n, Number run⦄ ∈ U⟧
⟹ (Says n run 4 (User m) (Card n) (Crypt (sesK (c * f)) (pubAK f)) # evsC4,
S ((User m, n, run) := S (User m, n, run) ⦇ExtAgrK := Some f⦈),
A, U) ∈ protocol" |
FC4: "⟦(evsFC4, S, A, U) ∈ protocol;
NonceS (S (Card n, n, run)) = Some s;
IntMapK (S (Card n, n, run)) = Some b;
ExtMapK (S (Card n, n, run)) = Some a;
IntAgrK (S (Card n, n, run)) = Some d;
ExtAgrK (S (Card n, n, run)) = Some e;
Crypt (sesK (d * e)) (pubAK (d * (s + a * b)))
∈ synth (analz (A ∪ spies evsFC4))⟧
⟹ (Says n run 4 Spy (Card n)
(Crypt (sesK (d * e)) (pubAK (d * (s + a * b)))) # evsFC4,
S, A, U) ∈ protocol" |
R4: "⟦(evsR4, S, A, U) ∈ protocol;
NonceS (S (Card n, n, run)) = Some s;
IntMapK (S (Card n, n, run)) = Some b;
ExtMapK (S (Card n, n, run)) = Some a;
IntAgrK (S (Card n, n, run)) = Some d;
ExtAgrK (S (Card n, n, run)) = Some e;
Says n run 4 X (Card n) (Crypt (sesK (d * e))
(pubAK (d * (s + a * b)))) ∈ set evsR4⟧
⟹ (Says n run 4 (Card n) X (Crypt (sesK (d * e))
⦃pubAK e, Auth_Data (priAK n) b, pubAK (priAK n),
Crypt (priSK CA) (Hash (pubAK (priAK n)))⦄) # evsR4,
S, A, U) ∈ protocol" |
FR4: "⟦(evsFR4, S, A, U) ∈ protocol; User m ≠ Spy;
NonceS (S (User m, n, run)) = Some s;
IntMapK (S (User m, n, run)) = Some a;
ExtMapK (S (User m, n, run)) = Some b;
IntAgrK (S (User m, n, run)) = Some c;
ExtAgrK (S (User m, n, run)) = Some f;
Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄ ∈ synth (analz (A ∪ spies evsFR4))⟧
⟹ (Says n run 4 Spy (User m) (Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄) # evsFR4,
S, A, U) ∈ protocol" |
C5: "⟦(evsC5, S, A, U) ∈ protocol;
NonceS (S (User m, n, run)) = Some s;
IntMapK (S (User m, n, run)) = Some a;
ExtMapK (S (User m, n, run)) = Some b;
IntAgrK (S (User m, n, run)) = Some c;
ExtAgrK (S (User m, n, run)) = Some f;
Says n run 4 X (User m) (Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄) ∈ set evsC5⟧
⟹ (Says n run 5 (User m) (Card n) (Crypt (sesK (c * f)) (Passwd m)) # evsC5,
S, A, U) ∈ protocol" |
FC5: "⟦(evsFC5, S, A, U) ∈ protocol;
IntAgrK (S (Card n, n, run)) = Some d;
ExtAgrK (S (Card n, n, run)) = Some e;
Crypt (sesK (d * e)) (Passwd n) ∈ synth (analz (A ∪ spies evsFC5))⟧
⟹ (Says n run 5 Spy (Card n) (Crypt (sesK (d * e)) (Passwd n)) # evsFC5,
S, A, U) ∈ protocol" |
R5: "⟦(evsR5, S, A, U) ∈ protocol;
IntAgrK (S (Card n, n, run)) = Some d;
ExtAgrK (S (Card n, n, run)) = Some e;
Says n run 5 X (Card n) (Crypt (sesK (d * e)) (Passwd n)) ∈ set evsR5⟧
⟹ (Says n run 5 (Card n) X (Crypt (sesK (d * e)) (Number 0)) # evsR5,
S, A, U) ∈ protocol" |
FR5: "⟦(evsFR5, S, A, U) ∈ protocol; User m ≠ Spy;
IntAgrK (S (User m, n, run)) = Some c;
ExtAgrK (S (User m, n, run)) = Some f;
Crypt (sesK (c * f)) (Number 0) ∈ synth (analz (A ∪ spies evsFR5))⟧
⟹ (Says n run 5 Spy (User m) (Crypt (sesK (c * f)) (Number 0)) # evsFR5,
S, A, U) ∈ protocol"
text ‹
\null
Here below are some comments about the most significant points of this definition.
\begin{itemize}
\item
Rules @{thm [source] R1} and @{thm [source] FR1} constrain the values of nonce $s$ to be different
from 0. In this way, the state of affairs where an incorrect PACE authentication key has been used
to encrypt nonce $s$, so that a wrong value results from the decryption, can be modeled in rule
@{thm [source] C2} by identifying such value with 0.
\item
The spy can disclose session keys as soon as they are established, namely in correspondence with
rules @{thm [source] R3} and @{thm [source] FR3}.
\\In the former rule, condition @{term "s' = s"} identifies Diffie-Hellman private key ‹c› as
the terminal's ephemeral private key for key agreement, and then $[c \times d \times (s + a \times
b)]G$ as the terminal's value of the shared secret, which the spy can compute by multiplying the
card's ephemeral public key $[d \times (s + a \times b)]G$ by ‹c› provided she knows
‹c›.
\\In the latter rule, the spy is required to know private keys ‹s›, ‹b›, and ‹d›
to be able to compute and send public key $[d \times (s + a \times b)]G$. This is the only way to
share with @{term "User m"} the same shared secret's value $[c \times d \times (s + a \times b)]G$,
which the spy can compute by multiplying the user's ephemeral public key $[c \times (s + a \times
b)]G$ by ‹d›.
\item
Rules @{thm [source] R3} and @{thm [source] FR3} record the user, the communication channel, and the
protocol run associated to the session key having been established by adding this information to the
set of the messages already used. In this way, rule @{thm [source] C4} can specify that the session
key computed by @{term "User m"} is fresh by assuming that a corresponding record be included in set
‹U›. In fact, a simple check that the session key be not included in ‹U› would vacuously
fail, as session keys are added to the set of the messages already used in rules @{thm [source] R3}
and @{thm [source] FR3}.
\end{itemize}
›
subsection "Secrecy theorems"
text ‹
This section contains a series of lemmas culminating in the secrecy theorems ‹pr_key_secrecy›
and ‹pr_passwd_secrecy›. Structured Isar proofs are used, possibly preceded by
\emph{apply}-style scripts in case a substantial amount of backward reasoning steps is required at
the beginning.
\null
›
lemma pr_state:
"(evs, S, A, U) ∈ protocol ⟹
(NonceS (S (X, n, run)) = None ⟶ IntMapK (S (X, n, run)) = None) ∧
(IntMapK (S (X, n, run)) = None ⟶ ExtMapK (S (X, n, run)) = None) ∧
(ExtMapK (S (X, n, run)) = None ⟶ IntAgrK (S (X, n, run)) = None) ∧
(IntAgrK (S (X, n, run)) = None ⟶ ExtAgrK (S (X, n, run)) = None)"
proof (erule protocol.induct, simp_all)
qed (rule_tac [!] impI, simp_all)
lemma pr_state_1:
"⟦(evs, S, A, U) ∈ protocol; NonceS (S (X, n, run)) = None⟧ ⟹
IntMapK (S (X, n, run)) = None"
by (simp add: pr_state)
lemma pr_state_2:
"⟦(evs, S, A, U) ∈ protocol; IntMapK (S (X, n, run)) = None⟧ ⟹
ExtMapK (S (X, n, run)) = None"
by (simp add: pr_state)
lemma pr_state_3:
"⟦(evs, S, A, U) ∈ protocol; ExtMapK (S (X, n, run)) = None⟧ ⟹
IntAgrK (S (X, n, run)) = None"
by (simp add: pr_state)
lemma pr_state_4:
"⟦(evs, S, A, U) ∈ protocol; IntAgrK (S (X, n, run)) = None⟧ ⟹
ExtAgrK (S (X, n, run)) = None"
by (simp add: pr_state)
lemma pr_analz_used:
"(evs, S, A, U) ∈ protocol ⟹ A ⊆ U"
by (erule protocol.induct, auto)
lemma pr_key_parts_intro [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Key K ∈ parts (A ∪ spies evs) ⟶
Key K ∈ A"
proof (erule protocol.induct, subst parts_simp, simp, blast, simp)
qed (simp_all add: parts_simp_insert parts_auth_data parts_crypt parts_mpair)
lemma pr_key_analz:
"(evs, S, A, U) ∈ protocol ⟹ (Key K ∈ analz (A ∪ spies evs)) = (Key K ∈ A)"
proof (rule iffI, drule subsetD [OF analz_parts_subset], erule pr_key_parts_intro,
assumption)
qed (rule subsetD [OF analz_subset], simp)
lemma pr_symk_used:
"(evs, S, A, U) ∈ protocol ⟹ Key (symK n) ∈ U"
by (erule protocol.induct, simp_all)
lemma pr_symk_analz:
"(evs, S, A, U) ∈ protocol ⟹ (Key (symK n) ∈ analz (A ∪ spies evs)) = (n ∈ bad)"
proof (simp add: pr_key_analz, erule protocol.induct, simp_all, rule_tac [2] impI,
rule_tac [!] iffI, simp_all, erule disjE, erule_tac [2-4] disjE, simp_all)
assume "Key (symK n) ∈ Key ` symK ` bad"
hence "∃m ∈ bad. symK n = symK m"
by (simp add: image_iff)
then obtain m where "m ∈ bad" and "symK n = symK m" ..
thus "n ∈ bad"
by (rule symK_bad)
next
assume "Key (symK n) ∈ Key ` range pubSK"
thus "n ∈ bad"
by (auto, drule_tac sym, erule_tac notE [OF pubSK_symK])
next
assume "Key (symK n) ∈ pubAK ` range priAK"
thus "n ∈ bad"
by blast
next
fix evsR3 S A U s a b c d
assume "(evsR3, S, A, U) ∈ protocol"
hence "Key (symK n) ∈ U"
by (rule pr_symk_used)
moreover assume "symK n = sesK (c * d * (s + a * b))"
ultimately have "Key (sesK (c * d * (s + a * b))) ∈ U"
by simp
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show "n ∈ bad"
by contradiction
next
fix evsFR3 S A U s a b c d
assume "(evsFR3, S, A, U) ∈ protocol"
hence "Key (symK n) ∈ U"
by (rule pr_symk_used)
moreover assume "symK n = sesK (c * d * (s + a * b))"
ultimately have "Key (sesK (c * d * (s + a * b))) ∈ U"
by simp
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show "n ∈ bad"
by contradiction
qed
lemma pr_sesk_card [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
IntAgrK (S (Card n, n, run)) = Some d ⟶
ExtAgrK (S (Card n, n, run)) = Some e ⟶
Key (sesK (d * e)) ∈ U"
proof (erule protocol.induct, simp_all, (rule impI)+, simp)
qed (subst (2) mult.commute, subst mult.assoc, simp)
lemma pr_sesk_user_1 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
IntAgrK (S (User m, n, run)) = Some c ⟶
ExtAgrK (S (User m, n, run)) = Some f ⟶
⦃Key (sesK (c * f)), Agent (User m), Number n, Number run⦄ ∈ U"
proof (erule protocol.induct, simp_all, (rule_tac [!] impI)+, simp_all)
fix evsC3 S A U m n run
assume A: "(evsC3, S, A, U) ∈ protocol" and
"ExtMapK (S (User m, n, run)) = None"
hence "IntAgrK (S (User m, n, run)) = None"
by (rule pr_state_3)
with A have "ExtAgrK (S (User m, n, run)) = None"
by (rule pr_state_4)
moreover assume "ExtAgrK (S (User m, n, run)) = Some f"
ultimately show "⦃Key (sesK (c * f)), Agent (User m), Number n, Number run⦄ ∈ U"
by simp
qed
lemma pr_sesk_user_2 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
⦃Key (sesK K), Agent (User m), Number n, Number run⦄ ∈ U ⟶
Key (sesK K) ∈ U"
by (erule protocol.induct, blast, simp_all)
lemma pr_auth_key_used:
"(evs, S, A, U) ∈ protocol ⟹ Pri_AgrK (priAK n) ∈ U"
by (erule protocol.induct, simp_all)
lemma pr_int_mapk_used [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
IntMapK (S (Card n, n, run)) = Some b ⟶
Pri_AgrK b ∈ U"
by (erule protocol.induct, simp_all)
lemma pr_valid_key_analz:
"(evs, S, A, U) ∈ protocol ⟹ Key (pubSK X) ∈ analz (A ∪ spies evs)"
by (simp add: pr_key_analz, erule protocol.induct, simp_all)
lemma pr_pri_agrk_parts [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Pri_AgrK x ∉ U ⟶
Pri_AgrK x ∉ parts (A ∪ spies evs)"
proof (induction arbitrary: x rule: protocol.induct,
simp_all add: parts_simp_insert parts_auth_data parts_crypt parts_mpair,
subst parts_simp, blast, blast, rule_tac [!] impI)
fix evsFR1 A U m s x
assume
"⋀x. Pri_AgrK x ∉ U ⟶ Pri_AgrK x ∉ parts (A ∪ spies evsFR1)" and
"Pri_AgrK x ∉ U"
hence A: "Pri_AgrK x ∉ parts (A ∪ spies evsFR1)" ..
assume B: "Crypt (symK m) (Pri_AgrK s) ∈ synth (analz (A ∪ spies evsFR1))"
show "x ≠ s"
proof
assume "x = s"
hence "Crypt (symK m) (Pri_AgrK x) ∈ synth (analz (A ∪ spies evsFR1))"
using B by simp
hence "Crypt (symK m) (Pri_AgrK x) ∈ analz (A ∪ spies evsFR1) ∨
Pri_AgrK x ∈ synth (analz (A ∪ spies evsFR1)) ∧
Key (symK m) ∈ analz (A ∪ spies evsFR1)"
(is "?P ∨ ?Q")
by (rule synth_crypt)
moreover {
assume ?P
hence "Crypt (symK m) (Pri_AgrK x) ∈ parts (A ∪ spies evsFR1)"
by (rule subsetD [OF analz_parts_subset])
hence "Pri_AgrK x ∈ parts (A ∪ spies evsFR1)"
by (rule parts.Body)
hence False
using A by contradiction
}
moreover {
assume ?Q
hence "Pri_AgrK x ∈ synth (analz (A ∪ spies evsFR1))" ..
hence "Pri_AgrK x ∈ analz (A ∪ spies evsFR1)"
by (rule synth_simp_intro, simp)
hence "Pri_AgrK x ∈ parts (A ∪ spies evsFR1)"
by (rule subsetD [OF analz_parts_subset])
hence False
using A by contradiction
}
ultimately show False ..
qed
next
fix evsR4 S A U b n run x
assume
A: "(evsR4, S, A, U) ∈ protocol" and
B: "IntMapK (S (Card n, n, run)) = Some b" and
C: "Pri_AgrK x ∉ U"
show "x ≠ priAK n ∧ x ≠ b"
proof (rule conjI, rule_tac [!] notI)
assume "x = priAK n"
moreover have "Pri_AgrK (priAK n) ∈ U"
using A by (rule pr_auth_key_used)
ultimately have "Pri_AgrK x ∈ U"
by simp
thus False
using C by contradiction
next
assume "x = b"
moreover have "Pri_AgrK b ∈ U"
using A and B by (rule pr_int_mapk_used)
ultimately have "Pri_AgrK x ∈ U"
by simp
thus False
using C by contradiction
qed
next
fix evsFR4 S A U s a b c f g x
assume
A: "⋀x. Pri_AgrK x ∉ U ⟶ Pri_AgrK x ∉ parts (A ∪ spies evsFR4)" and
B: "(evsFR4, S, A, U) ∈ protocol" and
C: "Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄ ∈ synth (analz (A ∪ spies evsFR4))"
(is "Crypt _ ?M ∈ synth (analz ?A)") and
D: "Pri_AgrK x ∉ U"
show "x ≠ g ∧ x ≠ b"
proof -
have E: "Pri_AgrK b ∈ U ∧ Pri_AgrK g ∈ U"
proof -
have "Crypt (sesK (c * f)) ?M ∈ analz ?A ∨
?M ∈ synth (analz ?A) ∧ Key (sesK (c * f)) ∈ analz ?A"
using C by (rule synth_crypt)
moreover {
assume "Crypt (sesK (c * f)) ?M ∈ analz ?A"
hence "Crypt (sesK (c * f)) ?M ∈ parts ?A"
by (rule subsetD [OF analz_parts_subset])
hence "?M ∈ parts ?A"
by (rule parts.Body)
hence "⦃Auth_Data g b, pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ parts ?A"
by (rule parts.Snd)
hence F: "Auth_Data g b ∈ parts ?A"
by (rule parts.Fst)
hence "Pri_AgrK b ∈ parts ?A"
by (rule parts.Auth_Snd)
moreover have "Pri_AgrK g ∈ parts ?A"
using F by (rule parts.Auth_Fst)
ultimately have "Pri_AgrK b ∈ parts ?A ∧ Pri_AgrK g ∈ parts ?A" ..
}
moreover {
assume "?M ∈ synth (analz ?A) ∧
Key (sesK (c * f)) ∈ analz ?A"
hence "?M ∈ synth (analz ?A)" ..
hence "⦃Auth_Data g b, pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ synth (analz ?A)"
by (rule synth_analz_snd)
hence "Auth_Data g b ∈ synth (analz ?A)"
by (rule synth_analz_fst)
hence "Auth_Data g b ∈ analz ?A ∨
Pri_AgrK g ∈ analz ?A ∧ Pri_AgrK b ∈ analz ?A"
by (rule synth_auth_data)
moreover {
assume "Auth_Data g b ∈ analz ?A"
hence F: "Auth_Data g b ∈ parts ?A"
by (rule subsetD [OF analz_parts_subset])
hence "Pri_AgrK b ∈ parts ?A"
by (rule parts.Auth_Snd)
moreover have "Pri_AgrK g ∈ parts ?A"
using F by (rule parts.Auth_Fst)
ultimately have "Pri_AgrK b ∈ parts ?A ∧ Pri_AgrK g ∈ parts ?A" ..
}
moreover {
assume F: "Pri_AgrK g ∈ analz ?A ∧ Pri_AgrK b ∈ analz ?A"
hence "Pri_AgrK b ∈ analz ?A" ..
hence "Pri_AgrK b ∈ parts ?A"
by (rule subsetD [OF analz_parts_subset])
moreover have "Pri_AgrK g ∈ analz ?A"
using F ..
hence "Pri_AgrK g ∈ parts ?A"
by (rule subsetD [OF analz_parts_subset])
ultimately have "Pri_AgrK b ∈ parts ?A ∧ Pri_AgrK g ∈ parts ?A" ..
}
ultimately have "Pri_AgrK b ∈ parts ?A ∧ Pri_AgrK g ∈ parts ?A" ..
}
ultimately have F: "Pri_AgrK b ∈ parts ?A ∧ Pri_AgrK g ∈ parts ?A" ..
hence "Pri_AgrK b ∈ parts ?A" ..
hence "Pri_AgrK b ∈ U"
by (rule contrapos_pp, insert A, simp)
moreover have "Pri_AgrK g ∈ parts ?A"
using F ..
hence "Pri_AgrK g ∈ U"
by (rule contrapos_pp, insert A, simp)
ultimately show ?thesis ..
qed
show ?thesis
proof (rule conjI, rule_tac [!] notI)
assume "x = g"
hence "Pri_AgrK x ∈ U"
using E by simp
thus False
using D by contradiction
next
assume "x = b"
hence "Pri_AgrK x ∈ U"
using E by simp
thus False
using D by contradiction
qed
qed
qed
lemma pr_pri_agrk_items:
"(evs, S, A, U) ∈ protocol ⟹
Pri_AgrK x ∉ U ⟹
items (insert (Pri_AgrK x) (A ∪ spies evs)) =
insert (Pri_AgrK x) (items (A ∪ spies evs))"
by (rule items_pri_agrk_out, rule pr_pri_agrk_parts)
lemma pr_auth_data_items:
"(evs, S, A, U) ∈ protocol ⟹
Pri_AgrK (priAK n) ∉ items (A ∪ spies evs) ∧
(IntMapK (S (Card n, n, run)) = Some b ⟶
Pri_AgrK b ∉ items (A ∪ spies evs))"
proof (induction arbitrary: n run b rule: protocol.induct,
simp_all add: items_simp_insert_2 items_crypt items_mpair pr_pri_agrk_items,
subst items_simp, blast+)
fix evsR1 S A U n' run' s n run b
assume
A: "(evsR1, S, A, U) ∈ protocol" and
B: "Pri_AgrK s ∉ U"
show
"(n = n' ∧ run = run' ⟶
priAK n' ≠ s ∧ (IntMapK (S (Card n', n', run')) = Some b ⟶ b ≠ s)) ∧
((n = n' ⟶ run ≠ run') ⟶
priAK n ≠ s ∧ (IntMapK (S (Card n, n, run)) = Some b ⟶ b ≠ s))"
proof (rule conjI, rule_tac [!] impI, rule_tac [!] conjI, rule_tac [2] impI,
rule_tac [4] impI, rule_tac [!] notI)
have "Pri_AgrK (priAK n) ∈ U"
using A by (rule pr_auth_key_used)
moreover assume "priAK n = s"
ultimately have "Pri_AgrK s ∈ U"
by simp
thus False
using B by contradiction
next
assume "IntMapK (S (Card n, n, run)) = Some b"
with A have "Pri_AgrK b ∈ U"
by (rule pr_int_mapk_used)
moreover assume "b = s"
ultimately have "Pri_AgrK s ∈ U"
by simp
thus False
using B by contradiction
next
have "Pri_AgrK (priAK n') ∈ U"
using A by (rule pr_auth_key_used)
moreover assume "priAK n' = s"
ultimately have "Pri_AgrK s ∈ U"
by simp
thus False
using B by contradiction
next
assume "IntMapK (S (Card n', n', run')) = Some b"
with A have "Pri_AgrK b ∈ U"
by (rule pr_int_mapk_used)
moreover assume "b = s"
ultimately have "Pri_AgrK s ∈ U"
by simp
thus False
using B by contradiction
qed
next
fix evsFR1 A m s n run b and S :: state
assume A: "⋀n run b. Pri_AgrK (priAK n) ∉ items (A ∪ spies evsFR1) ∧
(IntMapK (S (Card n, n, run)) = Some b ⟶
Pri_AgrK b ∉ items (A ∪ spies evsFR1))"
assume "Crypt (symK m) (Pri_AgrK s) ∈ synth (analz (A ∪ spies evsFR1))"
hence "Crypt (symK m) (Pri_AgrK s) ∈ analz (A ∪ spies evsFR1) ∨
Pri_AgrK s ∈ synth (analz (A ∪ spies evsFR1)) ∧
Key (symK m) ∈ analz (A ∪ spies evsFR1)"
(is "?P ∨ ?Q")
by (rule synth_crypt)
moreover {
assume ?P
hence "Crypt (symK m) (Pri_AgrK s) ∈ items (A ∪ spies evsFR1)"
by (rule subsetD [OF analz_items_subset])
hence "Pri_AgrK s ∈ items (A ∪ spies evsFR1)"
by (rule items.Body)
}
moreover {
assume ?Q
hence "Pri_AgrK s ∈ synth (analz (A ∪ spies evsFR1))" ..
hence "Pri_AgrK s ∈ analz (A ∪ spies evsFR1)"
by (rule synth_simp_intro, simp)
hence "Pri_AgrK s ∈ items (A ∪ spies evsFR1)"
by (rule subsetD [OF analz_items_subset])
}
ultimately have B: "Pri_AgrK s ∈ items (A ∪ spies evsFR1)" ..
show "Pri_AgrK (priAK n) ∉ items (insert (Pri_AgrK s) (A ∪ spies evsFR1)) ∧
(IntMapK (S (Card n, n, run)) = Some b ⟶
Pri_AgrK b ∉ items (insert (Pri_AgrK s) (A ∪ spies evsFR1)))"
by (simp add: items_simp_insert_1 [OF B] A)
next
fix evsC2 S A U a n run b and m :: nat
assume
A: "(evsC2, S, A, U) ∈ protocol" and
B: "Pri_AgrK a ∉ U"
show "m = 0 ⟶ priAK n ≠ a ∧ (IntMapK (S (Card n, n, run)) = Some b ⟶ b ≠ a)"
proof (rule impI, rule conjI, rule_tac [2] impI, rule_tac [!] notI)
have "Pri_AgrK (priAK n) ∈ U"
using A by (rule pr_auth_key_used)
moreover assume "priAK n = a"
ultimately have "Pri_AgrK a ∈ U"
by simp
thus False
using B by contradiction
next
assume "IntMapK (S (Card n, n, run)) = Some b"
with A have "Pri_AgrK b ∈ U"
by (rule pr_int_mapk_used)
moreover assume "b = a"
ultimately have "Pri_AgrK a ∈ U"
by simp
thus False
using B by contradiction
qed
next
fix evsR2 S A U b' n' run' b and n :: nat and run :: nat
assume
A: "(evsR2, S, A, U) ∈ protocol" and
B: "Pri_AgrK b' ∉ U"
show "n = n' ∧ run = run' ⟶ b' = b ⟶ Pri_AgrK b ∉ items (A ∪ spies evsR2)"
proof ((rule impI)+, drule sym, simp)
qed (rule contra_subsetD [OF items_parts_subset], rule pr_pri_agrk_parts [OF A B])
next
fix evsC3 S A U c n run b and m :: nat
assume
A: "(evsC3, S, A, U) ∈ protocol" and
B: "Pri_AgrK c ∉ U"
show "m = 0 ⟶ priAK n ≠ c ∧ (IntMapK (S (Card n, n, run)) = Some b ⟶ b ≠ c)"
proof (rule impI, rule conjI, rule_tac [2] impI, rule_tac [!] notI)
have "Pri_AgrK (priAK n) ∈ U"
using A by (rule pr_auth_key_used)
moreover assume "priAK n = c"
ultimately have "Pri_AgrK c ∈ U"
by simp
thus False
using B by contradiction
next
assume "IntMapK (S (Card n, n, run)) = Some b"
with A have "Pri_AgrK b ∈ U"
by (rule pr_int_mapk_used)
moreover assume "b = c"
ultimately have "Pri_AgrK c ∈ U"
by simp
thus False
using B by contradiction
qed
next
fix evsR3 A n' run' s b' c n run b and S :: state and s' :: pri_agrk
assume
A: "⋀n run b. Pri_AgrK (priAK n) ∉ items (A ∪ spies evsR3) ∧
(IntMapK (S (Card n, n, run)) = Some b ⟶
Pri_AgrK b ∉ items (A ∪ spies evsR3))" and
B: "IntMapK (S (Card n', n', run')) = Some b'"
show
"(s' = s ∧ Pri_AgrK c ∈ analz (A ∪ spies evsR3) ⟶
n = n' ∧ run = run' ⟶ b' = b ⟶
Pri_AgrK b ∉ items (A ∪ spies evsR3)) ∧
((s' = s ⟶ Pri_AgrK c ∉ analz (A ∪ spies evsR3)) ⟶
n = n' ∧ run = run' ⟶ b' = b ⟶
Pri_AgrK b ∉ items (A ∪ spies evsR3))"
proof (rule conjI, (rule_tac [!] impI)+)
have "Pri_AgrK (priAK n') ∉ items (A ∪ spies evsR3) ∧
(IntMapK (S (Card n', n', run')) = Some b' ⟶
Pri_AgrK b' ∉ items (A ∪ spies evsR3))"
using A .
hence "Pri_AgrK b' ∉ items (A ∪ spies evsR3)"
using B by simp
moreover assume "b' = b"
ultimately show "Pri_AgrK b ∉ items (A ∪ spies evsR3)"
by simp
next
have "Pri_AgrK (priAK n') ∉ items (A ∪ spies evsR3) ∧
(IntMapK (S (Card n', n', run')) = Some b' ⟶
Pri_AgrK b' ∉ items (A ∪ spies evsR3))"
using A .
hence "Pri_AgrK b' ∉ items (A ∪ spies evsR3)"
using B by simp
moreover assume "b' = b"
ultimately show "Pri_AgrK b ∉ items (A ∪ spies evsR3)"
by simp
qed
next
fix evsR4 A n' run' b' n run b and S :: state
let ?M = "⦃pubAK (priAK n'), Crypt (priSK CA) (Hash (pubAK (priAK n')))⦄"
assume
A: "⋀n run b. Pri_AgrK (priAK n) ∉ items (A ∪ spies evsR4) ∧
(IntMapK (S (Card n, n, run)) = Some b ⟶
Pri_AgrK b ∉ items (A ∪ spies evsR4))" and
B: "IntMapK (S (Card n', n', run')) = Some b'"
show
"Pri_AgrK (priAK n) ∉ items (insert (Auth_Data (priAK n') b')
(insert ?M (A ∪ spies evsR4))) ∧
(IntMapK (S (Card n, n, run)) = Some b ⟶
Pri_AgrK b ∉ items (insert (Auth_Data (priAK n') b')
(insert ?M (A ∪ spies evsR4))))"
proof (subst (1 2) insert_commute, simp add: items_mpair,
subst (1 3) insert_commute, simp add: items_simp_insert_2,
subst (1 2) insert_commute, simp add: items_crypt items_simp_insert_2)
have C: "Pri_AgrK (priAK n') ∉ items (A ∪ spies evsR4) ∧
(IntMapK (S (Card n', n', run')) = Some b' ⟶
Pri_AgrK b' ∉ items (A ∪ spies evsR4))"
using A .
hence "Pri_AgrK (priAK n') ∉ items (A ∪ spies evsR4)" ..
moreover have "Pri_AgrK b' ∉ items (A ∪ spies evsR4)"
using B and C by simp
ultimately show
"Pri_AgrK (priAK n) ∉ items (insert (Auth_Data (priAK n') b')
(A ∪ spies evsR4)) ∧
(IntMapK (S (Card n, n, run)) = Some b ⟶
Pri_AgrK b ∉ items (insert (Auth_Data (priAK n') b')
(A ∪ spies evsR4)))"
by (simp add: items_auth_data_out A)
qed
next
fix evsFR4 A s a b' c f g n run b and S :: state
let ?M = "⦃pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄"
assume
A: "⋀n run b. Pri_AgrK (priAK n) ∉ items (A ∪ spies evsFR4) ∧
(IntMapK (S (Card n, n, run)) = Some b ⟶
Pri_AgrK b ∉ items (A ∪ spies evsFR4))" and
B: "Crypt (sesK (c * f)) ⦃pubAK (c * (s + a * b')), Auth_Data g b', ?M⦄
∈ synth (analz (A ∪ spies evsFR4))"
(is "Crypt _ ?M' ∈ synth (analz ?A)")
have C: "Pri_AgrK b' ∈ items ?A ∨ Pri_AgrK g ∈ items ?A ⟶
Pri_AgrK b' ∈ items ?A ∧ Pri_AgrK g ∈ items ?A"
(is "?P ⟶ ?Q")
proof
assume ?P
have "Crypt (sesK (c * f)) ?M' ∈ analz ?A ∨
?M' ∈ synth (analz ?A) ∧ Key (sesK (c * f)) ∈ analz ?A"
using B by (rule synth_crypt)
moreover {
assume "Crypt (sesK (c * f)) ?M' ∈ analz ?A"
hence "Crypt (sesK (c * f)) ?M' ∈ items ?A"
by (rule subsetD [OF analz_items_subset])
hence "?M' ∈ items ?A"
by (rule items.Body)
hence "⦃Auth_Data g b', pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ items ?A"
by (rule items.Snd)
hence D: "Auth_Data g b' ∈ items ?A"
by (rule items.Fst)
have ?Q
proof (rule disjE [OF ‹?P›])
assume "Pri_AgrK b' ∈ items ?A"
moreover from this have "Pri_AgrK g ∈ items ?A"
by (rule items.Auth_Fst [OF D])
ultimately show ?Q ..
next
assume "Pri_AgrK g ∈ items ?A"
moreover from this have "Pri_AgrK b' ∈ items ?A"
by (rule items.Auth_Snd [OF D])
ultimately show ?Q
by simp
qed
}
moreover {
assume "?M' ∈ synth (analz ?A) ∧ Key (sesK (c * f)) ∈ analz ?A"
hence "?M' ∈ synth (analz ?A)" ..
hence "⦃Auth_Data g b', pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ synth (analz ?A)"
by (rule synth_analz_snd)
hence "Auth_Data g b' ∈ synth (analz ?A)"
by (rule synth_analz_fst)
hence "Auth_Data g b' ∈ analz ?A ∨
Pri_AgrK g ∈ analz ?A ∧ Pri_AgrK b' ∈ analz ?A"
by (rule synth_auth_data)
moreover {
assume "Auth_Data g b' ∈ analz ?A"
hence D: "Auth_Data g b' ∈ items ?A"
by (rule subsetD [OF analz_items_subset])
have ?Q
proof (rule disjE [OF ‹?P›])
assume "Pri_AgrK b' ∈ items ?A"
moreover from this have "Pri_AgrK g ∈ items ?A"
by (rule items.Auth_Fst [OF D])
ultimately show ?Q ..
next
assume "Pri_AgrK g ∈ items ?A"
moreover from this have "Pri_AgrK b' ∈ items ?A"
by (rule items.Auth_Snd [OF D])
ultimately show ?Q
by simp
qed
}
moreover {
assume D: "Pri_AgrK g ∈ analz ?A ∧ Pri_AgrK b' ∈ analz ?A"
hence "Pri_AgrK b' ∈ analz ?A" ..
hence "Pri_AgrK b' ∈ items ?A"
by (rule subsetD [OF analz_items_subset])
moreover have "Pri_AgrK g ∈ analz ?A"
using D ..
hence "Pri_AgrK g ∈ items ?A"
by (rule subsetD [OF analz_items_subset])
ultimately have ?Q ..
}
ultimately have ?Q ..
}
ultimately show ?Q ..
qed
show
"Pri_AgrK (priAK n) ∉ items (insert (Auth_Data g b')
(insert ?M (A ∪ spies evsFR4))) ∧
(IntMapK (S (Card n, n, run)) = Some b ⟶
Pri_AgrK b ∉ items (insert (Auth_Data g b')
(insert ?M (A ∪ spies evsFR4))))"
proof (subst (1 2) insert_commute, simp add: items_mpair,
subst (1 3) insert_commute, simp add: items_simp_insert_2,
subst (1 2) insert_commute, simp add: items_crypt items_simp_insert_2, cases ?P)
case True
with C have ?Q ..
thus
"Pri_AgrK (priAK n) ∉ items (insert (Auth_Data g b')
(A ∪ spies evsFR4)) ∧
(IntMapK (S (Card n, n, run)) = Some b ⟶
Pri_AgrK b ∉ items (insert (Auth_Data g b')
(A ∪ spies evsFR4)))"
by (simp add: items_auth_data_in items_simp_insert_1 A)
next
case False
thus
"Pri_AgrK (priAK n) ∉ items (insert (Auth_Data g b')
(A ∪ spies evsFR4)) ∧
(IntMapK (S (Card n, n, run)) = Some b ⟶
Pri_AgrK b ∉ items (insert (Auth_Data g b')
(A ∪ spies evsFR4)))"
by (simp add: items_auth_data_out A)
qed
qed
lemma pr_auth_key_analz:
"(evs, S, A, U) ∈ protocol ⟹ Pri_AgrK (priAK n) ∉ analz (A ∪ spies evs)"
proof (rule contra_subsetD [OF analz_items_subset], drule pr_auth_data_items)
qed (erule conjE)
lemma pr_int_mapk_analz:
"(evs, S, A, U) ∈ protocol ⟹
IntMapK (S (Card n, n, run)) = Some b ⟹
Pri_AgrK b ∉ analz (A ∪ spies evs)"
proof (rule contra_subsetD [OF analz_items_subset], drule pr_auth_data_items)
qed (erule conjE, rule mp)
lemma pr_key_set_unused [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evs) = H ∪ analz (A ∪ spies evs)"
proof (induction arbitrary: H rule: protocol.induct, simp_all add: analz_simp_insert_2,
rule impI, (subst analz_simp, blast)+, simp)
fix evsR1 S A U n s H
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsR1) = H ∪ analz (A ∪ spies evsR1)" and
B: "(evsR1, S, A, U) ∈ protocol" and
C: "Pri_AgrK s ∉ U"
let
?B = "H ∪ A ∪ spies evsR1" and
?C = "A ∪ spies evsR1"
show
"(n ∈ bad ⟶
H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK s) U ⟶
analz (insert (Crypt (symK n) (Pri_AgrK s)) (insert (Pri_AgrK s) ?B)) =
H ∪ analz (insert (Crypt (symK n) (Pri_AgrK s)) (insert (Pri_AgrK s) ?C))) ∧
(n ∉ bad ⟶
H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK s) U ⟶
analz (insert (Crypt (symK n) (Pri_AgrK s)) ?B) =
H ∪ analz (insert (Crypt (symK n) (Pri_AgrK s)) ?C))"
(is "(_ ⟶ _ ⟶ ?T) ∧ (_ ⟶ _ ⟶ ?T')")
proof (rule conjI, (rule_tac [!] impI)+)
assume "H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK s) U"
hence "insert (Pri_AgrK s) H ⊆ range Key ∪ range Pri_AgrK - U"
using C by blast
with A have "analz (insert (Pri_AgrK s) H ∪ A ∪ spies evsR1) =
insert (Pri_AgrK s) H ∪ analz (A ∪ spies evsR1)" ..
hence "analz (insert (Pri_AgrK s) ?B) = H ∪ insert (Pri_AgrK s) (analz ?C)"
by simp
moreover have "{Pri_AgrK s} ⊆ range Key ∪ range Pri_AgrK - U"
using C by simp
with A have "analz ({Pri_AgrK s} ∪ A ∪ spies evsR1) =
{Pri_AgrK s} ∪ analz (A ∪ spies evsR1)" ..
hence "insert (Pri_AgrK s) (analz ?C) = analz (insert (Pri_AgrK s) ?C)"
by simp
ultimately have D: "analz (insert (Pri_AgrK s) ?B) =
H ∪ analz (insert (Pri_AgrK s) ?C)"
by simp
assume "n ∈ bad"
hence E: "Key (invK (symK n)) ∈ analz ?C"
using B by (simp add: pr_symk_analz invK_symK)
have "Key (invK (symK n)) ∈ analz (insert (Pri_AgrK s) ?B)"
by (rule subsetD [OF _ E], rule analz_mono, blast)
hence "analz (insert (Crypt (symK n) (Pri_AgrK s)) (insert (Pri_AgrK s) ?B)) =
insert (Crypt (symK n) (Pri_AgrK s)) (analz (insert (Pri_AgrK s) ?B))"
by (simp add: analz_crypt_in)
moreover have "Key (invK (symK n)) ∈ analz (insert (Pri_AgrK s) ?C)"
by (rule subsetD [OF _ E], rule analz_mono, blast)
hence "analz (insert (Crypt (symK n) (Pri_AgrK s)) (insert (Pri_AgrK s) ?C)) =
insert (Crypt (symK n) (Pri_AgrK s)) (analz (insert (Pri_AgrK s) ?C))"
by (simp add: analz_crypt_in)
ultimately show ?T
using D by simp
next
assume "H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK s) U"
hence D: "H ⊆ range Key ∪ range Pri_AgrK - U"
by blast
with A have E: "analz ?B = H ∪ analz ?C" ..
moreover assume "n ∉ bad"
hence F: "Key (invK (symK n)) ∉ analz ?C"
using B by (simp add: pr_symk_analz invK_symK)
ultimately have "Key (invK (symK n)) ∉ analz ?B"
proof (simp add: invK_symK, insert pr_symk_used [OF B, of n])
qed (rule notI, drule subsetD [OF D], simp)
hence "analz (insert (Crypt (symK n) (Pri_AgrK s)) ?B) =
insert (Crypt (symK n) (Pri_AgrK s)) (analz ?B)"
by (simp add: analz_crypt_out)
moreover have "H ∪ analz (insert (Crypt (symK n) (Pri_AgrK s)) ?C) =
insert (Crypt (symK n) (Pri_AgrK s)) (H ∪ analz ?C)"
using F by (simp add: analz_crypt_out)
ultimately show ?T'
using E by simp
qed
next
fix evsFR1 S A U m s H
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsFR1) = H ∪ analz (A ∪ spies evsFR1)" and
B: "(evsFR1, S, A, U) ∈ protocol" and
C: "Crypt (symK m) (Pri_AgrK s) ∈ synth (analz (A ∪ spies evsFR1))"
let
?B = "H ∪ A ∪ spies evsFR1" and
?C = "A ∪ spies evsFR1"
show "H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (insert (Crypt (symK m) (Pri_AgrK s)) ?B) =
H ∪ analz (insert (Crypt (symK m) (Pri_AgrK s)) ?C)"
(is "_ ⟶ ?T")
proof (rule impI, cases "Key (invK (symK m)) ∈ analz ?C")
case True
assume "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have "analz ?B = H ∪ analz ?C" ..
moreover have "Pri_AgrK s ∈ analz ?C"
proof (insert synth_crypt [OF C], erule disjE, erule_tac [2] conjE)
assume "Crypt (symK m) (Pri_AgrK s) ∈ analz ?C"
thus ?thesis
using True by (rule analz.Decrypt)
next
assume "Pri_AgrK s ∈ synth (analz ?C)"
thus ?thesis
by (rule synth_simp_intro, simp)
qed
moreover from this have "Pri_AgrK s ∈ analz ?B"
by (rule rev_subsetD, rule_tac analz_mono, blast)
ultimately have D: "analz (insert (Pri_AgrK s) ?B) =
H ∪ analz (insert (Pri_AgrK s) ?C)"
by (simp add: analz_simp_insert_1)
have "Key (invK (symK m)) ∈ analz ?B"
by (rule subsetD [OF _ True], rule analz_mono, blast)
hence "analz (insert (Crypt (symK m) (Pri_AgrK s)) ?B) =
insert (Crypt (symK m) (Pri_AgrK s)) (analz (insert (Pri_AgrK s) ?B))"
by (simp add: analz_crypt_in)
moreover have "analz (insert (Crypt (symK m) (Pri_AgrK s)) ?C) =
insert (Crypt (symK m) (Pri_AgrK s)) (analz (insert (Pri_AgrK s) ?C))"
using True by (simp add: analz_crypt_in)
ultimately show ?T
using D by simp
next
case False
moreover assume D: "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have E: "analz ?B = H ∪ analz ?C" ..
ultimately have "Key (invK (symK m)) ∉ analz ?B"
proof (simp add: invK_symK, insert pr_symk_used [OF B, of m])
qed (rule notI, drule subsetD [OF D], simp)
hence "analz (insert (Crypt (symK m) (Pri_AgrK s)) ?B) =
insert (Crypt (symK m) (Pri_AgrK s)) (analz ?B)"
by (simp add: analz_crypt_out)
moreover have "H ∪ analz (insert (Crypt (symK m) (Pri_AgrK s)) ?C) =
insert (Crypt (symK m) (Pri_AgrK s)) (H ∪ analz ?C)"
using False by (simp add: analz_crypt_out)
ultimately show ?T
using E by simp
qed
next
fix evsC2 S A U a H and m :: nat
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsC2) = H ∪ analz (A ∪ spies evsC2)" and
B: "Pri_AgrK a ∉ U"
let
?B = "H ∪ A ∪ spies evsC2" and
?C = "A ∪ spies evsC2"
show
"(m = 0 ⟶
H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK a) U ⟶
insert (pubAK a) (analz (insert (Pri_AgrK a) ?B)) =
insert (pubAK a) (H ∪ analz (insert (Pri_AgrK a) ?C))) ∧
(0 < m ⟶
H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK a) U ⟶
insert (pubAK a) (analz ?B) =
insert (pubAK a) (H ∪ analz ?C))"
(is "(_ ⟶ _ ⟶ ?T) ∧ (_ ⟶ _ ⟶ ?T')")
proof (rule conjI, (rule_tac [!] impI)+)
assume "H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK a) U"
hence "insert (Pri_AgrK a) H ⊆ range Key ∪ range Pri_AgrK - U"
using B by blast
with A have "analz (insert (Pri_AgrK a) H ∪ A ∪ spies evsC2) =
insert (Pri_AgrK a) H ∪ analz (A ∪ spies evsC2)" ..
hence "analz (insert (Pri_AgrK a) ?B) = H ∪ insert (Pri_AgrK a) (analz ?C)"
by simp
moreover have "{Pri_AgrK a} ⊆ range Key ∪ range Pri_AgrK - U"
using B by simp
with A have "analz ({Pri_AgrK a} ∪ A ∪ spies evsC2) =
{Pri_AgrK a} ∪ analz (A ∪ spies evsC2)" ..
hence "insert (Pri_AgrK a) (analz ?C) = analz (insert (Pri_AgrK a) ?C)"
by simp
ultimately have "analz (insert (Pri_AgrK a) ?B) =
H ∪ analz (insert (Pri_AgrK a) ?C)"
by simp
thus ?T
by simp
next
assume "H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK a) U"
hence "H ⊆ range Key ∪ range Pri_AgrK - U"
by blast
with A have "analz ?B = H ∪ analz ?C" ..
thus ?T'
by simp
qed
next
fix evsR2 S A U b H
assume A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsR2) = H ∪ analz (A ∪ spies evsR2)"
let
?B = "H ∪ A ∪ spies evsR2" and
?C = "A ∪ spies evsR2"
show "H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK b) U ⟶
insert (pubAK b) (analz ?B) = insert (pubAK b) (H ∪ analz ?C)"
(is "_ ⟶ ?T")
proof
assume "H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK b) U"
hence "H ⊆ range Key ∪ range Pri_AgrK - U"
by blast
with A have "analz ?B = H ∪ analz ?C" ..
thus ?T
by simp
qed
next
fix evsC3 S A U s a b c H and m :: nat
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsC3) = H ∪ analz (A ∪ spies evsC3)" and
B: "Pri_AgrK c ∉ U"
let
?B = "H ∪ A ∪ spies evsC3" and
?C = "A ∪ spies evsC3"
show
"(m = 0 ⟶
H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK c) U ⟶
insert (pubAK (c * (s + a * b))) (analz (insert (Pri_AgrK c) ?B)) =
insert (pubAK (c * (s + a * b))) (H ∪ analz (insert (Pri_AgrK c) ?C))) ∧
(0 < m ⟶
H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK c) U ⟶
insert (pubAK (c * (s + a * b))) (analz ?B) =
insert (pubAK (c * (s + a * b))) (H ∪ analz ?C))"
(is "(_ ⟶ _ ⟶ ?T) ∧ (_ ⟶ _ ⟶ ?T')")
proof (rule conjI, (rule_tac [!] impI)+)
assume "H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK c) U"
hence "insert (Pri_AgrK c) H ⊆ range Key ∪ range Pri_AgrK - U"
using B by blast
with A have "analz (insert (Pri_AgrK c) H ∪ A ∪ spies evsC3) =
insert (Pri_AgrK c) H ∪ analz (A ∪ spies evsC3)" ..
hence "analz (insert (Pri_AgrK c) ?B) = H ∪ insert (Pri_AgrK c) (analz ?C)"
by simp
moreover have "{Pri_AgrK c} ⊆ range Key ∪ range Pri_AgrK - U"
using B by simp
with A have "analz ({Pri_AgrK c} ∪ A ∪ spies evsC3) =
{Pri_AgrK c} ∪ analz (A ∪ spies evsC3)" ..
hence "insert (Pri_AgrK c) (analz ?C) = analz (insert (Pri_AgrK c) ?C)"
by simp
ultimately have "analz (insert (Pri_AgrK c) ?B) =
H ∪ analz (insert (Pri_AgrK c) ?C)"
by simp
thus ?T
by simp
next
assume "H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK c) U"
hence "H ⊆ range Key ∪ range Pri_AgrK - U"
by blast
with A have "analz ?B = H ∪ analz ?C" ..
thus ?T'
by simp
qed
next
fix evsR3 S A U n run s s' a b c d X H
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsR3) = H ∪ analz (A ∪ spies evsR3)" and
B: "Key (sesK (c * d * (s + a * b))) ∉ U"
(is "Key ?K ∉ _")
let
?B = "H ∪ A ∪ spies evsR3" and
?C = "A ∪ spies evsR3" and
?K' = "sesK (c * d * (s' + a * b))"
show
"(s' = s ∧ Pri_AgrK c ∈ analz (A ∪ spies evsR3) ⟶
H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK d)
(insert (Key ?K) (insert ⦃Key ?K, Agent X, Number n, Number run⦄ U)) ⟶
insert (pubAK (d * (s + a * b))) (analz (insert (Key ?K) ?B)) =
insert (pubAK (d * (s + a * b))) (H ∪ analz (insert (Key ?K) ?C))) ∧
((s' = s ⟶ Pri_AgrK c ∉ analz (A ∪ spies evsR3)) ⟶
H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK d) (insert (Key ?K')
(insert (Key ?K) (insert ⦃Key ?K, Agent X, Number n, Number run⦄ U))) ⟶
insert (pubAK (d * (s + a * b))) (analz ?B) =
insert (pubAK (d * (s + a * b))) (H ∪ analz ?C))"
(is "(_ ⟶ _ ⟶ ?T) ∧ (_ ⟶ _ ⟶ ?T')")
proof (rule conjI, (rule_tac [!] impI)+)
assume "H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK d)
(insert (Key ?K) (insert ⦃Key ?K, Agent X, Number n, Number run⦄ U))"
hence "insert (Key ?K) H ⊆ range Key ∪ range Pri_AgrK - U"
using B by blast
with A have "analz (insert (Key ?K) H ∪ A ∪ spies evsR3) =
insert (Key ?K) H ∪ analz (A ∪ spies evsR3)" ..
hence "analz (insert (Key ?K) ?B) = H ∪ insert (Key ?K) (analz ?C)"
by simp
moreover have "{Key ?K} ⊆ range Key ∪ range Pri_AgrK - U"
using B by simp
with A have "analz ({Key ?K} ∪ A ∪ spies evsR3) =
{Key ?K} ∪ analz (A ∪ spies evsR3)" ..
hence "insert (Key ?K) (analz ?C) = analz (insert (Key ?K) ?C)"
by simp
ultimately have "analz (insert (Key ?K) ?B) = H ∪ analz (insert (Key ?K) ?C)"
by simp
thus ?T
by simp
next
assume "H ⊆ range Key ∪ range Pri_AgrK - insert (Pri_AgrK d) (insert (Key ?K')
(insert (Key ?K) (insert ⦃Key ?K, Agent X, Number n, Number run⦄ U)))"
hence "H ⊆ range Key ∪ range Pri_AgrK - U"
by blast
with A have "analz ?B = H ∪ analz ?C" ..
thus ?T'
by simp
qed
next
fix evsFR3 S A U m n run s a b c d H
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsFR3) = H ∪ analz (A ∪ spies evsFR3)" and
B: "Key (sesK (c * d * (s + a * b))) ∉ U"
(is "Key ?K ∉ _")
let
?B = "H ∪ A ∪ spies evsFR3" and
?C = "A ∪ spies evsFR3"
show
"H ⊆ range Key ∪ range Pri_AgrK - insert (Key ?K)
(insert ⦃Key ?K, Agent (User m), Number n, Number run⦄ U) ⟶
insert (pubAK (d * (s + a * b))) (analz (insert (Key ?K) ?B)) =
insert (pubAK (d * (s + a * b))) (H ∪ analz (insert (Key ?K) ?C))"
(is "_ ⟶ ?T")
proof
assume "H ⊆ range Key ∪ range Pri_AgrK - insert (Key ?K)
(insert ⦃Key ?K, Agent (User m), Number n, Number run⦄ U)"
hence "insert (Key ?K) H ⊆ range Key ∪ range Pri_AgrK - U"
using B by blast
with A have "analz (insert (Key ?K) H ∪ A ∪ spies evsFR3) =
insert (Key ?K) H ∪ analz (A ∪ spies evsFR3)" ..
hence "analz (insert (Key ?K) ?B) = H ∪ insert (Key ?K) (analz ?C)"
by simp
moreover have "{Key ?K} ⊆ range Key ∪ range Pri_AgrK - U"
using B by simp
with A have "analz ({Key ?K} ∪ A ∪ spies evsFR3) =
{Key ?K} ∪ analz (A ∪ spies evsFR3)" ..
hence "insert (Key ?K) (analz ?C) = analz (insert (Key ?K) ?C)"
by simp
ultimately have "analz (insert (Key ?K) ?B) = H ∪ analz (insert (Key ?K) ?C)"
by simp
thus ?T
by simp
qed
next
fix evsC4 S A U m n run c f H
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsC4) = H ∪ analz (A ∪ spies evsC4)" and
B: "(evsC4, S, A, U) ∈ protocol" and
C: "⦃Key (sesK (c * f)), Agent (User m), Number n, Number run⦄ ∈ U"
let
?B = "H ∪ A ∪ spies evsC4" and
?C = "A ∪ spies evsC4"
show "H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (insert (Crypt (sesK (c * f)) (pubAK f)) ?B) =
H ∪ analz (insert (Crypt (sesK (c * f)) (pubAK f)) ?C)"
(is "_ ⟶ ?T")
proof (rule impI, cases "Key (invK (sesK (c * f))) ∈ analz ?C")
case True
assume "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have D: "analz ?B = H ∪ analz ?C" ..
have "Key (invK (sesK (c * f))) ∈ analz ?B"
by (rule subsetD [OF _ True], rule analz_mono, blast)
hence "analz (insert (Crypt (sesK (c * f)) (pubAK f)) ?B) =
insert (Crypt (sesK (c * f)) (pubAK f)) (insert (pubAK f) (analz ?B))"
by (simp add: analz_crypt_in analz_simp_insert_2)
moreover have "H ∪ analz (insert (Crypt (sesK (c * f)) (pubAK f)) ?C) =
insert (Crypt (sesK (c * f)) (pubAK f)) (insert (pubAK f) (H ∪ analz ?C))"
using True by (simp add: analz_crypt_in analz_simp_insert_2)
ultimately show ?T
using D by simp
next
case False
moreover assume D: "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have E: "analz ?B = H ∪ analz ?C" ..
ultimately have "Key (invK (sesK (c * f))) ∉ analz ?B"
proof (simp add: invK_sesK, insert pr_sesk_user_2 [OF B C])
qed (rule notI, drule subsetD [OF D], simp)
hence "analz (insert (Crypt (sesK (c * f)) (pubAK f)) ?B) =
insert (Crypt (sesK (c * f)) (pubAK f)) (analz ?B)"
by (simp add: analz_crypt_out)
moreover have "H ∪ analz (insert (Crypt (sesK (c * f)) (pubAK f)) ?C) =
insert (Crypt (sesK (c * f)) (pubAK f)) (H ∪ analz ?C)"
using False by (simp add: analz_crypt_out)
ultimately show ?T
using E by simp
qed
next
fix evsFC4 S A U n run s a b d e H
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsFC4) = H ∪ analz (A ∪ spies evsFC4)" and
B: "(evsFC4, S, A, U) ∈ protocol" and
C: "IntAgrK (S (Card n, n, run)) = Some d" and
D: "ExtAgrK (S (Card n, n, run)) = Some e"
let
?B = "H ∪ A ∪ spies evsFC4" and
?C = "A ∪ spies evsFC4" and
?f = "d * (s + a * b)"
show "H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (insert (Crypt (sesK (d * e)) (pubAK ?f)) ?B) =
H ∪ analz (insert (Crypt (sesK (d * e)) (pubAK ?f)) ?C)"
(is "_ ⟶ ?T")
proof (rule impI, cases "Key (invK (sesK (d * e))) ∈ analz ?C")
case True
assume "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have E: "analz ?B = H ∪ analz ?C" ..
have "Key (invK (sesK (d * e))) ∈ analz ?B"
by (rule subsetD [OF _ True], rule analz_mono, blast)
hence "analz (insert (Crypt (sesK (d * e)) (pubAK ?f)) ?B) =
insert (Crypt (sesK (d * e)) (pubAK ?f)) (insert (pubAK ?f) (analz ?B))"
by (simp add: analz_crypt_in analz_simp_insert_2)
moreover have "H ∪ analz (insert (Crypt (sesK (d * e)) (pubAK ?f)) ?C) =
insert (Crypt (sesK (d * e)) (pubAK ?f)) (insert (pubAK ?f) (H ∪ analz ?C))"
using True by (simp add: analz_crypt_in analz_simp_insert_2)
ultimately show ?T
using E by simp
next
case False
moreover assume E: "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have F: "analz ?B = H ∪ analz ?C" ..
ultimately have "Key (invK (sesK (d * e))) ∉ analz ?B"
proof (simp add: invK_sesK, insert pr_sesk_card [OF B C D])
qed (rule notI, drule subsetD [OF E], simp)
hence "analz (insert (Crypt (sesK (d * e)) (pubAK ?f)) ?B) =
insert (Crypt (sesK (d * e)) (pubAK ?f)) (analz ?B)"
by (simp add: analz_crypt_out)
moreover have "H ∪ analz (insert (Crypt (sesK (d * e)) (pubAK ?f)) ?C) =
insert (Crypt (sesK (d * e)) (pubAK ?f)) (H ∪ analz ?C)"
using False by (simp add: analz_crypt_out)
ultimately show ?T
using F by simp
qed
next
fix evsR4 S A U n run b d e H
let
?B = "H ∪ A ∪ spies evsR4" and
?C = "A ∪ spies evsR4" and
?H = "Hash (pubAK (priAK n))" and
?M = "⦃pubAK (priAK n), Crypt (priSK CA) (Hash (pubAK (priAK n)))⦄" and
?M' = "⦃pubAK e, Auth_Data (priAK n) b, pubAK (priAK n),
Crypt (priSK CA) (Hash (pubAK (priAK n)))⦄"
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsR4) = H ∪ analz (A ∪ spies evsR4)" and
B: "(evsR4, S, A, U) ∈ protocol" and
C: "IntMapK (S (Card n, n, run)) = Some b" and
D: "IntAgrK (S (Card n, n, run)) = Some d" and
E: "ExtAgrK (S (Card n, n, run)) = Some e"
show "H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (insert (Crypt (sesK (d * e)) ?M') ?B) =
H ∪ analz (insert (Crypt (sesK (d * e)) ?M') ?C)"
(is "_ ⟶ ?T")
proof
assume F: "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have G: "analz ?B = H ∪ analz ?C" ..
have H: "Key (pubSK CA) ∈ analz ?C"
using B by (rule pr_valid_key_analz)
hence I: "analz (insert (Crypt (priSK CA) ?H) ?C) =
{Crypt (priSK CA) ?H, ?H} ∪ analz ?C"
by (simp add: analz_crypt_in analz_simp_insert_2)
have "Key (pubSK CA) ∈ analz ?B"
by (rule subsetD [OF _ H], rule analz_mono, blast)
hence J: "analz (insert (Crypt (priSK CA) ?H) ?B) =
{Crypt (priSK CA) ?H, ?H} ∪ analz ?B"
by (simp add: analz_crypt_in analz_simp_insert_2)
have K: "Pri_AgrK (priAK n) ∉ analz ?C"
using B by (rule pr_auth_key_analz)
hence L: "Pri_AgrK (priAK n) ∉ analz (insert (Crypt (priSK CA) ?H) ?C)"
using I by simp
have M: "Pri_AgrK b ∉ analz ?C"
using B and C by (rule pr_int_mapk_analz)
hence N: "Pri_AgrK b ∉ analz (insert (Crypt (priSK CA) ?H) ?C)"
using I by simp
have "Pri_AgrK (priAK n) ∈ U"
using B by (rule pr_auth_key_used)
hence "Pri_AgrK (priAK n) ∉ H"
using F by blast
hence O: "Pri_AgrK (priAK n) ∉ analz (insert (Crypt (priSK CA) ?H) ?B)"
using G and J and K by simp
have "Pri_AgrK b ∈ U"
using B and C by (rule pr_int_mapk_used)
hence "Pri_AgrK b ∉ H"
using F by blast
hence P: "Pri_AgrK b ∉ analz (insert (Crypt (priSK CA) ?H) ?B)"
using G and J and M by simp
show ?T
proof (cases "Key (invK (sesK (d * e))) ∈ analz ?C")
case True
have Q: "Key (invK (sesK (d * e))) ∈ analz ?B"
by (rule subsetD [OF _ True], rule analz_mono, blast)
show ?T
proof (simp add: analz_crypt_in analz_mpair analz_simp_insert_2 True Q,
rule equalityI, (rule_tac [!] insert_mono)+)
show "analz (insert (Auth_Data (priAK n) b) (insert ?M ?B)) ⊆
H ∪ analz (insert (Auth_Data (priAK n) b) (insert ?M ?C))"
proof (subst (1 2) insert_commute, simp add: analz_mpair analz_simp_insert_2
del: Un_insert_right, subst (1 3) insert_commute,
subst analz_auth_data_out [OF O P], subst analz_auth_data_out [OF L N])
qed (auto simp add: G I J)
next
show "H ∪ analz (insert (Auth_Data (priAK n) b) (insert ?M ?C)) ⊆
analz (insert (Auth_Data (priAK n) b) (insert ?M ?B))"
proof (subst (1 2) insert_commute, simp add: analz_mpair analz_simp_insert_2
del: Un_insert_right Un_subset_iff semilattice_sup_class.sup.bounded_iff,
subst (1 3) insert_commute, subst analz_auth_data_out [OF L N],
subst analz_auth_data_out [OF O P])
qed (auto simp add: G I J)
qed
next
case False
hence "Key (invK (sesK (d * e))) ∉ analz ?B"
proof (simp add: invK_sesK G, insert pr_sesk_card [OF B D E])
qed (rule notI, drule subsetD [OF F], simp)
hence "analz (insert (Crypt (sesK (d * e)) ?M') ?B) =
insert (Crypt (sesK (d * e)) ?M') (analz ?B)"
by (simp add: analz_crypt_out)
moreover have "H ∪ analz (insert (Crypt (sesK (d * e)) ?M') ?C) =
insert (Crypt (sesK (d * e)) ?M') (H ∪ analz ?C)"
using False by (simp add: analz_crypt_out)
ultimately show ?T
using G by simp
qed
qed
next
fix evsFR4 S A U m n run s a b c f g H
let
?B = "H ∪ A ∪ spies evsFR4" and
?C = "A ∪ spies evsFR4" and
?H = "Hash (pubAK g)" and
?M = "⦃pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄" and
?M' = "⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄"
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsFR4) = H ∪ analz (A ∪ spies evsFR4)" and
B: "(evsFR4, S, A, U) ∈ protocol" and
C: "IntAgrK (S (User m, n, run)) = Some c" and
D: "ExtAgrK (S (User m, n, run)) = Some f" and
E: "Crypt (sesK (c * f)) ?M' ∈ synth (analz ?C)"
have F:
"Key (invK (sesK (c * f))) ∈ analz ?C ⟶
Pri_AgrK b ∈ analz ?C ∨ Pri_AgrK g ∈ analz ?C ⟶
Pri_AgrK b ∈ analz ?C ∧ Pri_AgrK g ∈ analz ?C"
(is "?P ⟶ ?Q ⟶ ?R")
proof (rule impI)+
assume ?P and ?Q
have "Crypt (sesK (c * f)) ?M' ∈ analz ?C ∨
?M' ∈ synth (analz ?C) ∧ Key (sesK (c * f)) ∈ analz ?C"
using E by (rule synth_crypt)
moreover {
assume "Crypt (sesK (c * f)) ?M' ∈ analz ?C"
hence "?M' ∈ analz ?C"
using ‹?P› by (rule analz.Decrypt)
hence "⦃Auth_Data g b, pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ analz ?C"
by (rule analz.Snd)
hence G: "Auth_Data g b ∈ analz ?C"
by (rule analz.Fst)
have ?R
proof (rule disjE [OF ‹?Q›])
assume "Pri_AgrK b ∈ analz ?C"
moreover from this have "Pri_AgrK g ∈ analz ?C"
by (rule analz.Auth_Fst [OF G])
ultimately show ?R ..
next
assume "Pri_AgrK g ∈ analz ?C"
moreover from this have "Pri_AgrK b ∈ analz ?C"
by (rule analz.Auth_Snd [OF G])
ultimately show ?R
by simp
qed
}
moreover {
assume "?M' ∈ synth (analz ?C) ∧ Key (sesK (c * f)) ∈ analz ?C"
hence "?M' ∈ synth (analz ?C)" ..
hence "⦃Auth_Data g b, pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ synth (analz ?C)"
by (rule synth_analz_snd)
hence "Auth_Data g b ∈ synth (analz ?C)"
by (rule synth_analz_fst)
hence "Auth_Data g b ∈ analz ?C ∨
Pri_AgrK g ∈ analz ?C ∧ Pri_AgrK b ∈ analz ?C"
by (rule synth_auth_data)
moreover {
assume G: "Auth_Data g b ∈ analz ?C"
have ?R
proof (rule disjE [OF ‹?Q›])
assume "Pri_AgrK b ∈ analz ?C"
moreover from this have "Pri_AgrK g ∈ analz ?C"
by (rule analz.Auth_Fst [OF G])
ultimately show ?R ..
next
assume "Pri_AgrK g ∈ analz ?C"
moreover from this have "Pri_AgrK b ∈ analz ?C"
by (rule analz.Auth_Snd [OF G])
ultimately show ?R
by simp
qed
}
moreover {
assume "Pri_AgrK g ∈ analz ?C ∧ Pri_AgrK b ∈ analz ?C"
hence ?R
by simp
}
ultimately have ?R ..
}
ultimately show ?R ..
qed
show "H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (insert (Crypt (sesK (c * f)) ?M') ?B) =
H ∪ analz (insert (Crypt (sesK (c * f)) ?M') ?C)"
(is "_ ⟶ ?T")
proof
assume G: "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have H: "analz ?B = H ∪ analz ?C" ..
have I: "Key (pubSK CA) ∈ analz ?C"
using B by (rule pr_valid_key_analz)
hence J: "analz (insert (Crypt (priSK CA) ?H) ?C) =
{Crypt (priSK CA) ?H, ?H} ∪ analz ?C"
by (simp add: analz_crypt_in analz_simp_insert_2)
have "Key (pubSK CA) ∈ analz ?B"
by (rule subsetD [OF _ I], rule analz_mono, blast)
hence K: "analz (insert (Crypt (priSK CA) ?H) ?B) =
{Crypt (priSK CA) ?H, ?H} ∪ analz ?B"
by (simp add: analz_crypt_in analz_simp_insert_2)
show ?T
proof (cases "Key (invK (sesK (c * f))) ∈ analz ?C",
cases "Pri_AgrK g ∈ analz ?C ∨ Pri_AgrK b ∈ analz ?C", simp_all)
assume L: "Key (invK (sesK (c * f))) ∈ analz ?C"
have M: "Key (invK (sesK (c * f))) ∈ analz ?B"
by (rule subsetD [OF _ L], rule analz_mono, blast)
assume N: "Pri_AgrK g ∈ analz ?C ∨ Pri_AgrK b ∈ analz ?C"
hence O: "Pri_AgrK g ∈ analz (insert (Crypt (priSK CA) ?H) ?C) ∨
Pri_AgrK b ∈ analz (insert (Crypt (priSK CA) ?H) ?C)"
using J by simp
have "Pri_AgrK g ∈ analz ?B ∨ Pri_AgrK b ∈ analz ?B"
using H and N by blast
hence P: "Pri_AgrK g ∈ analz (insert (Crypt (priSK CA) ?H) ?B) ∨
Pri_AgrK b ∈ analz (insert (Crypt (priSK CA) ?H) ?B)"
using K by simp
have Q: "Pri_AgrK b ∈ analz ?C ∧ Pri_AgrK g ∈ analz ?C"
using F and L and N by blast
hence "Pri_AgrK g ∈ analz (insert (Crypt (priSK CA) ?H) ?C)"
using J by simp
hence R: "Pri_AgrK g ∈ analz (insert (Pri_AgrK b)
(insert (Crypt (priSK CA) ?H) ?C))"
by (rule rev_subsetD, rule_tac analz_mono, blast)
have S: "Pri_AgrK b ∈ analz (insert (Crypt (priSK CA) ?H) ?C)"
using J and Q by simp
have T: "Pri_AgrK b ∈ analz ?B ∧ Pri_AgrK g ∈ analz ?B"
using H and Q by simp
hence "Pri_AgrK g ∈ analz (insert (Crypt (priSK CA) ?H) ?B)"
using K by simp
hence U: "Pri_AgrK g ∈ analz (insert (Pri_AgrK b)
(insert (Crypt (priSK CA) ?H) ?B))"
by (rule rev_subsetD, rule_tac analz_mono, blast)
have V: "Pri_AgrK b ∈ analz (insert (Crypt (priSK CA) ?H) ?B)"
using K and T by simp
show ?T
proof (simp add: analz_crypt_in analz_mpair analz_simp_insert_2 L M,
rule equalityI, (rule_tac [!] insert_mono)+)
show "analz (insert (Auth_Data g b) (insert ?M ?B)) ⊆
H ∪ analz (insert (Auth_Data g b) (insert ?M ?C))"
proof (subst (1 2) insert_commute, simp add: analz_mpair analz_simp_insert_2
del: Un_insert_right, subst (1 3) insert_commute,
subst analz_auth_data_in [OF P], subst analz_auth_data_in [OF O],
simp del: Un_insert_right)
show
"analz (insert (Pri_AgrK g) (insert (Pri_AgrK b)
(insert (Crypt (priSK CA) ?H) ?B))) ⊆
H ∪ insert ?M (insert (pubAK g) (insert (Auth_Data g b)
(analz (insert (Pri_AgrK g) (insert (Pri_AgrK b)
(insert (Crypt (priSK CA) ?H) ?C))))))"
proof (subst analz_simp_insert_1 [OF U], subst analz_simp_insert_1 [OF V],
subst analz_simp_insert_1 [OF R], subst analz_simp_insert_1 [OF S])
qed (auto simp add: H J K)
qed
next
show "H ∪ analz (insert (Auth_Data g b) (insert ?M ?C)) ⊆
analz (insert (Auth_Data g b) (insert ?M ?B))"
proof (subst (1 2) insert_commute, simp add: analz_mpair analz_simp_insert_2
del: Un_insert_right Un_subset_iff semilattice_sup_class.sup.bounded_iff,
subst (2 4) insert_commute, subst analz_auth_data_in [OF O],
subst analz_auth_data_in [OF P], simp only: Un_insert_left Un_empty_left)
show
"H ∪ insert ?M (insert (pubAK g) (insert (Auth_Data g b)
(analz (insert (Pri_AgrK g) (insert (Pri_AgrK b)
(insert (Crypt (priSK CA) ?H) ?C)))))) ⊆
insert ?M (insert (pubAK g) (insert (Auth_Data g b)
(analz (insert (Pri_AgrK g) (insert (Pri_AgrK b)
(insert (Crypt (priSK CA) ?H) ?B))))))"
proof (subst analz_simp_insert_1 [OF R], subst analz_simp_insert_1 [OF S],
subst analz_simp_insert_1 [OF U], subst analz_simp_insert_1 [OF V])
qed (auto simp add: H J K)
qed
qed
next
assume L: "Key (invK (sesK (c * f))) ∈ analz ?C"
have M: "Key (invK (sesK (c * f))) ∈ analz ?B"
by (rule subsetD [OF _ L], rule analz_mono, blast)
assume N: "Pri_AgrK g ∉ analz ?C ∧ Pri_AgrK b ∉ analz ?C"
hence O: "Pri_AgrK g ∉ analz (insert (Crypt (priSK CA) ?H) ?C)"
using J by simp
have P: "Pri_AgrK b ∉ analz (insert (Crypt (priSK CA) ?H) ?C)"
using J and N by simp
have Q: "Pri_AgrK g ∈ U ∧ Pri_AgrK b ∈ U"
proof -
have "Crypt (sesK (c * f)) ?M' ∈ analz ?C ∨
?M' ∈ synth (analz ?C) ∧ Key (sesK (c * f)) ∈ analz ?C"
using E by (rule synth_crypt)
moreover {
assume "Crypt (sesK (c * f)) ?M' ∈ analz ?C"
hence "Crypt (sesK (c * f)) ?M' ∈ parts ?C"
by (rule subsetD [OF analz_parts_subset])
hence "?M' ∈ parts ?C"
by (rule parts.Body)
hence "⦃Auth_Data g b, pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ parts ?C"
by (rule parts.Snd)
hence R: "Auth_Data g b ∈ parts ?C"
by (rule parts.Fst)
hence "Pri_AgrK g ∈ parts ?C"
by (rule parts.Auth_Fst)
hence "Pri_AgrK g ∈ U"
by (rule contrapos_pp, rule_tac pr_pri_agrk_parts [OF B])
moreover have "Pri_AgrK b ∈ parts ?C"
using R by (rule parts.Auth_Snd)
hence "Pri_AgrK b ∈ U"
by (rule contrapos_pp, rule_tac pr_pri_agrk_parts [OF B])
ultimately have ?thesis ..
}
moreover {
assume "?M' ∈ synth (analz ?C) ∧
Key (sesK (c * f)) ∈ analz ?C"
hence "?M' ∈ synth (analz ?C)" ..
hence "⦃Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄ ∈ synth (analz ?C)"
by (rule synth_analz_snd)
hence "Auth_Data g b ∈ synth (analz ?C)"
by (rule synth_analz_fst)
hence "Auth_Data g b ∈ analz ?C ∨
Pri_AgrK g ∈ analz ?C ∧ Pri_AgrK b ∈ analz ?C"
by (rule synth_auth_data)
moreover {
assume "Auth_Data g b ∈ analz ?C"
hence R: "Auth_Data g b ∈ parts ?C"
by (rule subsetD [OF analz_parts_subset])
hence "Pri_AgrK g ∈ parts ?C"
by (rule parts.Auth_Fst)
hence "Pri_AgrK g ∈ U"
by (rule contrapos_pp, rule_tac pr_pri_agrk_parts [OF B])
moreover have "Pri_AgrK b ∈ parts ?C"
using R by (rule parts.Auth_Snd)
hence "Pri_AgrK b ∈ U"
by (rule contrapos_pp, rule_tac pr_pri_agrk_parts [OF B])
ultimately have ?thesis ..
}
moreover {
assume R: "Pri_AgrK g ∈ analz ?C ∧ Pri_AgrK b ∈ analz ?C"
hence "Pri_AgrK g ∈ analz ?C" ..
hence "Pri_AgrK g ∈ parts ?C"
by (rule subsetD [OF analz_parts_subset])
hence "Pri_AgrK g ∈ U"
by (rule contrapos_pp, rule_tac pr_pri_agrk_parts [OF B])
moreover have "Pri_AgrK b ∈ analz ?C"
using R ..
hence "Pri_AgrK b ∈ parts ?C"
by (rule subsetD [OF analz_parts_subset])
hence "Pri_AgrK b ∈ U"
by (rule contrapos_pp, rule_tac pr_pri_agrk_parts [OF B])
ultimately have ?thesis ..
}
ultimately have ?thesis ..
}
ultimately show ?thesis ..
qed
have R: "Pri_AgrK g ∉ analz ?B ∧ Pri_AgrK b ∉ analz ?B"
proof (simp add: H N, rule conjI, rule_tac [!] notI, drule_tac [!] subsetD [OF G])
qed (simp_all add: Q)
hence S: "Pri_AgrK g ∉ analz (insert (Crypt (priSK CA) ?H) ?B)"
using K by simp
have T: "Pri_AgrK b ∉ analz (insert (Crypt (priSK CA) ?H) ?B)"
using K and R by simp
show ?T
proof (simp add: analz_crypt_in analz_mpair analz_simp_insert_2 L M,
rule equalityI, (rule_tac [!] insert_mono)+)
show "analz (insert (Auth_Data g b) (insert ?M ?B)) ⊆
H ∪ analz (insert (Auth_Data g b) (insert ?M ?C))"
proof (subst (1 2) insert_commute, simp add: analz_mpair analz_simp_insert_2
del: Un_insert_right, subst (1 3) insert_commute,
subst analz_auth_data_out [OF S T], subst analz_auth_data_out [OF O P])
qed (auto simp add: H J K)
next
show "H ∪ analz (insert (Auth_Data g b) (insert ?M ?C)) ⊆
analz (insert (Auth_Data g b) (insert ?M ?B))"
proof (subst (1 2) insert_commute, simp add: analz_mpair analz_simp_insert_2
del: Un_insert_right Un_subset_iff semilattice_sup_class.sup.bounded_iff,
subst (2 4) insert_commute, subst analz_auth_data_out [OF O P],
subst analz_auth_data_out [OF S T])
qed (simp add: H J K)
qed
next
assume L: "Key (invK (sesK (c * f))) ∉ analz ?C"
hence "Key (invK (sesK (c * f))) ∉ analz ?B"
proof (simp add: invK_sesK, insert pr_sesk_user_1 [OF B C D,
THEN pr_sesk_user_2 [OF B]])
qed (rule notI, simp add: H, drule subsetD [OF G], simp)
hence "analz (insert (Crypt (sesK (c * f)) ?M') ?B) =
insert (Crypt (sesK (c * f)) ?M') (analz ?B)"
by (simp add: analz_crypt_out)
moreover have "H ∪ analz (insert (Crypt (sesK (c * f)) ?M') ?C) =
insert (Crypt (sesK (c * f)) ?M') (H ∪ analz ?C)"
using L by (simp add: analz_crypt_out)
ultimately show ?T
using H by simp
qed
qed
next
fix evsC5 S A U m n run c f H
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsC5) = H ∪ analz (A ∪ spies evsC5)" and
B: "(evsC5, S, A, U) ∈ protocol" and
C: "IntAgrK (S (User m, n, run)) = Some c" and
D: "ExtAgrK (S (User m, n, run)) = Some f"
let
?B = "H ∪ A ∪ spies evsC5" and
?C = "A ∪ spies evsC5"
show "H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (insert (Crypt (sesK (c * f)) (Passwd m)) ?B) =
H ∪ analz (insert (Crypt (sesK (c * f)) (Passwd m)) ?C)"
(is "_ ⟶ ?T")
proof (rule impI, cases "Key (invK (sesK (c * f))) ∈ analz ?C")
case True
assume "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have E: "analz ?B = H ∪ analz ?C" ..
have "Key (invK (sesK (c * f))) ∈ analz ?B"
by (rule subsetD [OF _ True], rule analz_mono, blast)
hence "analz (insert (Crypt (sesK (c * f)) (Passwd m)) ?B) =
insert (Crypt (sesK (c * f)) (Passwd m)) (insert (Passwd m) (analz ?B))"
by (simp add: analz_crypt_in analz_simp_insert_2)
moreover have "H ∪ analz (insert (Crypt (sesK (c * f)) (Passwd m)) ?C) =
insert (Crypt (sesK (c * f)) (Passwd m)) (insert (Passwd m) (H ∪ analz ?C))"
using True by (simp add: analz_crypt_in analz_simp_insert_2)
ultimately show ?T
using E by simp
next
case False
moreover assume E: "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have F: "analz ?B = H ∪ analz ?C" ..
ultimately have "Key (invK (sesK (c * f))) ∉ analz ?B"
proof (simp add: invK_sesK, insert pr_sesk_user_1 [OF B C D,
THEN pr_sesk_user_2 [OF B]])
qed (rule notI, drule subsetD [OF E], simp)
hence "analz (insert (Crypt (sesK (c * f)) (Passwd m)) ?B) =
insert (Crypt (sesK (c * f)) (Passwd m)) (analz ?B)"
by (simp add: analz_crypt_out)
moreover have "H ∪ analz (insert (Crypt (sesK (c * f)) (Passwd m)) ?C) =
insert (Crypt (sesK (c * f)) (Passwd m)) (H ∪ analz ?C)"
using False by (simp add: analz_crypt_out)
ultimately show ?T
using F by simp
qed
next
fix evsFC5 S A U n run d e H
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsFC5) = H ∪ analz (A ∪ spies evsFC5)" and
B: "(evsFC5, S, A, U) ∈ protocol" and
C: "IntAgrK (S (Card n, n, run)) = Some d" and
D: "ExtAgrK (S (Card n, n, run)) = Some e"
let
?B = "H ∪ A ∪ spies evsFC5" and
?C = "A ∪ spies evsFC5"
show "H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (insert (Crypt (sesK (d * e)) (Passwd n)) ?B) =
H ∪ analz (insert (Crypt (sesK (d * e)) (Passwd n)) ?C)"
(is "_ ⟶ ?T")
proof (rule impI, cases "Key (invK (sesK (d * e))) ∈ analz ?C")
case True
assume "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have E: "analz ?B = H ∪ analz ?C" ..
have "Key (invK (sesK (d * e))) ∈ analz ?B"
by (rule subsetD [OF _ True], rule analz_mono, blast)
hence "analz (insert (Crypt (sesK (d * e)) (Passwd n)) ?B) =
insert (Crypt (sesK (d * e)) (Passwd n)) (insert (Passwd n) (analz ?B))"
by (simp add: analz_crypt_in analz_simp_insert_2)
moreover have "H ∪ analz (insert (Crypt (sesK (d * e)) (Passwd n)) ?C) =
insert (Crypt (sesK (d * e)) (Passwd n)) (insert (Passwd n) (H ∪ analz ?C))"
using True by (simp add: analz_crypt_in analz_simp_insert_2)
ultimately show ?T
using E by simp
next
case False
moreover assume E: "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have F: "analz ?B = H ∪ analz ?C" ..
ultimately have "Key (invK (sesK (d * e))) ∉ analz ?B"
proof (simp add: invK_sesK, insert pr_sesk_card [OF B C D])
qed (rule notI, drule subsetD [OF E], simp)
hence "analz (insert (Crypt (sesK (d * e)) (Passwd n)) ?B) =
insert (Crypt (sesK (d * e)) (Passwd n)) (analz ?B)"
by (simp add: analz_crypt_out)
moreover have "H ∪ analz (insert (Crypt (sesK (d * e)) (Passwd n)) ?C) =
insert (Crypt (sesK (d * e)) (Passwd n)) (H ∪ analz ?C)"
using False by (simp add: analz_crypt_out)
ultimately show ?T
using F by simp
qed
next
fix evsR5 S A U n run d e H
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsR5) = H ∪ analz (A ∪ spies evsR5)" and
B: "(evsR5, S, A, U) ∈ protocol" and
C: "IntAgrK (S (Card n, n, run)) = Some d" and
D: "ExtAgrK (S (Card n, n, run)) = Some e"
let
?B = "H ∪ A ∪ spies evsR5" and
?C = "A ∪ spies evsR5"
show "H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (insert (Crypt (sesK (d * e)) (Number 0)) (H ∪ A ∪ spies evsR5)) =
H ∪ analz (insert (Crypt (sesK (d * e)) (Number 0)) (A ∪ spies evsR5))"
(is "_ ⟶ ?T")
proof (rule impI, cases "Key (invK (sesK (d * e))) ∈ analz ?C")
case True
assume "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have E: "analz ?B = H ∪ analz ?C" ..
have "Key (invK (sesK (d * e))) ∈ analz ?B"
by (rule subsetD [OF _ True], rule analz_mono, blast)
hence "analz (insert (Crypt (sesK (d * e)) (Number 0)) ?B) =
insert (Crypt (sesK (d * e)) (Number 0)) (insert (Number 0) (analz ?B))"
by (simp add: analz_crypt_in analz_simp_insert_2)
moreover have "H ∪ analz (insert (Crypt (sesK (d * e)) (Number 0)) ?C) =
insert (Crypt (sesK (d * e)) (Number 0)) (insert (Number 0) (H ∪ analz ?C))"
using True by (simp add: analz_crypt_in analz_simp_insert_2)
ultimately show ?T
using E by simp
next
case False
moreover assume E: "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have F: "analz ?B = H ∪ analz ?C" ..
ultimately have "Key (invK (sesK (d * e))) ∉ analz ?B"
proof (simp add: invK_sesK, insert pr_sesk_card [OF B C D])
qed (rule notI, drule subsetD [OF E], simp)
hence "analz (insert (Crypt (sesK (d * e)) (Number 0)) ?B) =
insert (Crypt (sesK (d * e)) (Number 0)) (analz ?B)"
by (simp add: analz_crypt_out)
moreover have "H ∪ analz (insert (Crypt (sesK (d * e)) (Number 0)) ?C) =
insert (Crypt (sesK (d * e)) (Number 0)) (H ∪ analz ?C)"
using False by (simp add: analz_crypt_out)
ultimately show ?T
using F by simp
qed
next
fix evsFR5 S A U m n run c f H
assume
A: "⋀H. H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (H ∪ A ∪ spies evsFR5) = H ∪ analz (A ∪ spies evsFR5)" and
B: "(evsFR5, S, A, U) ∈ protocol" and
C: "IntAgrK (S (User m, n, run)) = Some c" and
D: "ExtAgrK (S (User m, n, run)) = Some f"
let
?B = "H ∪ A ∪ spies evsFR5" and
?C = "A ∪ spies evsFR5"
show "H ⊆ range Key ∪ range Pri_AgrK - U ⟶
analz (insert (Crypt (sesK (c * f)) (Number 0)) (H ∪ A ∪ spies evsFR5)) =
H ∪ analz (insert (Crypt (sesK (c * f)) (Number 0)) (A ∪ spies evsFR5))"
(is "_ ⟶ ?T")
proof (rule impI, cases "Key (invK (sesK (c * f))) ∈ analz ?C")
case True
assume "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have E: "analz ?B = H ∪ analz ?C" ..
have "Key (invK (sesK (c * f))) ∈ analz ?B"
by (rule subsetD [OF _ True], rule analz_mono, blast)
hence "analz (insert (Crypt (sesK (c * f)) (Number 0)) ?B) =
insert (Crypt (sesK (c * f)) (Number 0)) (insert (Number 0) (analz ?B))"
by (simp add: analz_crypt_in analz_simp_insert_2)
moreover have "H ∪ analz (insert (Crypt (sesK (c * f)) (Number 0)) ?C) =
insert (Crypt (sesK (c * f)) (Number 0)) (insert (Number 0) (H ∪ analz ?C))"
using True by (simp add: analz_crypt_in analz_simp_insert_2)
ultimately show ?T
using E by simp
next
case False
moreover assume E: "H ⊆ range Key ∪ range Pri_AgrK - U"
with A have F: "analz ?B = H ∪ analz ?C" ..
ultimately have "Key (invK (sesK (c * f))) ∉ analz ?B"
proof (simp add: invK_sesK, insert pr_sesk_user_1 [OF B C D,
THEN pr_sesk_user_2 [OF B]])
qed (rule notI, drule subsetD [OF E], simp)
hence "analz (insert (Crypt (sesK (c * f)) (Number 0)) ?B) =
insert (Crypt (sesK (c * f)) (Number 0)) (analz ?B)"
by (simp add: analz_crypt_out)
moreover have "H ∪ analz (insert (Crypt (sesK (c * f)) (Number 0)) ?C) =
insert (Crypt (sesK (c * f)) (Number 0)) (H ∪ analz ?C)"
using False by (simp add: analz_crypt_out)
ultimately show ?T
using F by simp
qed
qed
lemma pr_key_unused:
"(evs, S, A, U) ∈ protocol ⟹
Key K ∉ U ⟹
analz (insert (Key K) (A ∪ spies evs)) =
insert (Key K) (analz (A ∪ spies evs))"
by (simp only: insert_def Un_assoc [symmetric], rule pr_key_set_unused, simp_all)
lemma pr_pri_agrk_unused:
"(evs, S, A, U) ∈ protocol ⟹
Pri_AgrK x ∉ U ⟹
analz (insert (Pri_AgrK x) (A ∪ spies evs)) =
insert (Pri_AgrK x) (analz (A ∪ spies evs))"
by (simp only: insert_def Un_assoc [symmetric], rule pr_key_set_unused, simp_all)
lemma pr_pri_agrk_analz_intro [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Pri_AgrK x ∈ analz (A ∪ spies evs) ⟶
Pri_AgrK x ∈ A"
proof (erule protocol.induct, subst analz_simp, simp, blast,
simp_all add: analz_simp_insert_2 pr_key_unused pr_pri_agrk_unused,
rule conjI, rule_tac [1-2] impI, rule_tac [!] impI)
fix evsR1 S A U n s
assume
A: "Pri_AgrK x ∈ analz (A ∪ spies evsR1) ⟶ Pri_AgrK x ∈ A"
(is "_ ∈ analz ?A ⟶ _") and
B: "(evsR1, S, A, U) ∈ protocol" and
C: "n ∈ bad" and
D: "Pri_AgrK x ∈ analz (insert (Crypt (symK n) (Pri_AgrK s))
(insert (Pri_AgrK s) (A ∪ spies evsR1)))" and
E: "Pri_AgrK s ∉ U"
have "Key (symK n) ∈ analz ?A"
using B and C by (simp add: pr_symk_analz)
hence "Key (invK (symK n)) ∈ analz ?A"
by (simp add: invK_symK)
hence "Key (invK (symK n)) ∈ analz (insert (Pri_AgrK s) ?A)"
using B and E by (simp add: pr_pri_agrk_unused)
hence "Pri_AgrK x ∈ analz (insert (Pri_AgrK s) ?A)"
using D by (simp add: analz_crypt_in)
hence "x = s ∨ Pri_AgrK x ∈ analz ?A"
using B and E by (simp add: pr_pri_agrk_unused)
thus "x = s ∨ Pri_AgrK x ∈ A"
using A by blast
next
fix evsR1 S A U n s
assume
A: "Pri_AgrK x ∈ analz (A ∪ spies evsR1) ⟶ Pri_AgrK x ∈ A"
(is "_ ∈ analz ?A ⟶ _") and
B: "(evsR1, S, A, U) ∈ protocol" and
C: "n ∉ bad" and
D: "Pri_AgrK x ∈ analz (insert (Crypt (symK n) (Pri_AgrK s))
(A ∪ spies evsR1))"
have "Key (symK n) ∉ analz ?A"
using B and C by (simp add: pr_symk_analz)
hence "Key (invK (symK n)) ∉ analz ?A"
by (simp add: invK_symK)
hence "Pri_AgrK x ∈ analz ?A"
using D by (simp add: analz_crypt_out)
with A show "Pri_AgrK x ∈ A" ..
next
fix evsFR1 A m s
assume
A: "Pri_AgrK x ∈ analz (A ∪ spies evsFR1) ⟶ Pri_AgrK x ∈ A"
(is "_ ∈ analz ?A ⟶ _") and
B: "Crypt (symK m) (Pri_AgrK s) ∈ synth (analz (A ∪ spies evsFR1))" and
C: "Pri_AgrK x ∈ analz (insert (Crypt (symK m) (Pri_AgrK s))
(A ∪ spies evsFR1))"
show "Pri_AgrK x ∈ A"
proof (cases "Key (invK (symK m)) ∈ analz ?A")
case True
have "Crypt (symK m) (Pri_AgrK s) ∈ analz ?A ∨
Pri_AgrK s ∈ synth (analz ?A) ∧ Key (symK m) ∈ analz ?A"
using B by (rule synth_crypt)
moreover {
assume "Crypt (symK m) (Pri_AgrK s) ∈ analz ?A"
hence "Pri_AgrK s ∈ analz ?A"
using True by (rule analz.Decrypt)
}
moreover {
assume "Pri_AgrK s ∈ synth (analz ?A) ∧ Key (symK m) ∈ analz ?A"
hence "Pri_AgrK s ∈ synth (analz ?A)" ..
hence "Pri_AgrK s ∈ analz ?A"
by (rule synth_simp_intro, simp)
}
ultimately have "Pri_AgrK s ∈ analz ?A" ..
moreover have "Pri_AgrK x ∈ analz (insert (Pri_AgrK s) ?A)"
using C and True by (simp add: analz_crypt_in)
ultimately have "Pri_AgrK x ∈ analz ?A"
by (simp add: analz_simp_insert_1)
with A show ?thesis ..
next
case False
hence "Pri_AgrK x ∈ analz ?A"
using C by (simp add: analz_crypt_out)
with A show ?thesis ..
qed
next
fix evsC4 A c f
assume
A: "Pri_AgrK x ∈ analz (A ∪ spies evsC4) ⟶ Pri_AgrK x ∈ A"
(is "_ ∈ analz ?A ⟶ _") and
B: "Pri_AgrK x ∈ analz (insert (Crypt (sesK (c * f)) (pubAK f))
(A ∪ spies evsC4))"
show "Pri_AgrK x ∈ A"
proof (cases "Key (invK (sesK (c * f))) ∈ analz ?A")
case True
hence "Pri_AgrK x ∈ analz ?A"
using B by (simp add: analz_crypt_in analz_simp_insert_2)
with A show ?thesis ..
next
case False
hence "Pri_AgrK x ∈ analz ?A"
using B by (simp add: analz_crypt_out)
with A show ?thesis ..
qed
next
fix evsFC4 A s a b d e
assume
A: "Pri_AgrK x ∈ analz (A ∪ spies evsFC4) ⟶ Pri_AgrK x ∈ A"
(is "_ ∈ analz ?A ⟶ _") and
B: "Pri_AgrK x ∈ analz (insert (Crypt (sesK (d * e)) (pubAK (d * (s + a * b))))
(A ∪ spies evsFC4))"
show "Pri_AgrK x ∈ A"
proof (cases "Key (invK (sesK (d * e))) ∈ analz ?A")
case True
hence "Pri_AgrK x ∈ analz ?A"
using B by (simp add: analz_crypt_in analz_simp_insert_2)
with A show ?thesis ..
next
case False
hence "Pri_AgrK x ∈ analz ?A"
using B by (simp add: analz_crypt_out)
with A show ?thesis ..
qed
next
fix evsR4 S A U n run b d e
let
?H = "Hash (pubAK (priAK n))" and
?M = "⦃pubAK (priAK n), Crypt (priSK CA) (Hash (pubAK (priAK n)))⦄" and
?M' = "⦃pubAK e, Auth_Data (priAK n) b, pubAK (priAK n),
Crypt (priSK CA) (Hash (pubAK (priAK n)))⦄"
assume
A: "Pri_AgrK x ∈ analz (A ∪ spies evsR4) ⟶ Pri_AgrK x ∈ A"
(is "_ ∈ analz ?A ⟶ _") and
B: "(evsR4, S, A, U) ∈ protocol" and
C: "IntMapK (S (Card n, n, run)) = Some b" and
D: "Pri_AgrK x ∈ analz (insert (Crypt (sesK (d * e)) ?M')
(A ∪ spies evsR4))"
show "Pri_AgrK x ∈ A"
proof (cases "Key (invK (sesK (d * e))) ∈ analz ?A")
case True
have "Key (pubSK CA) ∈ analz ?A"
using B by (rule pr_valid_key_analz)
hence E: "analz (insert (Crypt (priSK CA) ?H) ?A) =
{Crypt (priSK CA) ?H, ?H} ∪ analz ?A"
by (simp add: analz_crypt_in analz_simp_insert_2)
have "Pri_AgrK (priAK n) ∉ analz ?A"
using B by (rule pr_auth_key_analz)
hence F: "Pri_AgrK (priAK n) ∉ analz (insert (Crypt (priSK CA) ?H) ?A)"
using E by simp
have "Pri_AgrK b ∉ analz ?A"
using B and C by (rule pr_int_mapk_analz)
hence G: "Pri_AgrK b ∉ analz (insert (Crypt (priSK CA) ?H) ?A)"
using E by simp
have "Pri_AgrK x ∈ analz (insert ?M' ?A)"
using D and True by (simp add: analz_crypt_in)
hence "Pri_AgrK x ∈ analz (insert (Auth_Data (priAK n) b) (insert ?M ?A))"
by (simp add: analz_mpair analz_simp_insert_2)
hence "Pri_AgrK x ∈ analz ?A"
proof (subst (asm) insert_commute, simp add: analz_mpair analz_simp_insert_2
del: Un_insert_right, subst (asm) insert_commute,
subst (asm) analz_auth_data_out [OF F G])
qed (simp add: E)
with A show ?thesis ..
next
case False
hence "Pri_AgrK x ∈ analz ?A"
using D by (simp add: analz_crypt_out)
with A show ?thesis ..
qed
next
fix evsFR4 S A U m n run s a b c f g
let
?H = "Hash (pubAK g)" and
?M = "⦃pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄" and
?M' = "⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄"
assume
A: "Pri_AgrK x ∈ analz (A ∪ spies evsFR4) ⟶ Pri_AgrK x ∈ A"
(is "_ ∈ analz ?A ⟶ _") and
B: "(evsFR4, S, A, U) ∈ protocol" and
C: "Crypt (sesK (c * f)) ?M' ∈ synth (analz (A ∪ spies evsFR4))" and
D: "Pri_AgrK x ∈ analz (insert (Crypt (sesK (c * f)) ?M')
(A ∪ spies evsFR4))"
have E:
"Key (invK (sesK (c * f))) ∈ analz ?A ⟶
Pri_AgrK b ∈ analz ?A ∨ Pri_AgrK g ∈ analz ?A ⟶
Pri_AgrK b ∈ analz ?A ∧ Pri_AgrK g ∈ analz ?A"
(is "?P ⟶ ?Q ⟶ ?R")
proof (rule impI)+
assume ?P and ?Q
have "Crypt (sesK (c * f)) ?M' ∈ analz ?A ∨
?M' ∈ synth (analz ?A) ∧ Key (sesK (c * f)) ∈ analz ?A"
using C by (rule synth_crypt)
moreover {
assume "Crypt (sesK (c * f)) ?M' ∈ analz ?A"
hence "?M' ∈ analz ?A"
using ‹?P› by (rule analz.Decrypt)
hence "⦃Auth_Data g b, pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ analz ?A"
by (rule analz.Snd)
hence F: "Auth_Data g b ∈ analz ?A"
by (rule analz.Fst)
have ?R
proof (rule disjE [OF ‹?Q›])
assume "Pri_AgrK b ∈ analz ?A"
moreover from this have "Pri_AgrK g ∈ analz ?A"
by (rule analz.Auth_Fst [OF F])
ultimately show ?R ..
next
assume "Pri_AgrK g ∈ analz ?A"
moreover from this have "Pri_AgrK b ∈ analz ?A"
by (rule analz.Auth_Snd [OF F])
ultimately show ?R
by simp
qed
}
moreover {
assume "?M' ∈ synth (analz ?A) ∧ Key (sesK (c * f)) ∈ analz ?A"
hence "?M' ∈ synth (analz ?A)" ..
hence "⦃Auth_Data g b, pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ synth (analz ?A)"
by (rule synth_analz_snd)
hence "Auth_Data g b ∈ synth (analz ?A)"
by (rule synth_analz_fst)
hence "Auth_Data g b ∈ analz ?A ∨
Pri_AgrK g ∈ analz ?A ∧ Pri_AgrK b ∈ analz ?A"
by (rule synth_auth_data)
moreover {
assume F: "Auth_Data g b ∈ analz ?A"
have ?R
proof (rule disjE [OF ‹?Q›])
assume "Pri_AgrK b ∈ analz ?A"
moreover from this have "Pri_AgrK g ∈ analz ?A"
by (rule analz.Auth_Fst [OF F])
ultimately show ?R ..
next
assume "Pri_AgrK g ∈ analz ?A"
moreover from this have "Pri_AgrK b ∈ analz ?A"
by (rule analz.Auth_Snd [OF F])
ultimately show ?R
by simp
qed
}
moreover {
assume "Pri_AgrK g ∈ analz ?A ∧ Pri_AgrK b ∈ analz ?A"
hence ?R
by simp
}
ultimately have ?R ..
}
ultimately show ?R ..
qed
show "Pri_AgrK x ∈ A"
proof (cases "Key (invK (sesK (c * f))) ∈ analz ?A")
case True
have "Key (pubSK CA) ∈ analz ?A"
using B by (rule pr_valid_key_analz)
hence F: "analz (insert (Crypt (priSK CA) ?H) ?A) =
{Crypt (priSK CA) ?H, ?H} ∪ analz ?A"
by (simp add: analz_crypt_in analz_simp_insert_2)
show ?thesis
proof (cases "Pri_AgrK g ∈ analz ?A ∨ Pri_AgrK b ∈ analz ?A", simp_all)
assume G: "Pri_AgrK g ∈ analz ?A ∨ Pri_AgrK b ∈ analz ?A"
hence H: "Pri_AgrK g ∈ analz (insert (Crypt (priSK CA) ?H) ?A) ∨
Pri_AgrK b ∈ analz (insert (Crypt (priSK CA) ?H) ?A)"
using F by simp
have I: "Pri_AgrK b ∈ analz ?A ∧ Pri_AgrK g ∈ analz ?A"
using E and G and True by blast
hence "Pri_AgrK g ∈ analz (insert (Crypt (priSK CA) ?H) ?A)"
using F by simp
hence J: "Pri_AgrK g ∈ analz (insert (Pri_AgrK b)
(insert (Crypt (priSK CA) ?H) ?A))"
by (rule rev_subsetD, rule_tac analz_mono, blast)
have K: "Pri_AgrK b ∈ analz (insert (Crypt (priSK CA) ?H) ?A)"
using F and I by simp
have "Pri_AgrK x ∈ analz (insert ?M' ?A)"
using D and True by (simp add: analz_crypt_in)
hence "Pri_AgrK x ∈ analz (insert (Auth_Data g b) (insert ?M ?A))"
by (simp add: analz_mpair analz_simp_insert_2)
hence "Pri_AgrK x ∈ analz ?A"
proof (subst (asm) insert_commute, simp add: analz_mpair analz_simp_insert_2
del: Un_insert_right, subst (asm) insert_commute,
subst (asm) analz_auth_data_in [OF H], simp del: Un_insert_right)
assume "Pri_AgrK x ∈ analz (insert (Pri_AgrK g) (insert (Pri_AgrK b)
(insert (Crypt (priSK CA) ?H) ?A)))"
thus ?thesis
proof (subst (asm) analz_simp_insert_1 [OF J],
subst (asm) analz_simp_insert_1 [OF K])
qed (simp add: F)
qed
with A show ?thesis ..
next
assume G: "Pri_AgrK g ∉ analz ?A ∧ Pri_AgrK b ∉ analz ?A"
hence H: "Pri_AgrK g ∉ analz (insert (Crypt (priSK CA) ?H) ?A)"
using F by simp
have I: "Pri_AgrK b ∉ analz (insert (Crypt (priSK CA) ?H) ?A)"
using F and G by simp
have "Pri_AgrK x ∈ analz (insert ?M' ?A)"
using D and True by (simp add: analz_crypt_in)
hence "Pri_AgrK x ∈ analz (insert (Auth_Data g b) (insert ?M ?A))"
by (simp add: analz_mpair analz_simp_insert_2)
hence "Pri_AgrK x ∈ analz ?A"
proof (subst (asm) insert_commute, simp add: analz_mpair analz_simp_insert_2
del: Un_insert_right, subst (asm) insert_commute,
subst (asm) analz_auth_data_out [OF H I])
qed (simp add: F)
with A show ?thesis ..
qed
next
case False
hence "Pri_AgrK x ∈ analz ?A"
using D by (simp add: analz_crypt_out)
with A show ?thesis ..
qed
next
fix evsC5 A m c f
assume
A: "Pri_AgrK x ∈ analz (A ∪ spies evsC5) ⟶ Pri_AgrK x ∈ A"
(is "_ ∈ analz ?A ⟶ _") and
B: "Pri_AgrK x ∈ analz (insert (Crypt (sesK (c * f)) (Passwd m))
(A ∪ spies evsC5))"
show "Pri_AgrK x ∈ A"
proof (cases "Key (invK (sesK (c * f))) ∈ analz ?A")
case True
hence "Pri_AgrK x ∈ analz ?A"
using B by (simp add: analz_crypt_in analz_simp_insert_2)
with A show ?thesis ..
next
case False
hence "Pri_AgrK x ∈ analz ?A"
using B by (simp add: analz_crypt_out)
with A show ?thesis ..
qed
next
fix evsFC5 A n d e
assume
A: "Pri_AgrK x ∈ analz (A ∪ spies evsFC5) ⟶ Pri_AgrK x ∈ A"
(is "_ ∈ analz ?A ⟶ _") and
B: "Pri_AgrK x ∈ analz (insert (Crypt (sesK (d * e)) (Passwd n))
(A ∪ spies evsFC5))"
show "Pri_AgrK x ∈ A"
proof (cases "Key (invK (sesK (d * e))) ∈ analz ?A")
case True
hence "Pri_AgrK x ∈ analz ?A"
using B by (simp add: analz_crypt_in analz_simp_insert_2)
with A show ?thesis ..
next
case False
hence "Pri_AgrK x ∈ analz ?A"
using B by (simp add: analz_crypt_out)
with A show ?thesis ..
qed
next
fix evsR5 A d e
assume
A: "Pri_AgrK x ∈ analz (A ∪ spies evsR5) ⟶ Pri_AgrK x ∈ A"
(is "_ ∈ analz ?A ⟶ _") and
B: "Pri_AgrK x ∈ analz (insert (Crypt (sesK (d * e)) (Number 0))
(A ∪ spies evsR5))"
show "Pri_AgrK x ∈ A"
proof (cases "Key (invK (sesK (d * e))) ∈ analz ?A")
case True
hence "Pri_AgrK x ∈ analz ?A"
using B by (simp add: analz_crypt_in analz_simp_insert_2)
with A show ?thesis ..
next
case False
hence "Pri_AgrK x ∈ analz ?A"
using B by (simp add: analz_crypt_out)
with A show ?thesis ..
qed
next
fix evsFR5 A c f
assume
A: "Pri_AgrK x ∈ analz (A ∪ spies evsFR5) ⟶ Pri_AgrK x ∈ A"
(is "_ ∈ analz ?A ⟶ _") and
B: "Pri_AgrK x ∈ analz (insert (Crypt (sesK (c * f)) (Number 0))
(A ∪ spies evsFR5))"
show "Pri_AgrK x ∈ A"
proof (cases "Key (invK (sesK (c * f))) ∈ analz ?A")
case True
hence "Pri_AgrK x ∈ analz ?A"
using B by (simp add: analz_crypt_in analz_simp_insert_2)
with A show ?thesis ..
next
case False
hence "Pri_AgrK x ∈ analz ?A"
using B by (simp add: analz_crypt_out)
with A show ?thesis ..
qed
qed
lemma pr_pri_agrk_analz:
"(evs, S, A, U) ∈ protocol ⟹
(Pri_AgrK x ∈ analz (A ∪ spies evs)) = (Pri_AgrK x ∈ A)"
proof (rule iffI, erule pr_pri_agrk_analz_intro, assumption)
qed (rule subsetD [OF analz_subset], simp)
lemma pr_ext_agrk_user_1 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
User m ≠ Spy ⟶
Says n run 4 (User m) (Card n) (Crypt (sesK K) (pubAK e)) ∈ set evs ⟶
ExtAgrK (S (User m, n, run)) ≠ None"
by (erule protocol.induct, simp_all, (rule_tac [!] impI)+, simp_all)
lemma pr_ext_agrk_user_2 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
User m ≠ Spy ⟶
Says n run 4 X (User m) (Crypt (sesK K)
⦃pubAK e, Auth_Data x y, pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄)
∈ set evs ⟶
ExtAgrK (S (User m, n, run)) ≠ None"
using [[simproc del: defined_all]] proof (erule protocol.induct, simp_all, (rule_tac [!] impI)+, simp_all,
(erule conjE)+)
fix evs S A U n run s a b d e X
assume "(evs, S, A, U) ∈ protocol"
moreover assume "0 < m"
hence "User m ≠ Spy"
by simp
moreover assume A: "User m = X" and
"Says n run 4 X (Card n) (Crypt (sesK (d * e))
(pubAK (d * (s + a * b)))) ∈ set evs"
hence "Says n run 4 (User m) (Card n) (Crypt (sesK (d * e))
(pubAK (d * (s + a * b)))) ∈ set evs"
by simp
ultimately have "ExtAgrK (S (User m, n, run)) ≠ None"
by (rule pr_ext_agrk_user_1)
thus "∃e. ExtAgrK (S (X, n, run)) = Some e"
using A by simp
qed
lemma pr_ext_agrk_user_3 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
User m ≠ Spy ⟶
ExtAgrK (S (User m, n, run)) = Some e ⟶
Says n run 4 (User m) (Card n) (Crypt (sesK K) (pubAK e')) ∈ set evs ⟶
e' = e"
proof (erule protocol.induct, simp_all, (rule conjI, (rule_tac [!] impI)+)+,
(erule conjE)+, simp_all)
assume "agrK e' = agrK e"
with agrK_inj show "e' = e"
by (rule injD)
next
fix evsC4 S A U n run and m :: nat
assume "(evsC4, S, A, U) ∈ protocol"
moreover assume "0 < m"
hence "User m ≠ Spy"
by simp
moreover assume
"Says n run 4 (User m) (Card n) (Crypt (sesK K) (pubAK e')) ∈ set evsC4"
ultimately have "ExtAgrK (S (User m, n, run)) ≠ None"
by (rule pr_ext_agrk_user_1)
moreover assume "ExtAgrK (S (User m, n, run)) = None"
ultimately show "e' = e"
by contradiction
qed
lemma pr_ext_agrk_user_4 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
ExtAgrK (S (User m, n, run)) = Some f ⟶
(∃X. Says n run 3 X (User m) (pubAK f) ∈ set evs)"
proof (erule protocol.induct, simp_all, rule_tac [!] impI, rule_tac [1-2] impI,
rule_tac [5] impI, simp_all)
qed blast+
declare fun_upd_apply [simp del]
lemma pr_ext_agrk_user_5 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Says n run 3 X (User m) (pubAK f) ∈ set evs ⟶
(∃s a b d. f = d * (s + a * b) ∧
NonceS (S (Card n, n, run)) = Some s ∧
IntMapK (S (Card n, n, run)) = Some b ∧
ExtMapK (S (Card n, n, run)) = Some a ∧
IntAgrK (S (Card n, n, run)) = Some d ∧
d ≠ 0 ∧ s + a * b ≠ 0) ∨
(∃b. Pri_AgrK b ∈ A ∧
ExtMapK (S (User m, n, run)) = Some b)"
(is "_ ⟹ ?H evs ⟶ ?P S n run ∨ ?Q S A n run")
apply (erule protocol.induct, simp_all add: pr_pri_agrk_analz)
apply (rule conjI)
apply (rule_tac [1-2] impI)+
apply (rule_tac [3] conjI, (rule_tac [3] impI)+)+
apply (rule_tac [4] impI)+
apply ((rule_tac [5] impI)+, (rule_tac [5] conjI)?)+
apply (rule_tac [6] impI)+
apply ((rule_tac [7] impI)+, (rule_tac [7] conjI)?)+
apply (rule_tac [8] impI)+
apply ((rule_tac [9] impI)+, (rule_tac [9] conjI)?)+
apply (rule_tac [10] impI)+
apply (rule_tac [11] impI)+
apply (rule_tac [12] conjI, (rule_tac [12] impI)+)+
apply (rule_tac [13] impI)+
apply (rule_tac [14] conjI, (rule_tac [14] impI)+)+
apply (erule_tac [14] conjE)+
apply (rule_tac [15] impI)+
apply ((rule_tac [16] impI)+, (rule_tac [16] conjI)?)+
apply (erule_tac [16] conjE)+
apply (rule_tac [17-18] impI)
proof -
fix evsR1 S A U s n' run'
assume
"?H evsR1 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsR1"
hence A: "?P S n run ∨ ?Q S A n run" ..
assume B: "NonceS (S (Card n', n', run')) = None"
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇NonceS := Some s⦈)"
show "?P ?S n run ∨
(∃b. (b = s ∨ Pri_AgrK b ∈ A) ∧ ExtMapK (?S (User m, n, run)) = Some b)"
proof (rule disjE [OF A], rule disjI1, simp add: fun_upd_apply, rule impI, simp add: B)
qed (rule disjI2, simp add: fun_upd_apply, blast)
next
fix evsR1 S A U s n' run'
assume
"?H evsR1 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsR1"
hence A: "?P S n run ∨ ?Q S A n run" ..
assume B: "NonceS (S (Card n', n', run')) = None"
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇NonceS := Some s⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
proof (rule disjE [OF A], rule disjI1, simp add: fun_upd_apply, rule impI, simp add: B)
qed (rule disjI2, simp add: fun_upd_apply)
next
fix evsC2 S A U s a n' run'
assume
"?H evsC2 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsC2"
hence A: "?P S n run ∨ ?Q S A n run" ..
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨
(∃b. (b = a ∨ Pri_AgrK b ∈ A) ∧ ExtMapK (?S (User m, n, run)) = Some b)"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a m' n' run'
assume
"?H evsC2 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsC2"
hence A: "?P S n run ∨ ?Q S A n run" ..
let ?S = "S((User m', n', run') := S (User m', n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a n' run'
assume
"?H evsC2 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsC2"
hence A: "?P S n run ∨ ?Q S A n run" ..
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨
(∃b. (b = a ∨ Pri_AgrK b ∈ A) ∧ ExtMapK (?S (User m, n, run)) = Some b)"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a m' n' run'
assume
"?H evsC2 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsC2"
hence A: "?P S n run ∨ ?Q S A n run" ..
let ?S = "S((User m', n', run') := S (User m', n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a n' run'
assume
"?H evsC2 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsC2"
hence A: "?P S n run ∨ ?Q S A n run" ..
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨
(∃b. (b = a ∨ Pri_AgrK b ∈ A) ∧ ExtMapK (?S (User m, n, run)) = Some b)"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a m' n' run'
assume
"?H evsC2 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsC2"
hence A: "?P S n run ∨ ?Q S A n run" ..
let ?S = "S((User m', n', run') := S (User m', n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a n' run'
assume
"?H evsC2 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsC2"
hence A: "?P S n run ∨ ?Q S A n run" ..
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨
(∃b. (b = a ∨ Pri_AgrK b ∈ A) ∧ ExtMapK (?S (User m, n, run)) = Some b)"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a m' n' run'
assume
"?H evsC2 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsC2"
hence A: "?P S n run ∨ ?Q S A n run" ..
let ?S = "S((User m', n', run') := S (User m', n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsR2 S A U a b n' run'
assume
"?H evsR2 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsR2"
hence A: "?P S n run ∨ ?Q S A n run" ..
assume B: "IntMapK (S (Card n', n', run')) = None"
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntMapK := Some b, ExtMapK := Some a⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
proof (rule disjE [OF A], rule disjI1, simp add: fun_upd_apply, rule impI, simp add: B)
qed (rule disjI2, simp add: fun_upd_apply)
next
fix evsC3 S A U b c m' n' run'
assume
"?H evsC3 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsC3"
hence A: "?P S n run ∨ ?Q S A n run" ..
assume
"ExtMapK (S (User m', n', run')) = None" and
"m' = 0"
hence B: "ExtMapK (S (Spy, n', run')) = None"
by simp
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇ExtMapK := Some b, IntAgrK := Some c⦈)"
show "?P ?S n run ∨
(∃b. (b = c ∨ Pri_AgrK b ∈ A) ∧ ExtMapK (?S (User m, n, run)) = Some b)"
proof (rule disjE [OF A], simp add: fun_upd_apply)
qed (rule disjI2, simp add: fun_upd_apply, rule conjI, rule impI, simp add: B, blast)
next
fix evsC3 S A U b c m' n' run'
assume
"?H evsC3 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsC3"
hence A: "?P S n run ∨ ?Q S A n run" ..
assume B: "ExtMapK (S (User m', n', run')) = None"
let ?S = "S((User m', n', run') := S (User m', n', run')
⦇ExtMapK := Some b, IntAgrK := Some c⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
proof (rule disjE [OF A], simp add: fun_upd_apply)
qed (rule disjI2, simp add: fun_upd_apply, rule impI, simp add: B)
next
fix evsR3 A U s a b c d n' run' X and S :: state
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntAgrK := Some d, ExtAgrK := Some (c * (s + a * b))⦈)"
assume "agrK f = agrK (d * (s + a * b))"
with agrK_inj have "f = d * (s + a * b)"
by (rule injD)
moreover assume
"NonceS (S (Card n', n', run')) = Some s" and
"IntMapK (S (Card n', n', run')) = Some b" and
"ExtMapK (S (Card n', n', run')) = Some a" and
"d ≠ 0" and
"s + a * b ≠ 0"
ultimately show "?P ?S n' run' ∨
(∃b. Pri_AgrK b ∈ A ∧ ExtMapK (?S (X, n', run')) = Some b)"
by (simp add: fun_upd_apply)
next
fix evsR3 S A U s a b c d n' run'
assume
"?H evsR3 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsR3"
hence A: "?P S n run ∨ ?Q S A n run" ..
assume B: "IntAgrK (S (Card n', n', run')) = None"
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntAgrK := Some d, ExtAgrK := Some (c * (s + a * b))⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
proof (rule disjE [OF A], rule disjI1, simp add: fun_upd_apply, rule impI, simp add: B)
qed (rule disjI2, simp add: fun_upd_apply)
next
fix evsR3 A U s s' a b c d n' run' X and S :: state
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntAgrK := Some d, ExtAgrK := Some (c * (s' + a * b))⦈)"
assume "agrK f = agrK (d * (s + a * b))"
with agrK_inj have "f = d * (s + a * b)"
by (rule injD)
moreover assume
"NonceS (S (Card n', n', run')) = Some s" and
"IntMapK (S (Card n', n', run')) = Some b" and
"ExtMapK (S (Card n', n', run')) = Some a" and
"d ≠ 0" and
"s + a * b ≠ 0"
ultimately show "?P ?S n' run' ∨
(∃b. Pri_AgrK b ∈ A ∧ ExtMapK (?S (X, n', run')) = Some b)"
by (simp add: fun_upd_apply)
next
fix evsR3 S A U s a b c d n' run'
assume
"?H evsR3 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsR3"
hence A: "?P S n run ∨ ?Q S A n run" ..
assume B: "IntAgrK (S (Card n', n', run')) = None"
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntAgrK := Some d, ExtAgrK := Some (c * (s + a * b))⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
proof (rule disjE [OF A], rule disjI1, simp add: fun_upd_apply, rule impI, simp add: B)
qed (rule disjI2, simp add: fun_upd_apply)
next
fix evsC4 S A U f m' n' run'
assume
"?H evsC4 ⟶ ?P S n run ∨ ?Q S A n run" and
"?H evsC4"
hence A: "?P S n run ∨ ?Q S A n run" ..
let ?S = "S((User m', n', run') := S (User m', n', run')
⦇ExtAgrK := Some f⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
qed
declare fun_upd_apply [simp]
lemma pr_int_agrk_user_1 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
IntAgrK (S (User m, n, run)) = Some c ⟶
Pri_AgrK c ∈ U"
by (erule protocol.induct, simp_all)
lemma pr_int_agrk_user_2 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
User m ≠ Spy ⟶
IntAgrK (S (User m, n, run)) = Some c ⟶
Pri_AgrK c ∉ A"
proof (erule protocol.induct, simp_all, rule_tac [3] conjI, (rule_tac [!] impI)+,
rule_tac [2] impI, rule_tac [4] impI, rule_tac [!] notI, simp_all)
fix evsR1 S A U s
assume
"(evsR1, S, A, U) ∈ protocol" and
"IntAgrK (S (User m, n, run)) = Some s"
hence "Pri_AgrK s ∈ U"
by (rule pr_int_agrk_user_1)
moreover assume "Pri_AgrK s ∉ U"
ultimately show False
by contradiction
next
fix evsC2 S A U a
assume
"(evsC2, S, A, U) ∈ protocol" and
"IntAgrK (S (User m, n, run)) = Some a"
hence "Pri_AgrK a ∈ U"
by (rule pr_int_agrk_user_1)
moreover assume "Pri_AgrK a ∉ U"
ultimately show False
by contradiction
next
fix evsC3 S A U
assume "(evsC3, S, A, U) ∈ protocol"
hence "A ⊆ U"
by (rule pr_analz_used)
moreover assume "Pri_AgrK c ∈ A"
ultimately have "Pri_AgrK c ∈ U" ..
moreover assume "Pri_AgrK c ∉ U"
ultimately show False
by contradiction
next
fix evsC3 S A U c'
assume
"(evsC3, S, A, U) ∈ protocol" and
"IntAgrK (S (User m, n, run)) = Some c'"
hence "Pri_AgrK c' ∈ U"
by (rule pr_int_agrk_user_1)
moreover assume "Pri_AgrK c' ∉ U"
ultimately show False
by contradiction
qed
lemma pr_int_agrk_user_3 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
NonceS (S (User m, n, run)) = Some s ⟶
IntMapK (S (User m, n, run)) = Some a ⟶
ExtMapK (S (User m, n, run)) = Some b ⟶
IntAgrK (S (User m, n, run)) = Some c ⟶
c * (s + a * b) ≠ 0"
proof (erule protocol.induct, simp_all, rule conjI, (rule_tac [1-2] impI)+,
(rule_tac [3] impI)+, simp_all)
fix evsC2 S A U n run m
assume A: "(evsC2, S, A, U) ∈ protocol"
moreover assume "NonceS (S (User m, n, run)) = None"
ultimately have "IntMapK (S (User m, n, run)) = None"
by (rule pr_state_1)
with A have "ExtMapK (S (User m, n, run)) = None"
by (rule pr_state_2)
moreover assume "ExtMapK (S (User m, n, run)) = Some b"
ultimately show "c ≠ 0 ∧ s + a * b ≠ 0"
by simp
next
fix evsC2 S A U n run m
assume A: "(evsC2, S, A, U) ∈ protocol"
moreover assume "NonceS (S (User m, n, run)) = None"
ultimately have "IntMapK (S (User m, n, run)) = None"
by (rule pr_state_1)
with A have "ExtMapK (S (User m, n, run)) = None"
by (rule pr_state_2)
moreover assume "ExtMapK (S (User m, n, run)) = Some b"
ultimately show "c ≠ 0 ∧ a ≠ 0 ∧ b ≠ 0"
by simp
qed
lemma pr_int_agrk_card [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
NonceS (S (Card n, n, run)) = Some s ⟶
IntMapK (S (Card n, n, run)) = Some b ⟶
ExtMapK (S (Card n, n, run)) = Some a ⟶
IntAgrK (S (Card n, n, run)) = Some d ⟶
d * (s + a * b) ≠ 0"
proof (erule protocol.induct, simp_all, (rule_tac [!] impI)+, simp_all)
fix evsR1 S A U n run
assume
"(evsR1, S, A, U) ∈ protocol" and
"NonceS (S (Card n, n, run)) = None"
hence "IntMapK (S (Card n, n, run)) = None"
by (rule pr_state_1)
moreover assume "IntMapK (S (Card n, n, run)) = Some b"
ultimately show "d ≠ 0 ∧ s + a * b ≠ 0"
by simp
next
fix evsR2 S A U n run
assume A: "(evsR2, S, A, U) ∈ protocol" and
"IntMapK (S (Card n, n, run)) = None"
hence "ExtMapK (S (Card n, n, run)) = None"
by (rule pr_state_2)
with A have "IntAgrK (S (Card n, n, run)) = None"
by (rule pr_state_3)
moreover assume "IntAgrK (S (Card n, n, run)) = Some d"
ultimately show "d ≠ 0 ∧ s + a * b ≠ 0"
by simp
qed
lemma pr_ext_agrk_card [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
NonceS (S (Card n, n, run)) = Some s ⟶
IntMapK (S (Card n, n, run)) = Some b ⟶
ExtMapK (S (Card n, n, run)) = Some a ⟶
IntAgrK (S (Card n, n, run)) = Some d ⟶
ExtAgrK (S (Card n, n, run)) = Some (c * (s + a * b)) ⟶
Pri_AgrK c ∉ A ⟶
Key (sesK (c * d * (s + a * b))) ∉ A"
apply (erule protocol.induct, simp_all add: pr_pri_agrk_analz)
apply (rule conjI)
apply (rule_tac [1-2] impI)+
apply (rule_tac [3] impI)+
apply (rule_tac [4] conjI, (rule_tac [4] impI)+)+
apply (erule_tac [4] conjE)+
apply (rule_tac [5] impI)
apply (erule_tac [5] conjE)+
apply (rule_tac [6] impI)+
apply (erule_tac [6] conjE)+
apply (rule_tac [6] notI)
apply ((rule_tac [7] impI)+, (rule_tac [7] conjI)?)+
apply (erule_tac [7] conjE)+
apply (rule_tac [8] impI)
apply (erule_tac [8] conjE)+
apply (rule_tac [9] impI)+
apply (rule_tac [9] notI)
apply (rule_tac [10] impI)+
apply (rule_tac [11] impI)+
apply (rule_tac [11] notI)
proof simp_all
fix evsR1 S A U n run
assume
"(evsR1, S, A, U) ∈ protocol" and
"NonceS (S (Card n, n, run)) = None"
hence "IntMapK (S (Card n, n, run)) = None"
by (rule pr_state_1)
moreover assume "IntMapK (S (Card n, n, run)) = Some b"
ultimately show "Key (sesK (c * d * (s + a * b))) ∉ A"
by simp
next
fix evsR1 S A U n run
assume
"(evsR1, S, A, U) ∈ protocol" and
"NonceS (S (Card n, n, run)) = None"
hence "IntMapK (S (Card n, n, run)) = None"
by (rule pr_state_1)
moreover assume "IntMapK (S (Card n, n, run)) = Some b"
ultimately show "Key (sesK (c * d * (s + a * b))) ∉ A"
by simp
next
fix evsR2 S A U n run
assume A: "(evsR2, S, A, U) ∈ protocol" and
"IntMapK (S (Card n, n, run)) = None"
hence "ExtMapK (S (Card n, n, run)) = None"
by (rule pr_state_2)
with A have "IntAgrK (S (Card n, n, run)) = None"
by (rule pr_state_3)
moreover assume "IntAgrK (S (Card n, n, run)) = Some d"
ultimately show "Key (sesK (c * d * (s + a * b))) ∉ A"
by simp
next
fix evsR3 S A U s a' b' c' d'
assume
"(evsR3, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some (c * (s + a * b))"
hence "Key (sesK (d * (c * (s + a * b)))) ∈ U"
by (rule pr_sesk_card)
moreover have "d * (c * (s + a * b)) = c * d * (s + a * b)"
by simp
ultimately have "Key (sesK (c * d * (s + a * b))) ∈ U"
by simp
moreover assume "sesK (c * d * (s + a * b)) = sesK (c' * d' * (s + a' * b'))"
ultimately have "Key (sesK (c' * d' * (s + a' * b'))) ∈ U"
by simp
moreover assume "Key (sesK (c' * d' * (s + a' * b'))) ∉ U"
ultimately show False
by contradiction
next
fix evsR3 S A U s' a' b' c' d'
assume
"(evsR3, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some (c * (s + a * b))"
hence "Key (sesK (d * (c * (s + a * b)))) ∈ U"
by (rule pr_sesk_card)
moreover have "d * (c * (s + a * b)) = c * d * (s + a * b)"
by simp
ultimately have "Key (sesK (c * d * (s + a * b))) ∈ U"
by simp
moreover assume "sesK (c * d * (s + a * b)) = sesK (c' * d' * (s' + a' * b'))"
ultimately have "Key (sesK (c' * d' * (s' + a' * b'))) ∈ U"
by simp
moreover assume "Key (sesK (c' * d' * (s' + a' * b'))) ∉ U"
ultimately show False
by contradiction
next
fix evsR3 S A U s' c'
assume "(evsR3, S, A, U) ∈ protocol"
hence "A ⊆ U"
by (rule pr_analz_used)
moreover assume "Key (sesK (c' * d * (s' + a * b))) ∉ U"
ultimately have "Key (sesK (c' * d * (s' + a * b))) ∉ A"
by (rule contra_subsetD)
moreover assume "c' * (s' + a * b) = c * (s + a * b)"
hence "c' * d * (s' + a * b) = c * d * (s + a * b)"
by simp
ultimately show "Key (sesK (c * d * (s + a * b))) ∉ A"
by simp
next
fix evsFR3 S A U s' a' b' c' d'
assume
"(evsFR3, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some (c * (s + a * b))"
hence "Key (sesK (d * (c * (s + a * b)))) ∈ U"
by (rule pr_sesk_card)
moreover have "d * (c * (s + a * b)) = c * d * (s + a * b)"
by simp
ultimately have "Key (sesK (c * d * (s + a * b))) ∈ U"
by simp
moreover assume "sesK (c * d * (s + a * b)) = sesK (c' * d' * (s' + a' * b'))"
ultimately have "Key (sesK (c' * d' * (s' + a' * b'))) ∈ U"
by simp
moreover assume "Key (sesK (c' * d' * (s' + a' * b'))) ∉ U"
ultimately show False
by contradiction
qed
declare fun_upd_apply [simp del]
lemma pr_sesk_user_3 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
⦃Key (sesK K), Agent (User m), Number n, Number run⦄ ∈ U ⟶
Key (sesK K) ∈ A ⟶
(∃d e. K = d * e ∧
IntAgrK (S (Card n, n, run)) = Some d ∧
ExtAgrK (S (Card n, n, run)) = Some e) ∨
(∃b. Pri_AgrK b ∈ A ∧
ExtMapK (S (User m, n, run)) = Some b)"
(is "_ ⟹ ?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run")
apply (erule protocol.induct, simp_all add: pr_pri_agrk_analz, blast)
apply (rule conjI)
apply (rule_tac [1-2] impI)+
apply (rule_tac [3] conjI, (rule_tac [3] impI)+)+
apply (rule_tac [4] impI)+
apply ((rule_tac [5] impI)+, (rule_tac [5] conjI)?)+
apply (rule_tac [6] impI)+
apply ((rule_tac [7] impI)+, (rule_tac [7] conjI)?)+
apply (rule_tac [8] impI)+
apply ((rule_tac [9] impI)+, (rule_tac [9] conjI)?)+
apply (rule_tac [10] impI)+
apply (rule_tac [11] impI)+
apply (rule_tac [12] conjI, (rule_tac [12] impI)+)+
apply (rule_tac [13] impI)+
apply (rule_tac [14] conjI, (rule_tac [14] impI)+)+
apply (erule_tac [14] conjE)+
apply ((rule_tac [15] impI)+, (rule_tac [15] conjI)?)+
apply (rule_tac [16] impI)+
apply ((rule_tac [17] impI)+, (rule_tac [17] conjI)?)+
apply (rule_tac [18-20] impI)+
proof -
fix evsR1 S A U s n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇NonceS := Some s⦈)"
show "?P ?S n run ∨
(∃b. (b = s ∨ Pri_AgrK b ∈ A) ∧ ExtMapK (?S (User m, n, run)) = Some b)"
proof (rule disjE [OF A], rule disjI1, simp add: fun_upd_apply, rule impI, simp)
qed (rule disjI2, simp add: fun_upd_apply, blast)
next
fix evsR1 S A U s n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇NonceS := Some s⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
proof (rule disjE [OF A], rule disjI1, simp add: fun_upd_apply, rule impI, simp)
qed (rule disjI2, simp add: fun_upd_apply)
next
fix evsC2 S A U s a n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨
(∃b. (b = a ∨ Pri_AgrK b ∈ A) ∧ ExtMapK (?S (User m, n, run)) = Some b)"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a m n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
let ?S = "S((User m, n', run') := S (User m, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨
(∃b. (b = a ∨ Pri_AgrK b ∈ A) ∧ ExtMapK (?S (User m, n, run)) = Some b)"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a m n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
let ?S = "S((User m, n', run') := S (User m, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨
(∃b. (b = a ∨ Pri_AgrK b ∈ A) ∧ ExtMapK (?S (User m, n, run)) = Some b)"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a m n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
let ?S = "S((User m, n', run') := S (User m, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨
(∃b. (b = a ∨ Pri_AgrK b ∈ A) ∧ ExtMapK (?S (User m, n, run)) = Some b)"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsC2 S A U s a m n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
let ?S = "S((User m, n', run') := S (User m, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
next
fix evsR2 S A U a b n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntMapK := Some b, ExtMapK := Some a⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
proof (rule disjE [OF A], rule disjI1, simp add: fun_upd_apply, rule impI, simp)
qed (rule disjI2, simp add: fun_upd_apply)
next
fix evsC3 S A U b c m' n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
assume
"ExtMapK (S (User m', n', run')) = None" and
"m' = 0"
hence B: "ExtMapK (S (Spy, n', run')) = None"
by simp
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇ExtMapK := Some b, IntAgrK := Some c⦈)"
show "?P ?S n run ∨
(∃b. (b = c ∨ Pri_AgrK b ∈ A) ∧ ExtMapK (?S (User m, n, run)) = Some b)"
proof (rule disjE [OF A], rule disjI1, simp add: fun_upd_apply)
qed (rule disjI2, simp add: fun_upd_apply, rule conjI, rule impI, simp add: B, blast)
next
fix evsC3 S A U b c m' n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
assume B: "ExtMapK (S (User m', n', run')) = None"
let ?S = "S((User m', n', run') := S (User m', n', run')
⦇ExtMapK := Some b, IntAgrK := Some c⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
proof (rule disjE [OF A], rule disjI1, simp add: fun_upd_apply)
qed (rule disjI2, simp add: fun_upd_apply, rule impI, simp add: B)
next
fix evsR3 A s a b c d n' run' X and S :: state
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntAgrK := Some d, ExtAgrK := Some (c * (s + a * b))⦈)"
assume "sesK K = sesK (c * d * (s + a * b))"
with sesK_inj have "K = c * d * (s + a * b)"
by (rule injD)
thus "?P ?S n' run' ∨
(∃b. Pri_AgrK b ∈ A ∧ ExtMapK (?S (X, n', run')) = Some b)"
by (simp add: fun_upd_apply)
next
fix evsR3 A U s a b c d n' run' and S :: state
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntAgrK := Some d, ExtAgrK := Some (c * (s + a * b))⦈)"
assume "sesK K = sesK (c * d * (s + a * b))"
with sesK_inj have "K = c * d * (s + a * b)"
by (rule injD)
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately have "Key (sesK K) ∉ U"
by simp
moreover assume
"(evsR3, S, A, U) ∈ protocol" and
"⦃Key (sesK K), Agent (User m), Number n, Number run⦄ ∈ U"
hence "Key (sesK K) ∈ U"
by (rule pr_sesk_user_2)
ultimately show "?P ?S n run ∨ ?Q ?S A n run"
by contradiction
next
fix evsR3 S A U s a b c d n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
assume B: "IntAgrK (S (Card n', n', run')) = None"
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntAgrK := Some d, ExtAgrK := Some (c * (s + a * b))⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
proof (rule disjE [OF A], rule disjI1, simp add: fun_upd_apply, rule impI, simp add: B)
qed (rule disjI2, simp add: fun_upd_apply)
next
fix evsR3 A U s s' a b c d n' run' X and S :: state
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntAgrK := Some d, ExtAgrK := Some (c * (s' + a * b))⦈)"
assume "(evsR3, S, A, U) ∈ protocol"
hence "A ⊆ U"
by (rule pr_analz_used)
moreover assume "Key (sesK (c * d * (s + a * b))) ∈ A"
ultimately have "Key (sesK (c * d * (s + a * b))) ∈ U" ..
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show "?P ?S n' run' ∨
(∃b. Pri_AgrK b ∈ A ∧ ExtMapK (?S (X, n', run')) = Some b)"
by contradiction
next
fix evsR3 S A U s a b c d n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
assume B: "IntAgrK (S (Card n', n', run')) = None"
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntAgrK := Some d, ExtAgrK := Some (c * (s + a * b))⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
proof (rule disjE [OF A], rule disjI1, simp add: fun_upd_apply, rule impI, simp add: B)
qed (rule disjI2, simp add: fun_upd_apply)
next
fix evsFR3 A U s a b c d n' run' and S :: state
assume "sesK K = sesK (c * d * (s + a * b))"
with sesK_inj have "K = c * d * (s + a * b)"
by (rule injD)
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately have "Key (sesK K) ∉ U"
by simp
moreover assume
"(evsFR3, S, A, U) ∈ protocol" and
"⦃Key (sesK K), Agent (User m), Number n, Number run⦄ ∈ U"
hence "Key (sesK K) ∈ U"
by (rule pr_sesk_user_2)
ultimately show "?P S n run ∨ ?Q S A n run"
by contradiction
next
fix evsC4 S A U f m' n' run'
assume
"?H1 U ⟶ ?H2 A ⟶ ?P S n run ∨ ?Q S A n run" and
"?H1 U" and
"?H2 A"
hence A: "?P S n run ∨ ?Q S A n run"
by simp
let ?S = "S((User m', n', run') := S (User m', n', run')
⦇ExtAgrK := Some f⦈)"
show "?P ?S n run ∨ ?Q ?S A n run"
by (rule disjE [OF A], simp_all add: fun_upd_apply, blast)
qed
declare fun_upd_apply [simp]
lemma pr_sesk_auth [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Crypt (sesK K) ⦃pubAK e, Auth_Data x y, pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ parts (A ∪ spies evs) ⟶
Key (sesK K) ∈ U"
proof (erule protocol.induct, subst parts_simp, (simp, blast)+,
simp_all add: parts_simp_insert parts_auth_data parts_crypt parts_mpair,
rule_tac [!] impI)
fix evsR4 S A U n run d e
assume
"(evsR4, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some e"
thus "Key (sesK (d * e)) ∈ U"
by (rule pr_sesk_card)
next
fix evsFR4 S A U m n run c f
assume A: "(evsFR4, S, A, U) ∈ protocol" and
"IntAgrK (S (User m, n, run)) = Some c" and
"ExtAgrK (S (User m, n, run)) = Some f"
hence "⦃Key (sesK (c * f)), Agent (User m), Number n, Number run⦄ ∈ U"
by (rule pr_sesk_user_1)
with A show "Key (sesK (c * f)) ∈ U"
by (rule pr_sesk_user_2)
qed
lemma pr_sesk_passwd [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Says n run 5 X (Card n) (Crypt (sesK K) (Passwd m)) ∈ set evs ⟶
Key (sesK K) ∈ U"
proof (erule protocol.induct, simp_all, rule_tac [!] impI)
fix evsC5 S A U m n run s a b c f g X
assume "(evsC5, S, A, U) ∈ protocol"
moreover assume "Says n run 4 X (User m) (Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄) ∈ set evsC5"
(is "Says _ _ _ _ _ ?M ∈ _")
hence "?M ∈ spies evsC5"
by (rule set_spies)
hence "?M ∈ A ∪ spies evsC5" ..
hence "?M ∈ parts (A ∪ spies evsC5)"
by (rule parts.Inj)
ultimately show "Key (sesK (c * f)) ∈ U"
by (rule pr_sesk_auth)
next
fix evsFC5 S A U n run d e
assume
"(evsFC5, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some e"
thus "Key (sesK (d * e)) ∈ U"
by (rule pr_sesk_card)
qed
lemma pr_sesk_card_user [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
User m ≠ Spy ⟶
NonceS (S (User m, n, run)) = Some s ⟶
IntMapK (S (User m, n, run)) = Some a ⟶
ExtMapK (S (User m, n, run)) = Some b ⟶
IntAgrK (S (User m, n, run)) = Some c ⟶
NonceS (S (Card n, n, run)) = Some s' ⟶
IntMapK (S (Card n, n, run)) = Some b' ⟶
ExtMapK (S (Card n, n, run)) = Some a' ⟶
IntAgrK (S (Card n, n, run)) = Some d ⟶
ExtAgrK (S (Card n, n, run)) = Some (c * (s + a * b)) ⟶
s' + a' * b' = s + a * b ⟶
Key (sesK (c * d * (s + a * b))) ∉ A"
apply (erule protocol.induct, rule_tac [!] impI, simp_all add: pr_pri_agrk_analz)
apply (rule impI)+
apply (rule_tac [2] impI)
apply (rule_tac [2] conjI)
apply (rule_tac [2-3] impI)+
apply (rule_tac [4] impI)+
apply (rule_tac [5] impI)+
apply (rule_tac [6] conjI, (rule_tac [6] impI)+)+
apply (rule_tac [6] conjI)
apply (erule_tac [6] conjE)+
apply (rule_tac [8] impI)+
apply (rule_tac [8] notI)
apply (rule_tac [9] impI, rule_tac [9] conjI)+
apply (rule_tac [9] impI)+
apply (rule_tac [10] impI)+
apply (rule_tac [10] notI)
apply (rule_tac [11] impI)+
apply (rule_tac [12] impI)+
apply (rule_tac [12] notI)
proof simp_all
fix evsR1 S A U n run
assume "(evsR1, S, A, U) ∈ protocol" and
"NonceS (S (Card n, n, run)) = None"
hence "IntMapK (S (Card n, n, run)) = None"
by (rule pr_state_1)
moreover assume "IntMapK (S (Card n, n, run)) = Some b'"
ultimately show "Key (sesK (c * d * (s + a * b))) ∉ A"
by simp
next
fix evsC2 S A U m n run
assume A: "(evsC2, S, A, U) ∈ protocol"
moreover assume "NonceS (S (User m, n, run)) = None"
ultimately have "IntMapK (S (User m, n, run)) = None"
by (rule pr_state_1)
with A have "ExtMapK (S (User m, n, run)) = None"
by (rule pr_state_2)
moreover assume "ExtMapK (S (User m, n, run)) = Some b"
ultimately show "Key (sesK (c * d * (a * b))) ∉ A"
by simp
next
fix evsC2 S A U m n run
assume A: "(evsC2, S, A, U) ∈ protocol"
moreover assume "NonceS (S (User m, n, run)) = None"
ultimately have "IntMapK (S (User m, n, run)) = None"
by (rule pr_state_1)
with A have "ExtMapK (S (User m, n, run)) = None"
by (rule pr_state_2)
moreover assume "ExtMapK (S (User m, n, run)) = Some b"
ultimately show "Key (sesK (c * d * (s + a * b))) ∉ A"
by simp
next
fix evsR2 S A U n run
assume A: "(evsR2, S, A, U) ∈ protocol" and
"IntMapK (S (Card n, n, run)) = None"
hence "ExtMapK (S (Card n, n, run)) = None"
by (rule pr_state_2)
with A have "IntAgrK (S (Card n, n, run)) = None"
by (rule pr_state_3)
moreover assume "IntAgrK (S (Card n, n, run)) = Some d"
ultimately show "Key (sesK (c * d * (s + a * b))) ∉ A"
by simp
next
fix evsC3 S A U n run
assume A: "(evsC3, S, A, U) ∈ protocol" and
"NonceS (S (Card n, n, run)) = Some s'" and
"IntMapK (S (Card n, n, run)) = Some b'" and
"ExtMapK (S (Card n, n, run)) = Some a'" and
"IntAgrK (S (Card n, n, run)) = Some d"
moreover assume B: "s' + a' * b' = s + a * b" and
"ExtAgrK (S (Card n, n, run)) = Some (c * (s + a * b))"
hence "ExtAgrK (S (Card n, n, run)) = Some (c * (s' + a' * b'))"
by simp
moreover assume C: "Pri_AgrK c ∉ U"
have "A ⊆ U"
using A by (rule pr_analz_used)
hence "Pri_AgrK c ∉ A"
using C by (rule contra_subsetD)
ultimately have "Key (sesK (c * d * (s' + a' * b'))) ∉ A"
by (rule pr_ext_agrk_card)
thus "Key (sesK (c * d * (s + a * b))) ∉ A"
using B by simp
next
fix evsR3 S A U n run
assume "(evsR3, S, A, U) ∈ protocol"
moreover assume "0 < m"
hence "User m ≠ Spy"
by simp
moreover assume "IntAgrK (S (User m, n, run)) = Some c"
ultimately have "Pri_AgrK c ∉ A"
by (rule pr_int_agrk_user_2)
moreover assume "Pri_AgrK c ∈ A"
ultimately show False
by contradiction
next
fix evsR3 S A U
assume "(evsR3, S, A, U) ∈ protocol"
hence "A ⊆ U"
by (rule pr_analz_used)
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show "Key (sesK (c * d * (s + a * b))) ∉ A"
by (rule contra_subsetD)
next
fix evsR3 S A U s' a' b' c' d'
assume
"(evsR3, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some (c * (s + a * b))"
hence "Key (sesK (d * (c * (s + a * b)))) ∈ U"
by (rule pr_sesk_card)
moreover have "d * (c * (s + a * b)) = c * d * (s + a * b)"
by simp
ultimately have "Key (sesK (c * d * (s + a * b))) ∈ U"
by simp
moreover assume "sesK (c * d * (s + a * b)) = sesK (c' * d' * (s' + a' * b'))"
ultimately have "Key (sesK (c' * d' * (s' + a' * b'))) ∈ U"
by simp
moreover assume "Key (sesK (c' * d' * (s' + a' * b'))) ∉ U"
ultimately show False
by simp
next
fix evsR3 S A U s' a' b' c' d'
assume
"(evsR3, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some (c * (s + a * b))"
hence "Key (sesK (d * (c * (s + a * b)))) ∈ U"
by (rule pr_sesk_card)
moreover have "d * (c * (s + a * b)) = c * d * (s + a * b)"
by simp
ultimately have "Key (sesK (c * d * (s + a * b))) ∈ U"
by simp
moreover assume "sesK (c * d * (s + a * b)) = sesK (c' * d' * (s' + a' * b'))"
ultimately have "Key (sesK (c' * d' * (s' + a' * b'))) ∈ U"
by simp
moreover assume "Key (sesK (c' * d' * (s' + a' * b'))) ∉ U"
ultimately show False
by simp
next
fix evsR3 S A U s' c'
assume "(evsR3, S, A, U) ∈ protocol"
hence "A ⊆ U"
by (rule pr_analz_used)
moreover assume "Key (sesK (c' * d * (s' + a' * b'))) ∉ U"
ultimately have "Key (sesK (c' * d * (s' + a' * b'))) ∉ A"
by (rule contra_subsetD)
moreover assume "c' * (s' + a' * b') = c * (s + a * b)"
hence "c' * d * (s' + a' * b') = c * d * (s + a * b)"
by simp
ultimately show "Key (sesK (c * d * (s + a * b))) ∉ A"
by simp
next
fix evsFR3 S A U s' a' b' c' d'
assume
"(evsFR3, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some (c * (s + a * b))"
hence "Key (sesK (d * (c * (s + a * b)))) ∈ U"
by (rule pr_sesk_card)
moreover have "d * (c * (s + a * b)) = c * d * (s + a * b)"
by simp
ultimately have "Key (sesK (c * d * (s + a * b))) ∈ U"
by simp
moreover assume "sesK (c * d * (s + a * b)) = sesK (c' * d' * (s' + a' * b'))"
ultimately have "Key (sesK (c' * d' * (s' + a' * b'))) ∈ U"
by simp
moreover assume "Key (sesK (c' * d' * (s' + a' * b'))) ∉ U"
ultimately show False
by simp
qed
lemma pr_sign_key_used:
"(evs, S, A, U) ∈ protocol ⟹ Key (priSK X) ∈ U"
by (erule protocol.induct, simp_all)
lemma pr_sign_key_analz:
"(evs, S, A, U) ∈ protocol ⟹ Key (priSK X) ∉ analz (A ∪ spies evs)"
proof (simp add: pr_key_analz, erule protocol.induct,
auto simp add: priSK_pubSK priSK_symK)
fix evsR3 S A U s a b c d
assume "(evsR3, S, A, U) ∈ protocol"
hence "Key (priSK X) ∈ U"
by (rule pr_sign_key_used)
moreover assume "priSK X = sesK (c * d * (s + a * b))"
ultimately have "Key (sesK (c * d * (s + a * b))) ∈ U"
by simp
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show False
by contradiction
next
fix evsFR3 S A U s a b c d
assume "(evsFR3, S, A, U) ∈ protocol"
hence "Key (priSK X) ∈ U"
by (rule pr_sign_key_used)
moreover assume "priSK X = sesK (c * d * (s + a * b))"
ultimately have "Key (sesK (c * d * (s + a * b))) ∈ U"
by simp
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show False
by contradiction
qed
lemma pr_auth_data_parts [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Auth_Data (priAK n) b ∈ parts (A ∪ spies evs) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)"
(is "_ ⟹ ?M ∈ _ ⟶ _")
apply (erule protocol.induct, simp, subst parts_simp, simp, blast+, simp_all
add: parts_simp_insert parts_auth_data parts_crypt parts_mpair del: fun_upd_apply)
apply (rule impI)
apply ((rule_tac [2] conjI)?, rule_tac [2] impI)+
apply (rule_tac [3] impI)+
apply (rule_tac [4] impI, (rule_tac [4] conjI)?)+
apply (rule_tac [5] impI)+
apply (rule_tac [6] impI, (rule_tac [6] conjI)?)+
apply (rule_tac [7] impI)+
apply (rule_tac [8] impI, (rule_tac [8] conjI)?)+
apply (rule_tac [9] impI)+
apply (rule_tac [10] impI)
apply (rule_tac [11] conjI)
apply (rule_tac [11-12] impI)+
apply (rule_tac [13] conjI)
apply (rule_tac [13-14] impI)+
apply (rule_tac [15-17] impI)
apply (erule_tac [17] conjE)
proof -
fix evsR1 A n' run' s and S :: state
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇NonceS := Some s⦈)"
assume
"?M ∈ parts (A ∪ spies evsR1) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsR1)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp, blast)
next
fix evsC2 A n' run' s a and S :: state
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
assume
"?M ∈ parts (A ∪ spies evsC2) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsC2)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp)
next
fix evsC2 A n' run' m' s a and S :: state
let ?S = "S((User m', n', run') := S (User m', n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
assume
"?M ∈ parts (A ∪ spies evsC2) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsC2)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp)
next
fix evsC2 A n' run' s a and S :: state
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
assume
"?M ∈ parts (A ∪ spies evsC2) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsC2)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp)
next
fix evsC2 A n' run' m' a and S :: state
let ?S = "S((User m', n', run') := S (User m', n', run')
⦇NonceS := Some 0, IntMapK := Some a⦈)"
assume
"?M ∈ parts (A ∪ spies evsC2) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsC2)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp)
next
fix evsC2 A n' run' s a and S :: state
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
assume
"?M ∈ parts (A ∪ spies evsC2) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsC2)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp)
next
fix evsC2 A n' run' m' s a and S :: state
let ?S = "S((User m', n', run') := S (User m', n', run')
⦇NonceS := Some s, IntMapK := Some a⦈)"
assume
"?M ∈ parts (A ∪ spies evsC2) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsC2)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp)
next
fix evsC2 A n' run' a and S :: state
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇NonceS := Some 0, IntMapK := Some a⦈)"
assume
"?M ∈ parts (A ∪ spies evsC2) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsC2)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp)
next
fix evsC2 A n' run' m' a and S :: state
let ?S = "S((User m', n', run') := S (User m', n', run')
⦇NonceS := Some 0, IntMapK := Some a⦈)"
assume
"?M ∈ parts (A ∪ spies evsC2) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsC2)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp)
next
fix evsR2 A n' run' a b' and S :: state
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntMapK := Some b', ExtMapK := Some a⦈)"
assume
"?M ∈ parts (A ∪ spies evsR2) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsR2)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
moreover assume "IntMapK (S (Card n', n', run')) = None"
ultimately show "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
proof (rule_tac x = m in exI, rule_tac x = run in exI, simp)
qed (rule impI, simp)
next
fix evsC3 A n' run' b' c and S :: state
let ?S = "S((Spy, n', run') := S (Spy, n', run')
⦇ExtMapK := Some b', IntAgrK := Some c⦈)"
assume
"?M ∈ parts (A ∪ spies evsC3) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsC3)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp)
next
fix evsC3 A n' run' b' c m and S :: state
let ?S = "S((User m, n', run') := S (User m, n', run')
⦇ExtMapK := Some b', IntAgrK := Some c⦈)"
assume
"?M ∈ parts (A ∪ spies evsC3) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsC3)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp)
next
fix evsR3 A n' run' s a b' c d and S :: state
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntAgrK := Some d, ExtAgrK := Some (c * (s + a * b'))⦈)"
assume
"?M ∈ parts (A ∪ spies evsR3) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsR3)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp, blast)
next
fix evsR3 A n' run' s a b' c d and S :: state
let ?S = "S((Card n', n', run') := S (Card n', n', run')
⦇IntAgrK := Some d, ExtAgrK := Some (c * (s + a * b'))⦈)"
assume
"?M ∈ parts (A ∪ spies evsR3) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsR3)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp, blast)
next
fix evsC4 A n' run' c f m and S :: state
let ?S = "S((User m, n', run') := S (User m, n', run')⦇ExtAgrK := Some f⦈)"
assume
"?M ∈ parts (A ∪ spies evsC4) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
"?M ∈ parts (A ∪ spies evsC4)"
hence "∃m run. IntMapK (S (Card m, m, run)) = Some b" ..
then obtain m and run where "IntMapK (S (Card m, m, run)) = Some b"
by blast
thus "∃m run. IntMapK (?S (Card m, m, run)) = Some b"
by (rule_tac x = m in exI, rule_tac x = run in exI, simp)
next
fix evsR4 n' run' b' and S :: state
assume "IntMapK (S (Card n', n', run')) = Some b'"
thus "∃m run. IntMapK (S (Card m, m, run)) = Some b'"
by blast
next
fix evsFR4 A U s a b' c f g and S :: state
assume
A: "?M ∈ parts (A ∪ spies evsFR4) ⟶
(∃m run. IntMapK (S (Card m, m, run)) = Some b)" and
B: "(evsFR4, S, A, U) ∈ protocol" and
C: "Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b')), Auth_Data g b', pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄ ∈ synth (analz (A ∪ spies evsFR4))"
(is "Crypt _ ?M' ∈ synth (analz ?A)") and
D: "priAK n = g" and
E: "b = b'"
show "∃m run. IntMapK (S (Card m, m, run)) = Some b'"
proof -
have "Crypt (sesK (c * f)) ?M' ∈ analz ?A ∨
?M' ∈ synth (analz ?A) ∧ Key (sesK (c * f)) ∈ analz ?A"
using C by (rule synth_crypt)
moreover {
assume "Crypt (sesK (c * f)) ?M' ∈ analz ?A"
hence "Crypt (sesK (c * f)) ?M' ∈ parts ?A"
by (rule subsetD [OF analz_parts_subset])
hence "?M' ∈ parts ?A"
by (rule parts.Body)
hence "⦃Auth_Data g b', pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ parts ?A"
by (rule parts.Snd)
hence "Auth_Data g b' ∈ parts ?A"
by (rule parts.Fst)
}
moreover {
assume "?M' ∈ synth (analz ?A) ∧ Key (sesK (c * f)) ∈ analz ?A"
hence "?M' ∈ synth (analz ?A)" ..
hence "⦃Auth_Data g b', pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ synth (analz ?A)"
by (rule synth_analz_snd)
hence "Auth_Data g b' ∈ synth (analz ?A)"
by (rule synth_analz_fst)
hence "Auth_Data g b' ∈ analz ?A ∨
Pri_AgrK g ∈ analz ?A ∧ Pri_AgrK b' ∈ analz ?A"
by (rule synth_auth_data)
moreover {
assume "Auth_Data g b' ∈ analz ?A"
hence "Auth_Data g b' ∈ parts ?A"
by (rule subsetD [OF analz_parts_subset])
}
moreover {
assume "Pri_AgrK g ∈ analz ?A ∧ Pri_AgrK b' ∈ analz ?A"
hence "Pri_AgrK g ∈ analz ?A" ..
hence "Pri_AgrK (priAK n) ∈ analz ?A"
using D by simp
moreover have "Pri_AgrK (priAK n) ∉ analz ?A"
using B by (rule pr_auth_key_analz)
ultimately have "Auth_Data g b' ∈ parts ?A"
by contradiction
}
ultimately have "Auth_Data g b' ∈ parts ?A" ..
}
ultimately have "Auth_Data g b' ∈ parts ?A" ..
thus ?thesis
using A and D and E by simp
qed
qed
lemma pr_sign_parts [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Crypt (priSK CA) (Hash (pubAK g)) ∈ parts (A ∪ spies evs) ⟶
(∃n. g = priAK n)"
(is "_ ⟹ ?M g ∈ _ ⟶ _")
proof (erule protocol.induct, subst parts_simp, (simp, blast)+, simp_all add:
parts_simp_insert parts_auth_data parts_crypt parts_mpair, rule_tac [!] impI)
fix evsR4 n
assume "agrK g = agrK (priAK n)"
with agrK_inj have "g = priAK n"
by (rule injD)
thus "∃n. g = priAK n" ..
next
fix evsFR4 S A U s a b c f g'
assume
A: "?M g ∈ parts (A ∪ spies evsFR4) ⟶ (∃n. g = priAK n)" and
B: "(evsFR4, S, A, U) ∈ protocol" and
C: "Crypt (sesK (c * f)) ⦃pubAK (c * (s + a * b)), Auth_Data g' b,
pubAK g', ?M g'⦄ ∈ synth (analz (A ∪ spies evsFR4))"
(is "?M' ∈ synth (analz ?A)")
assume "agrK g = agrK g'"
with agrK_inj have D: "g = g'"
by (rule injD)
show "∃n. g = priAK n"
proof -
have "?M' ∈ analz ?A ∨
⦃pubAK (c * (s + a * b)), Auth_Data g' b, pubAK g', ?M g'⦄
∈ synth (analz ?A) ∧
Key (sesK (c * f)) ∈ analz ?A"
using C by (rule synth_crypt)
moreover {
assume "?M' ∈ analz ?A"
hence "?M' ∈ parts ?A"
by (rule subsetD [OF analz_parts_subset])
hence "⦃pubAK (c * (s + a * b)), Auth_Data g' b, pubAK g', ?M g'⦄
∈ parts ?A"
by (rule parts.Body)
hence "?M g' ∈ parts ?A"
by (rule_tac parts.Snd, assumption?)+
hence "∃n. g' = priAK n"
using A and D by simp
}
moreover {
assume
"⦃pubAK (c * (s + a * b)), Auth_Data g' b, pubAK g', ?M g'⦄
∈ synth (analz ?A) ∧
Key (sesK (c * f)) ∈ analz ?A"
hence
"⦃pubAK (c * (s + a * b)), Auth_Data g' b, pubAK g', ?M g'⦄
∈ synth (analz ?A)" ..
hence "⦃Auth_Data g' b, pubAK g', ?M g'⦄ ∈ synth (analz ?A)"
by (rule synth_analz_snd)
hence "⦃pubAK g', ?M g'⦄ ∈ synth (analz ?A)"
by (rule synth_analz_snd)
hence "?M g' ∈ synth (analz ?A)"
by (rule synth_analz_snd)
hence "?M g' ∈ analz ?A ∨
Hash (pubAK g') ∈ synth (analz ?A) ∧ Key (priSK CA) ∈ analz ?A"
by (rule synth_crypt)
moreover {
assume "?M g' ∈ analz ?A"
hence "?M g' ∈ parts ?A"
by (rule subsetD [OF analz_parts_subset])
hence "∃n. g' = priAK n"
using A and D by simp
}
moreover {
assume "Hash (pubAK g') ∈ synth (analz ?A) ∧
Key (priSK CA) ∈ analz ?A"
hence "Key (priSK CA) ∈ analz ?A" ..
moreover have "Key (priSK CA) ∉ analz ?A"
using B by (rule pr_sign_key_analz)
ultimately have "∃n. g' = priAK n"
by contradiction
}
ultimately have "∃n. g' = priAK n" ..
}
ultimately have "∃n. g' = priAK n" ..
thus "∃n. g = priAK n"
using D by simp
qed
qed
lemma pr_key_secrecy_aux [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
User m ≠ Spy ⟶
NonceS (S (User m, n, run)) = Some s ⟶
IntMapK (S (User m, n, run)) = Some a ⟶
ExtMapK (S (User m, n, run)) = Some b ⟶
IntAgrK (S (User m, n, run)) = Some c ⟶
ExtAgrK (S (User m, n, run)) = Some f ⟶
Says n run 4 X (User m) (Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄) ∈ set evs ⟶
Key (sesK (c * f)) ∉ A"
supply [[simproc del: defined_all]]
apply (erule protocol.induct, (rule_tac [!] impI)+, simp_all split: if_split_asm)
apply (erule_tac [7] disjE)
apply simp_all
apply (erule_tac [7] conjE)+
apply (erule_tac [8] disjE)+
apply (erule_tac [8] conjE)+
apply simp_all
apply (rule_tac [8] notI)
proof -
fix evsC2 S A U m n run
assume A: "(evsC2, S, A, U) ∈ protocol"
moreover assume "NonceS (S (User m, n, run)) = None"
ultimately have "IntMapK (S (User m, n, run)) = None"
by (rule pr_state_1)
with A have "ExtMapK (S (User m, n, run)) = None"
by (rule pr_state_2)
moreover assume "ExtMapK (S (User m, n, run)) = Some b"
ultimately show "Key (sesK (c * f)) ∉ A"
by simp
next
fix evsC2 S A U m n run
assume A: "(evsC2, S, A, U) ∈ protocol"
moreover assume "NonceS (S (User m, n, run)) = None"
ultimately have "IntMapK (S (User m, n, run)) = None"
by (rule pr_state_1)
with A have "ExtMapK (S (User m, n, run)) = None"
by (rule pr_state_2)
moreover assume "ExtMapK (S (User m, n, run)) = Some b"
ultimately show "Key (sesK (c * f)) ∉ A"
by simp
next
fix evsC3 S A U m n run
assume A: "(evsC3, S, A, U) ∈ protocol" and
"ExtMapK (S (User m, n, run)) = None"
hence "IntAgrK (S (User m, n, run)) = None"
by (rule pr_state_3)
with A have "ExtAgrK (S (User m, n, run)) = None"
by (rule pr_state_4)
moreover assume "ExtAgrK (S (User m, n, run)) = Some f"
ultimately show "Key (sesK (c * f)) ∉ A"
by simp
next
fix evsR3 S A U d s' s'' a' b' c'
assume
A: "(evsR3, S, A, U) ∈ protocol" and
B: "Key (sesK (c' * d * (s'' + a' * b'))) ∉ U" and
C: "Says n run 4 X (User m) (Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄) ∈ set evsR3"
(is "Says _ _ _ _ _ ?M ∈ _")
show "s'' = s' ∧ Pri_AgrK c' ∈ analz (A ∪ spies evsR3) ⟶
sesK (c * f) ≠ sesK (c' * d * (s' + a' * b'))"
proof (rule impI, rule notI, erule conjE)
have "?M ∈ spies evsR3"
using C by (rule set_spies)
hence "?M ∈ A ∪ spies evsR3"
by simp
hence "?M ∈ parts (A ∪ spies evsR3)"
by (rule parts.Inj)
with A have "Key (sesK (c * f)) ∈ U"
by (rule pr_sesk_auth)
moreover assume "sesK (c * f) = sesK (c' * d * (s' + a' * b'))" and "s'' = s'"
hence "Key (sesK (c * f)) ∉ U"
using B by simp
ultimately show False
by contradiction
qed
next
fix evsFR3 S A U s' a' b' c' d
assume
A: "(evsFR3, S, A, U) ∈ protocol" and
B: "Key (sesK (c' * d * (s' + a' * b'))) ∉ U" and
C: "Says n run 4 X (User m) (Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄) ∈ set evsFR3"
(is "Says _ _ _ _ _ ?M ∈ _")
show "sesK (c * f) ≠ sesK (c' * d * (s' + a' * b'))"
proof
have "?M ∈ spies evsFR3"
using C by (rule set_spies)
hence "?M ∈ A ∪ spies evsFR3"
by simp
hence "?M ∈ parts (A ∪ spies evsFR3)"
by (rule parts.Inj)
with A have "Key (sesK (c * f)) ∈ U"
by (rule pr_sesk_auth)
moreover assume "sesK (c * f) = sesK (c' * d * (s' + a' * b'))"
hence "Key (sesK (c * f)) ∉ U"
using B by simp
ultimately show False
by contradiction
qed
next
fix evsC4 S A U n run and m :: nat
assume "(evsC4, S, A, U) ∈ protocol"
moreover assume "0 < m"
hence "User m ≠ Spy"
by simp
moreover assume "Says n run 4 X (User m) (Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄) ∈ set evsC4"
ultimately have "ExtAgrK (S (User m, n, run)) ≠ None"
by (rule pr_ext_agrk_user_2)
moreover assume "ExtAgrK (S (User m, n, run)) = None"
ultimately show "Key (sesK (c * f)) ∉ A"
by contradiction
next
fix evsR4 A U n run X s' a' b' d e and S :: state
assume A: "User m = X"
assume "agrK (c * (s + a * b')) = agrK e"
with agrK_inj have B: "c * (s + a * b') = e"
by (rule injD)
assume "sesK (c * f) = sesK (d * e)"
with sesK_inj have "c * f = d * e"
by (rule injD)
hence C: "c * f = c * d * (s + a * b')"
using B by simp
assume "ExtAgrK (S (X, n, run)) = Some f"
hence D: "ExtAgrK (S (User m, n, run)) = Some f"
using A by simp
assume E: "(evsR4, S, A, U) ∈ protocol"
moreover assume "0 < m"
hence F: "User m ≠ Spy"
by simp
moreover assume "NonceS (S (X, n, run)) = Some s"
hence G: "NonceS (S (User m, n, run)) = Some s"
using A by simp
moreover assume "IntMapK (S (X, n, run)) = Some a"
hence H: "IntMapK (S (User m, n, run)) = Some a"
using A by simp
moreover assume "ExtMapK (S (X, n, run)) = Some b'"
hence I: "ExtMapK (S (User m, n, run)) = Some b'"
using A by simp
moreover assume "IntAgrK (S (X, n, run)) = Some c"
hence J: "IntAgrK (S (User m, n, run)) = Some c"
using A by simp
moreover assume K: "NonceS (S (Card n, n, run)) = Some s'"
moreover assume L: "IntMapK (S (Card n, n, run)) = Some b'"
moreover assume M: "ExtMapK (S (Card n, n, run)) = Some a'"
moreover assume N: "IntAgrK (S (Card n, n, run)) = Some d"
moreover assume "ExtAgrK (S (Card n, n, run)) = Some e"
hence "ExtAgrK (S (Card n, n, run)) = Some (c * (s + a * b'))"
using B by simp
moreover assume "Says n run 4 X (Card n)
(Crypt (sesK (d * e)) (pubAK (d * (s' + a' * b')))) ∈ set evsR4"
hence "Says n run 4 (User m) (Card n)
(Crypt (sesK (d * e)) (pubAK (d * (s' + a' * b')))) ∈ set evsR4"
using A by simp
with E and F and D have "d * (s' + a' * b') = f"
by (rule pr_ext_agrk_user_3)
hence "c * d * (s' + a' * b') = c * d * (s + a * b')"
using C by auto
hence "s' + a' * b' = s + a * b'"
proof auto
assume "c = 0"
moreover have "c * (s + a * b') ≠ 0"
using E and G and H and I and J by (rule pr_int_agrk_user_3)
ultimately show ?thesis
by simp
next
assume "d = 0"
moreover have "d * (s' + a' * b') ≠ 0"
using E and K and L and M and N by (rule pr_int_agrk_card)
ultimately show ?thesis
by simp
qed
ultimately have "Key (sesK (c * d * (s + a * b'))) ∉ A"
by (rule pr_sesk_card_user)
moreover have "c * d * (s + a * b') = d * e"
using B by simp
ultimately show "Key (sesK (d * e)) ∉ A"
by simp
next
fix evsFR4 S A U m n run b g
assume
A: "(evsFR4, S, A, U) ∈ protocol" and
B: "ExtMapK (S (User m, n, run)) = Some b" and
C: "IntAgrK (S (User m, n, run)) = Some c" and
D: "ExtAgrK (S (User m, n, run)) = Some f" and
E: "0 < m" and
F: "Key (sesK (c * f)) ∈ A"
assume G: "Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄ ∈ synth (analz (A ∪ spies evsFR4))"
(is "Crypt _ ?M ∈ synth (analz ?A)")
hence "Crypt (sesK (c * f)) ?M ∈ analz ?A ∨
?M ∈ synth (analz ?A) ∧ Key (sesK (c * f)) ∈ analz ?A"
by (rule synth_crypt)
moreover {
assume "Crypt (sesK (c * f)) ?M ∈ analz ?A"
hence "Crypt (sesK (c * f)) ?M ∈ parts ?A"
by (rule subsetD [OF analz_parts_subset])
hence "?M ∈ parts ?A"
by (rule parts.Body)
hence "Crypt (priSK CA) (Hash (pubAK g)) ∈ parts ?A"
by (rule_tac parts.Snd, assumption?)+
with A have "∃n. g = priAK n"
by (rule pr_sign_parts)
}
moreover {
assume "?M ∈ synth (analz ?A) ∧ Key (sesK (c * f)) ∈ analz ?A"
hence "?M ∈ synth (analz ?A)" ..
hence "⦃Auth_Data g b, pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ synth (analz ?A)"
by (rule synth_analz_snd)
hence "⦃pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄ ∈ synth (analz ?A)"
by (rule synth_analz_snd)
hence "Crypt (priSK CA) (Hash (pubAK g)) ∈ synth (analz ?A)"
by (rule synth_analz_snd)
hence "Crypt (priSK CA) (Hash (pubAK g)) ∈ analz ?A ∨
Hash (pubAK g) ∈ synth (analz ?A) ∧ Key (priSK CA) ∈ analz ?A"
by (rule synth_crypt)
moreover {
assume "Crypt (priSK CA) (Hash (pubAK g)) ∈ analz ?A"
hence "Crypt (priSK CA) (Hash (pubAK g)) ∈ parts ?A"
by (rule subsetD [OF analz_parts_subset])
with A have "∃n. g = priAK n"
by (rule pr_sign_parts)
}
moreover {
assume "Hash (pubAK g) ∈ synth (analz ?A) ∧ Key (priSK CA) ∈ analz ?A"
hence "Key (priSK CA) ∈ analz ?A" ..
moreover have "Key (priSK CA) ∉ analz ?A"
using A by (rule pr_sign_key_analz)
ultimately have "∃n. g = priAK n"
by contradiction
}
ultimately have "∃n. g = priAK n" ..
}
ultimately have "∃n. g = priAK n" ..
then obtain n' where "g = priAK n'" ..
hence "Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data (priAK n') b, pubAK (priAK n'),
Crypt (priSK CA) (Hash (pubAK (priAK n')))⦄ ∈ synth (analz ?A)"
(is "Crypt _ ?M ∈ _")
using G by simp
hence "Crypt (sesK (c * f)) ?M ∈ analz ?A ∨
?M ∈ synth (analz ?A) ∧ Key (sesK (c * f)) ∈ analz ?A"
by (rule synth_crypt)
moreover {
assume "Crypt (sesK (c * f)) ?M ∈ analz ?A"
hence "Crypt (sesK (c * f)) ?M ∈ parts ?A"
by (rule subsetD [OF analz_parts_subset])
hence "?M ∈ parts ?A"
by (rule parts.Body)
hence "⦃Auth_Data (priAK n') b, pubAK (priAK n'),
Crypt (priSK CA) (Hash (pubAK (priAK n')))⦄ ∈ parts ?A"
by (rule parts.Snd)
hence "Auth_Data (priAK n') b ∈ parts ?A"
by (rule parts.Fst)
}
moreover {
assume "?M ∈ synth (analz ?A) ∧ Key (sesK (c * f)) ∈ analz ?A"
hence "?M ∈ synth (analz ?A)" ..
hence "⦃Auth_Data (priAK n') b, pubAK (priAK n'),
Crypt (priSK CA) (Hash (pubAK (priAK n')))⦄ ∈ synth (analz ?A)"
by (rule synth_analz_snd)
hence "Auth_Data (priAK n') b ∈ synth (analz ?A)"
by (rule synth_analz_fst)
hence "Auth_Data (priAK n') b ∈ analz ?A ∨
Pri_AgrK (priAK n') ∈ analz ?A ∧ Pri_AgrK b ∈ analz ?A"
by (rule synth_auth_data)
moreover {
assume "Auth_Data (priAK n') b ∈ analz ?A"
hence "Auth_Data (priAK n') b ∈ parts ?A"
by (rule subsetD [OF analz_parts_subset])
}
moreover {
assume "Pri_AgrK (priAK n') ∈ analz ?A ∧ Pri_AgrK b ∈ analz ?A"
hence "Pri_AgrK (priAK n') ∈ analz ?A" ..
moreover have "Pri_AgrK (priAK n') ∉ analz ?A"
using A by (rule pr_auth_key_analz)
ultimately have "Auth_Data (priAK n') b ∈ parts ?A"
by contradiction
}
ultimately have "Auth_Data (priAK n') b ∈ parts ?A" ..
}
ultimately have "Auth_Data (priAK n') b ∈ parts ?A" ..
with A have "∃n run. IntMapK (S (Card n, n, run)) = Some b"
by (rule pr_auth_data_parts)
then obtain n' and run' where "IntMapK (S (Card n', n', run')) = Some b"
by blast
with A have "Pri_AgrK b ∉ analz ?A"
by (rule pr_int_mapk_analz)
hence H: "Pri_AgrK b ∉ A"
using A by (simp add: pr_pri_agrk_analz)
have "∃X. Says n run 3 X (User m) (pubAK f) ∈ set evsFR4"
using A and D by (rule pr_ext_agrk_user_4)
then obtain X where "Says n run 3 X (User m) (pubAK f) ∈ set evsFR4" ..
with A have
"(∃s a b d. f = d * (s + a * b) ∧
NonceS (S (Card n, n, run)) = Some s ∧
IntMapK (S (Card n, n, run)) = Some b ∧
ExtMapK (S (Card n, n, run)) = Some a ∧
IntAgrK (S (Card n, n, run)) = Some d ∧
d ≠ 0 ∧ s + a * b ≠ 0) ∨
(∃b. Pri_AgrK b ∈ A ∧
ExtMapK (S (User m, n, run)) = Some b)"
(is "(∃s a b d. ?P s a b d) ∨ ?Q")
by (rule pr_ext_agrk_user_5)
moreover have I: "¬ ?Q"
proof (rule notI, erule exE, erule conjE)
fix b'
assume "ExtMapK (S (User m, n, run)) = Some b'"
hence "b' = b"
using B by simp
moreover assume "Pri_AgrK b' ∈ A"
ultimately have "Pri_AgrK b ∈ A"
by simp
thus False
using H by contradiction
qed
ultimately have "∃s a b d. ?P s a b d"
by simp
then obtain s' and a' and b' and d where J: "?P s' a' b' d"
by blast
hence "ExtAgrK (S (User m, n, run)) = Some (d * (s' + a' * b'))"
using D by simp
with A and C have
"⦃Key (sesK (c * (d * (s' + a' * b')))), Agent (User m), Number n, Number run⦄ ∈ U"
by (rule pr_sesk_user_1)
moreover have K: "Key (sesK (c * (d * (s' + a' * b')))) ∈ A"
using F and J by simp
ultimately have
"(∃d' e'. c * (d * (s' + a' * b')) = d' * e' ∧
IntAgrK (S (Card n, n, run)) = Some d' ∧
ExtAgrK (S (Card n, n, run)) = Some e') ∨
(∃b. Pri_AgrK b ∈ A ∧
ExtMapK (S (User m, n, run)) = Some b)"
(is "(∃d e. ?P d e) ∨ _")
by (rule pr_sesk_user_3 [OF A])
hence "∃d e. ?P d e"
using I by simp
then obtain d' and e' where L: "?P d' e'"
by blast
hence "d' = d"
using J by simp
hence "d * c * (s' + a' * b') = d * e'"
using L by simp
hence "e' = c * (s' + a' * b')"
using J by simp
hence M: "ExtAgrK (S (Card n, n, run)) = Some (c * (s' + a' * b'))"
using L by simp
have "c * (d * (s' + a' * b')) = c * d * (s' + a' * b')"
by simp
hence "Key (sesK (c * (d * (s' + a' * b')))) = Key (sesK (c * d * (s' + a' * b')))"
by (rule arg_cong)
hence "Key (sesK (c * d * (s' + a' * b'))) ∈ A"
using K by simp
moreover have "Key (sesK (c * d * (s' + a' * b'))) ∉ A"
proof (rule pr_ext_agrk_card [OF A, of n run], simp_all add: J M)
qed (rule pr_int_agrk_user_2 [OF A, of m n run], simp_all add: C E)
ultimately show False
by contradiction
qed
theorem pr_key_secrecy [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
User m ≠ Spy ⟶
Says n run 5 (User m) (Card n) (Crypt (sesK K) (Passwd m)) ∈ set evs ⟶
Key (sesK K) ∉ analz (A ∪ spies evs)"
proof (simp add: pr_key_analz, erule protocol.induct, simp_all,
(rule_tac [1] impI)+, (rule_tac [2-3] impI)+, rule_tac [1-2] notI, simp_all)
fix evsR3 S A U s a b c d
assume
"(evsR3, S, A, U) ∈ protocol" and
"Says n run 5 (User m) (Card n)
(Crypt (sesK (c * d * (s + a * b))) (Passwd m)) ∈ set evsR3"
hence "Key (sesK (c * d * (s + a * b))) ∈ U"
by (rule pr_sesk_passwd)
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show False
by contradiction
next
fix evsFR3 S A U s a b c d
assume
"(evsFR3, S, A, U) ∈ protocol" and
"Says n run 5 (User m) (Card n)
(Crypt (sesK (c * d * (s + a * b))) (Passwd m)) ∈ set evsFR3"
hence "Key (sesK (c * d * (s + a * b))) ∈ U"
by (rule pr_sesk_passwd)
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show False
by contradiction
next
fix evsC5 S A U n run s a b c f g X and m :: nat
assume "(evsC5, S, A, U) ∈ protocol"
moreover assume "0 < m"
hence "User m ≠ Spy"
by simp
moreover assume
"NonceS (S (User m, n, run)) = Some s" and
"IntMapK (S (User m, n, run)) = Some a" and
"ExtMapK (S (User m, n, run)) = Some b" and
"IntAgrK (S (User m, n, run)) = Some c" and
"ExtAgrK (S (User m, n, run)) = Some f" and
"Says n run 4 X (User m) (Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄)
∈ set evsC5"
ultimately show "Key (sesK (c * f)) ∉ A"
by (rule pr_key_secrecy_aux)
qed
theorem pr_passwd_secrecy [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
User m ≠ Spy ⟶
Passwd m ∉ analz (A ∪ spies evs)"
proof (erule protocol.induct, rule_tac [!] impI, simp_all add: analz_simp_insert_2,
rule contra_subsetD [OF analz_parts_subset], subst parts_simp, simp, blast+,
rule_tac [3] impI)
fix evsR1 S A U n s
assume
A: "Passwd m ∉ analz (A ∪ spies evsR1)" and
B: "(evsR1, S, A, U) ∈ protocol" and
C: "Pri_AgrK s ∉ U"
show
"(n ∈ bad ⟶ Passwd m ∉ analz (insert (Crypt (symK n) (Pri_AgrK s))
(insert (Pri_AgrK s) (A ∪ spies evsR1)))) ∧
(n ∉ bad ⟶ Passwd m ∉ analz (insert (Crypt (symK n) (Pri_AgrK s))
(A ∪ spies evsR1)))"
(is "(_ ⟶ ?T) ∧ (_ ⟶ ?T')")
proof (rule conjI, rule_tac [!] impI)
assume "n ∈ bad"
hence "Key (invK (symK n)) ∈ analz (A ∪ spies evsR1)"
using B by (simp add: pr_symk_analz invK_symK)
hence "Key (invK (symK n)) ∈ analz (insert (Pri_AgrK s) (A ∪ spies evsR1))"
by (rule rev_subsetD, rule_tac analz_mono, blast)
moreover have "analz (insert (Pri_AgrK s) (A ∪ spies evsR1)) =
insert (Pri_AgrK s) (analz (A ∪ spies evsR1))"
using B and C by (rule pr_pri_agrk_unused)
ultimately show ?T
using A by (simp add: analz_crypt_in)
next
assume "n ∉ bad"
hence "Key (invK (symK n)) ∉ analz (A ∪ spies evsR1)"
using B by (simp add: pr_symk_analz invK_symK)
thus ?T'
using A by (simp add: analz_crypt_out)
qed
next
fix evsFR1 A m' s
assume
A: "Passwd m ∉ analz (A ∪ spies evsFR1)" and
B: "Crypt (symK m') (Pri_AgrK s) ∈ synth (analz (A ∪ spies evsFR1))"
thus "Passwd m ∉ analz (insert (Crypt (symK m') (Pri_AgrK s)) (A ∪ spies evsFR1))"
proof (cases "Key (invK (symK m')) ∈ analz (A ∪ spies evsFR1)",
simp_all add: analz_crypt_in analz_crypt_out)
case True
have "Crypt (symK m') (Pri_AgrK s) ∈ analz (A ∪ spies evsFR1) ∨
Pri_AgrK s ∈ synth (analz (A ∪ spies evsFR1)) ∧
Key (symK m') ∈ analz (A ∪ spies evsFR1)"
(is "?P ∨ ?Q")
using B by (rule synth_crypt)
moreover {
assume ?P
hence "Pri_AgrK s ∈ analz (A ∪ spies evsFR1)"
using True by (rule analz.Decrypt)
}
moreover {
assume ?Q
hence "Pri_AgrK s ∈ synth (analz (A ∪ spies evsFR1))" ..
hence "Pri_AgrK s ∈ analz (A ∪ spies evsFR1)"
by (rule synth_simp_intro, simp)
}
ultimately have "Pri_AgrK s ∈ analz (A ∪ spies evsFR1)" ..
thus "Passwd m ∉ analz (insert (Pri_AgrK s) (A ∪ spies evsFR1))"
using A by (simp add: analz_simp_insert_1)
qed
next
fix evsC2 S A U a
assume
"Passwd m ∉ analz (A ∪ spies evsC2)" and
"(evsC2, S, A, U) ∈ protocol" and
"Pri_AgrK a ∉ U"
thus "Passwd m ∉ analz (insert (Pri_AgrK a) (A ∪ spies evsC2))"
by (subst pr_pri_agrk_unused, simp_all)
next
fix evsC3 S A U c and m' :: nat
assume
"Passwd m ∉ analz (A ∪ spies evsC3)" and
"(evsC3, S, A, U) ∈ protocol" and
"Pri_AgrK c ∉ U"
thus "m' = 0 ⟶ Passwd m ∉ analz (insert (Pri_AgrK c) (A ∪ spies evsC3))"
by (rule_tac impI, subst pr_pri_agrk_unused, simp_all)
next
fix evsR3 S A U s s' a b c d
assume "Passwd m ∉ analz (A ∪ spies evsR3)"
moreover assume
"(evsR3, S, A, U) ∈ protocol" and
"Key (sesK (c * d * (s + a * b))) ∉ U"
(is "Key ?K ∉ _")
hence "analz (insert (Key ?K) (A ∪ spies evsR3)) =
insert (Key ?K) (analz (A ∪ spies evsR3))"
by (rule pr_key_unused)
ultimately show "s' = s ∧ Pri_AgrK c ∈ analz (A ∪ spies evsR3) ⟶
Passwd m ∉ analz (insert (Key ?K) (A ∪ spies evsR3))"
by simp
next
fix evsFR3 S A U s a b c d
assume "Passwd m ∉ analz (A ∪ spies evsFR3)"
moreover assume
"(evsFR3, S, A, U) ∈ protocol" and
"Key (sesK (c * d * (s + a * b))) ∉ U"
(is "Key ?K ∉ _")
hence "analz (insert (Key ?K) (A ∪ spies evsFR3)) =
insert (Key ?K) (analz (A ∪ spies evsFR3))"
by (rule pr_key_unused)
ultimately show "Passwd m ∉ analz (insert (Key ?K) (A ∪ spies evsFR3))"
by simp
next
fix evsC4 A c f
assume "Passwd m ∉ analz (A ∪ spies evsC4)"
thus "Passwd m ∉ analz (insert (Crypt (sesK (c * f)) (pubAK f)) (A ∪ spies evsC4))"
by (cases "Key (invK (sesK (c * f))) ∈ analz (A ∪ spies evsC4)",
simp_all add: analz_crypt_in analz_crypt_out analz_simp_insert_2)
next
fix evsFC4 A s a b d e
assume "Passwd m ∉ analz (A ∪ spies evsFC4)"
thus "Passwd m ∉ analz (insert (Crypt (sesK (d * e)) (pubAK (d * (s + a * b))))
(A ∪ spies evsFC4))"
by (cases "Key (invK (sesK (d * e))) ∈ analz (A ∪ spies evsFC4)",
simp_all add: analz_crypt_in analz_crypt_out analz_simp_insert_2)
next
fix evsR4 S A U n run b d e
let
?A = "A ∪ spies evsR4" and
?H = "Hash (pubAK (priAK n))" and
?M = "⦃pubAK (priAK n), Crypt (priSK CA) (Hash (pubAK (priAK n)))⦄"
assume
A: "Passwd m ∉ analz ?A" and
B: "(evsR4, S, A, U) ∈ protocol" and
C: "IntMapK (S (Card n, n, run)) = Some b"
show "Passwd m ∉ analz (insert (Crypt (sesK (d * e))
⦃pubAK e, Auth_Data (priAK n) b, ?M⦄) ?A)"
proof (cases "Key (invK (sesK (d * e))) ∈ analz ?A",
simp_all add: analz_crypt_in analz_crypt_out analz_mpair analz_simp_insert_2 A)
have "Key (pubSK CA) ∈ analz ?A"
using B by (rule pr_valid_key_analz)
hence D: "analz (insert (Crypt (priSK CA) ?H) ?A) =
{Crypt (priSK CA) ?H, ?H} ∪ analz ?A"
by (simp add: analz_crypt_in analz_simp_insert_2)
have "Pri_AgrK (priAK n) ∉ analz ?A"
using B by (rule pr_auth_key_analz)
hence E: "Pri_AgrK (priAK n) ∉ analz (insert (Crypt (priSK CA) ?H) ?A)"
using D by simp
have "Pri_AgrK b ∉ analz ?A"
using B and C by (rule pr_int_mapk_analz)
hence F: "Pri_AgrK b ∉ analz (insert (Crypt (priSK CA) ?H) ?A)"
using D by simp
show "Passwd m ∉ analz (insert (Auth_Data (priAK n) b) (insert ?M ?A))"
proof ((subst insert_commute, simp add: analz_mpair analz_simp_insert_2)+,
subst analz_auth_data_out [OF E F])
qed (simp add: A D)
qed
next
fix evsFR4 S A U s a b c f g
let
?A = "A ∪ spies evsFR4" and
?H = "Hash (pubAK g)" and
?M = "⦃pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄" and
?M' = "⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄"
assume
A: "Passwd m ∉ analz ?A" and
B: "(evsFR4, S, A, U) ∈ protocol" and
C: "Crypt (sesK (c * f)) ?M' ∈ synth (analz ?A)"
have D:
"Key (invK (sesK (c * f))) ∈ analz ?A ⟶
Pri_AgrK b ∈ analz ?A ∨ Pri_AgrK g ∈ analz ?A ⟶
Pri_AgrK b ∈ analz ?A ∧ Pri_AgrK g ∈ analz ?A"
(is "?P ⟶ ?Q ⟶ ?R")
proof (rule impI)+
assume ?P and ?Q
have "Crypt (sesK (c * f)) ?M' ∈ analz ?A ∨
?M' ∈ synth (analz ?A) ∧ Key (sesK (c * f)) ∈ analz ?A"
using C by (rule synth_crypt)
moreover {
assume "Crypt (sesK (c * f)) ?M' ∈ analz ?A"
hence "?M' ∈ analz ?A"
using ‹?P› by (rule analz.Decrypt)
hence "⦃Auth_Data g b, pubAK g, Crypt (priSK CA) (Hash (pubAK g))⦄
∈ analz ?A"
by (rule analz.Snd)
hence E: "Auth_Data g b ∈ analz ?A"
by (rule analz.Fst)
have ?R
proof (rule disjE [OF ‹?Q›])
assume "Pri_AgrK b ∈ analz ?A"
moreover from this have "Pri_AgrK g ∈ analz ?A"
by (rule analz.Auth_Fst [OF E])
ultimately show ?R ..
next
assume "Pri_AgrK g ∈ analz ?A"
moreover from this have "Pri_AgrK b ∈ analz ?A"
by (rule analz.Auth_Snd [OF E])
ultimately show ?R
by simp
qed
}
moreover {
assume "?M' ∈ synth (analz ?A) ∧
Key (sesK (c * f)) ∈ analz ?A"
hence "?M' ∈ synth (analz ?A)" ..
hence "⦃Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄ ∈ synth (analz ?A)"
by (rule synth_analz_snd)
hence "Auth_Data g b ∈ synth (analz ?A)"
by (rule synth_analz_fst)
hence "Auth_Data g b ∈ analz ?A ∨
Pri_AgrK g ∈ analz ?A ∧ Pri_AgrK b ∈ analz ?A"
by (rule synth_auth_data)
moreover {
assume E: "Auth_Data g b ∈ analz ?A"
have ?R
proof (rule disjE [OF ‹?Q›])
assume "Pri_AgrK b ∈ analz ?A"
moreover from this have "Pri_AgrK g ∈ analz ?A"
by (rule analz.Auth_Fst [OF E])
ultimately show ?R ..
next
assume "Pri_AgrK g ∈ analz ?A"
moreover from this have "Pri_AgrK b ∈ analz ?A"
by (rule analz.Auth_Snd [OF E])
ultimately show ?R
by simp
qed
}
moreover {
assume "Pri_AgrK g ∈ analz ?A ∧ Pri_AgrK b ∈ analz ?A"
hence ?R
by simp
}
ultimately have ?R ..
}
ultimately show ?R ..
qed
show "Passwd m ∉ analz (insert (Crypt (sesK (c * f)) ?M') ?A)"
proof (cases "Key (invK (sesK (c * f))) ∈ analz ?A",
simp_all add: analz_crypt_in analz_crypt_out analz_mpair analz_simp_insert_2 A)
assume E: "Key (invK (sesK (c * f))) ∈ analz ?A"
have "Key (pubSK CA) ∈ analz ?A"
using B by (rule pr_valid_key_analz)
hence F: "analz (insert (Crypt (priSK CA) ?H) ?A) =
{Crypt (priSK CA) ?H, ?H} ∪ analz ?A"
by (simp add: analz_crypt_in analz_simp_insert_2)
show "Passwd m ∉ analz (insert (Auth_Data g b) (insert ?M ?A))"
proof (cases "Pri_AgrK g ∈ analz ?A ∨ Pri_AgrK b ∈ analz ?A", simp_all)
assume G: "Pri_AgrK g ∈ analz ?A ∨ Pri_AgrK b ∈ analz ?A"
hence H: "Pri_AgrK g ∈ analz (insert (Crypt (priSK CA) ?H) ?A) ∨
Pri_AgrK b ∈ analz (insert (Crypt (priSK CA) ?H) ?A)"
using F by simp
have I: "Pri_AgrK b ∈ analz ?A ∧ Pri_AgrK g ∈ analz ?A"
using D and E and G by blast
hence "Pri_AgrK g ∈ analz (insert (Crypt (priSK CA) ?H) ?A)"
using F by simp
hence J: "Pri_AgrK g ∈ analz (insert (Pri_AgrK b)
(insert (Crypt (priSK CA) ?H) ?A))"
by (rule rev_subsetD, rule_tac analz_mono, blast)
have K: "Pri_AgrK b ∈ analz (insert (Crypt (priSK CA) ?H) ?A)"
using F and I by simp
show ?thesis
proof ((subst insert_commute, simp add: analz_mpair analz_simp_insert_2)+,
subst analz_auth_data_in [OF H], simp del: Un_insert_right,
subst analz_simp_insert_1 [OF J], subst analz_simp_insert_1 [OF K])
qed (simp add: A F)
next
assume G: "Pri_AgrK g ∉ analz ?A ∧ Pri_AgrK b ∉ analz ?A"
hence H: "Pri_AgrK g ∉ analz (insert (Crypt (priSK CA) ?H) ?A)"
using F by simp
have I: "Pri_AgrK b ∉ analz (insert (Crypt (priSK CA) ?H) ?A)"
using F and G by simp
show ?thesis
proof ((subst insert_commute, simp add: analz_mpair analz_simp_insert_2)+,
subst analz_auth_data_out [OF H I])
qed (simp add: A F)
qed
qed
next
fix evsC5 S A U m' n run s a b c f g X
let ?M = "⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄"
assume
A: "Passwd m ∉ analz (A ∪ spies evsC5)" and
B: "0 < m" and
C: "(evsC5, S, A, U) ∈ protocol" and
D: "NonceS (S (User m', n, run)) = Some s" and
E: "IntMapK (S (User m', n, run)) = Some a" and
F: "ExtMapK (S (User m', n, run)) = Some b" and
G: "IntAgrK (S (User m', n, run)) = Some c" and
H: "ExtAgrK (S (User m', n, run)) = Some f" and
I: "Says n run 4 X (User m') (Crypt (sesK (c * f)) ?M) ∈ set evsC5"
from A show "Passwd m ∉ analz (insert (Crypt (sesK (c * f)) (Passwd m'))
(A ∪ spies evsC5))"
proof (cases "Key (invK (sesK (c * f))) ∈ analz (A ∪ spies evsC5)",
simp_all add: analz_crypt_in analz_crypt_out analz_simp_insert_2, rule_tac notI)
case True
moreover assume "m = m'"
hence "User m' ≠ Spy"
using B by simp
hence "Key (sesK (c * f)) ∉ A"
by (rule pr_key_secrecy_aux [OF C _ D E F G H I])
hence "Key (invK (sesK (c * f))) ∉ analz (A ∪ spies evsC5)"
using C by (simp add: pr_key_analz invK_sesK)
ultimately show False
by contradiction
qed
next
fix evsFC5 A n d e
assume
A: "Passwd m ∉ analz (A ∪ spies evsFC5)" and
B: "Crypt (sesK (d * e)) (Passwd n) ∈ synth (analz (A ∪ spies evsFC5))"
from A show "Passwd m ∉ analz (insert (Crypt (sesK (d * e)) (Passwd n))
(A ∪ spies evsFC5))"
proof (cases "Key (invK (sesK (d * e))) ∈ analz (A ∪ spies evsFC5)",
simp_all add: analz_crypt_in analz_crypt_out analz_simp_insert_2, rule_tac notI)
case True
have "Crypt (sesK (d * e)) (Passwd n) ∈ analz (A ∪ spies evsFC5) ∨
Passwd n ∈ synth (analz (A ∪ spies evsFC5)) ∧
Key (sesK (d * e)) ∈ analz (A ∪ spies evsFC5)"
(is "?P ∨ ?Q")
using B by (rule synth_crypt)
moreover {
assume ?P
hence "Passwd n ∈ analz (A ∪ spies evsFC5)"
using True by (rule analz.Decrypt)
}
moreover {
assume ?Q
hence "Passwd n ∈ synth (analz (A ∪ spies evsFC5))" ..
hence "Passwd n ∈ analz (A ∪ spies evsFC5)"
by (rule synth_simp_intro, simp)
}
ultimately have "Passwd n ∈ analz (A ∪ spies evsFC5)" ..
moreover assume "m = n"
hence "Passwd n ∉ analz (A ∪ spies evsFC5)"
using A by simp
ultimately show False
by contradiction
qed
next
fix evsR5 A d e
assume "Passwd m ∉ analz (A ∪ spies evsR5)"
thus "Passwd m ∉ analz (insert (Crypt (sesK (d * e)) (Number 0)) (A ∪ spies evsR5))"
by (cases "Key (invK (sesK (d * e))) ∈ analz (A ∪ spies evsR5)",
simp_all add: analz_crypt_in analz_crypt_out analz_simp_insert_2)
next
fix evsFR5 A c f
assume "Passwd m ∉ analz (A ∪ spies evsFR5)"
thus "Passwd m ∉ analz (insert (Crypt (sesK (c * f)) (Number 0)) (A ∪ spies evsFR5))"
by (cases "Key (invK (sesK (c * f))) ∈ analz (A ∪ spies evsFR5)",
simp_all add: analz_crypt_in analz_crypt_out analz_simp_insert_2)
qed
subsection "Authenticity theorems"
text ‹
This section contains a series of lemmas culminating in the authenticity theorems
‹pr_user_authenticity› and ‹pr_card_authenticity›. Structured Isar proofs are used.
\null
›
lemma pr_passwd_parts [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Crypt (sesK K) (Passwd m) ∈ parts (A ∪ spies evs) ⟶
(∃n run. Says n run 5 (User m) (Card n) (Crypt (sesK K) (Passwd m)) ∈ set evs) ∨
(∃run. Says m run 5 Spy (Card m) (Crypt (sesK K) (Passwd m)) ∈ set evs)"
(is "_ ⟹ ?M ∈ _ ⟶ ?P evs ∨ ?Q evs")
proof (erule protocol.induct, subst parts_simp, (simp, blast)+)
qed (simp_all add: parts_simp_insert parts_auth_data parts_crypt parts_mpair, blast+)
lemma pr_unique_run_1 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
⦃Key (sesK (d * e)), Agent (User m), Number n', Number run'⦄ ∈ U ⟶
IntAgrK (S (Card n, n, run)) = Some d ⟶
ExtAgrK (S (Card n, n, run)) = Some e ⟶
n' = n ∧ run' = run"
proof (erule protocol.induct, simp_all, rule_tac [3] conjI, (rule_tac [1-4] impI)+,
(rule_tac [5] impI)+, simp_all, (erule_tac [2-3] conjE)+, (rule_tac [!] ccontr))
fix evsR3 S A U s' a b c
assume "c * (s' + a * b) = e"
hence A: "d * e = c * d * (s' + a * b)"
by simp
assume
"(evsR3, S, A, U) ∈ protocol" and
"⦃Key (sesK (d * e)), Agent (User m), Number n', Number run'⦄ ∈ U"
hence "Key (sesK (d * e)) ∈ U"
by (rule pr_sesk_user_2)
hence "Key (sesK (c * d * (s' + a * b))) ∈ U"
by (simp only: A)
moreover assume "Key (sesK (c * d * (s' + a * b))) ∉ U"
ultimately show False
by contradiction
next
fix evsR3 S A U s a b c d'
assume "Key (sesK (c * d' * (s + a * b))) ∉ U"
moreover assume "sesK (d * e) = sesK (c * d' * (s + a * b))"
with sesK_inj have "d * e = c * d' * (s + a * b)"
by (rule injD)
ultimately have "Key (sesK (d * e)) ∉ U"
by simp
moreover assume
"(evsR3, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some e"
hence "Key (sesK (d * e)) ∈ U"
by (rule pr_sesk_card)
ultimately show False
by contradiction
next
fix evsFR3 S A U s a b c d'
assume "Key (sesK (c * d' * (s + a * b))) ∉ U"
moreover assume "sesK (d * e) = sesK (c * d' * (s + a * b))"
with sesK_inj have "d * e = c * d' * (s + a * b)"
by (rule injD)
ultimately have "Key (sesK (d * e)) ∉ U"
by simp
moreover assume
"(evsFR3, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some e"
hence "Key (sesK (d * e)) ∈ U"
by (rule pr_sesk_card)
ultimately show False
by contradiction
qed
lemma pr_unique_run_2:
"(evs, S, A, U) ∈ protocol ⟹
IntAgrK (S (User m, n', run')) = Some c ⟹
ExtAgrK (S (User m, n', run')) = Some f ⟹
IntAgrK (S (Card n, n, run)) = Some d ⟹
ExtAgrK (S (Card n, n, run)) = Some e ⟹
d * e = c * f ⟹
n' = n ∧ run' = run"
proof (frule pr_sesk_user_1, assumption+, drule sym [of "d * e"], simp)
qed (rule pr_unique_run_1)
lemma pr_unique_run_3 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
IntAgrK (S (Card n', n', run')) = Some d' ⟶
ExtAgrK (S (Card n', n', run')) = Some e' ⟶
IntAgrK (S (Card n, n, run)) = Some d ⟶
ExtAgrK (S (Card n, n, run)) = Some e ⟶
d * e = d' * e' ⟶
n' = n ∧ run' = run"
proof (erule protocol.induct, simp_all, rule_tac [!] conjI, (rule_tac [!] impI)+,
simp_all, rule_tac [!] ccontr)
fix evsR3 S A U n' run' s' a b c
assume "c * (s' + a * b) = e"
hence A: "d * e = c * d * (s' + a * b)"
by simp
assume
"(evsR3, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n', n', run')) = Some d'" and
"ExtAgrK (S (Card n', n', run')) = Some e'"
hence "Key (sesK (d' * e')) ∈ U"
by (rule pr_sesk_card)
moreover assume "d * e = d' * e'"
ultimately have "Key (sesK (c * d * (s' + a * b))) ∈ U"
using A by simp
moreover assume "Key (sesK (c * d * (s' + a * b))) ∉ U"
ultimately show False
by contradiction
next
fix evsR3 S A U s' a b c
assume "c * (s' + a * b) = e'"
hence A: "d' * e' = c * d' * (s' + a * b)"
by simp
assume
"(evsR3, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some e"
hence "Key (sesK (d * e)) ∈ U"
by (rule pr_sesk_card)
moreover assume "d * e = d' * e'"
ultimately have "Key (sesK (c * d' * (s' + a * b))) ∈ U"
using A by simp
moreover assume "Key (sesK (c * d' * (s' + a * b))) ∉ U"
ultimately show False
by contradiction
qed
lemma pr_unique_run_4 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Says n' run' 5 X (Card n') (Crypt (sesK (d * e)) (Passwd m)) ∈ set evs ⟶
IntAgrK (S (Card n, n, run)) = Some d ⟶
ExtAgrK (S (Card n, n, run)) = Some e ⟶
n' = n ∧ run' = run"
using [[simproc del: defined_all]]
proof (erule protocol.induct, simp_all, (rule_tac [!] impI)+, rule_tac [1-3] impI,
simp_all, (erule_tac [2-3] conjE)+)
fix evsR3 S A U n run s' a b c
assume "c * (s' + a * b) = e"
hence A: "d * e = c * d * (s' + a * b)"
by simp
assume
"(evsR3, S, A, U) ∈ protocol" and
"Says n' run' 5 X (Card n') (Crypt (sesK (d * e)) (Passwd m)) ∈ set evsR3"
hence "Key (sesK (d * e)) ∈ U"
by (rule pr_sesk_passwd)
hence "Key (sesK (c * d * (s' + a * b))) ∈ U"
by (simp only: A)
moreover assume "Key (sesK (c * d * (s' + a * b))) ∉ U"
ultimately show "n' = n ∧ run' = run"
by contradiction
next
fix evsC5 S A U m n' run' c f
assume
"(evsC5, S, A, U) ∈ protocol" and
"IntAgrK (S (User m, n', run')) = Some c" and
"ExtAgrK (S (User m, n', run')) = Some f" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some e"
moreover assume "sesK (d * e) = sesK (c * f)"
with sesK_inj have "d * e = c * f"
by (rule injD)
ultimately show "n' = n ∧ run' = run"
by (rule pr_unique_run_2)
next
fix evsFC5 S A U n' run' d' e'
assume
"(evsFC5, S, A, U) ∈ protocol" and
"IntAgrK (S (Card n', n', run')) = Some d'" and
"ExtAgrK (S (Card n', n', run')) = Some e'" and
"IntAgrK (S (Card n, n, run)) = Some d" and
"ExtAgrK (S (Card n, n, run)) = Some e"
moreover assume "sesK (d * e) = sesK (d' * e')"
with sesK_inj have "d * e = d' * e'"
by (rule injD)
ultimately show "n' = n ∧ run' = run"
by (rule pr_unique_run_3)
qed
theorem pr_user_authenticity [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Says n run 5 X (Card n) (Crypt (sesK K) (Passwd m)) ∈ set evs ⟶
Says n run 5 (User m) (Card n) (Crypt (sesK K) (Passwd m)) ∈ set evs"
proof (erule protocol.induct, simp_all, rule impI, simp)
fix evsFC5 S A U n run d e
assume
A: "Says n run 5 Spy (Card n) (Crypt (sesK (d * e)) (Passwd n)) ∈ set evsFC5 ⟶
Says n run 5 (User n) (Card n) (Crypt (sesK (d * e)) (Passwd n)) ∈ set evsFC5"
(is "_ ⟶ ?T") and
B: "(evsFC5, S, A, U) ∈ protocol" and
C: "IntAgrK (S (Card n, n, run)) = Some d" and
D: "ExtAgrK (S (Card n, n, run)) = Some e" and
E: "Crypt (sesK (d * e)) (Passwd n) ∈ synth (analz (A ∪ spies evsFC5))"
show "n = 0 ∨ ?T"
proof (cases "n = 0", simp_all)
assume "0 < n"
hence "User n ≠ Spy"
by simp
with B have F: "Passwd n ∉ analz (A ∪ spies evsFC5)"
by (rule pr_passwd_secrecy)
have "Crypt (sesK (d * e)) (Passwd n) ∈ analz (A ∪ spies evsFC5) ∨
Passwd n ∈ synth (analz (A ∪ spies evsFC5)) ∧
Key (sesK (d * e)) ∈ analz (A ∪ spies evsFC5)"
(is "?P ∨ ?Q")
using E by (rule synth_crypt)
moreover have "¬ ?Q"
proof
assume ?Q
hence "Passwd n ∈ synth (analz (A ∪ spies evsFC5))" ..
hence "Passwd n ∈ analz (A ∪ spies evsFC5)"
by (rule synth_simp_intro, simp)
thus False
using F by contradiction
qed
ultimately have ?P
by simp
hence "Crypt (sesK (d * e)) (Passwd n) ∈ parts (A ∪ spies evsFC5)"
by (rule subsetD [OF analz_parts_subset])
with B have
"(∃n' run'. Says n' run' 5 (User n) (Card n') (Crypt (sesK (d * e)) (Passwd n))
∈ set evsFC5) ∨
(∃run'. Says n run' 5 Spy (Card n) (Crypt (sesK (d * e)) (Passwd n))
∈ set evsFC5)"
(is "(∃n' run'. ?P n' run') ∨ (∃run'. ?Q run')")
by (rule pr_passwd_parts)
moreover {
assume "∃n' run'. ?P n' run'"
then obtain n' and run' where "?P n' run'"
by blast
moreover from this have "n' = n ∧ run' = run"
by (rule pr_unique_run_4 [OF B _ C D])
ultimately have ?T
by simp
}
moreover {
assume "∃run'. ?Q run'"
then obtain run' where "?Q run'" ..
moreover from this have "n = n ∧ run' = run"
by (rule pr_unique_run_4 [OF B _ C D])
ultimately have "?Q run"
by simp
with A have ?T ..
}
ultimately show ?T ..
qed
qed
lemma pr_confirm_parts [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Crypt (sesK K) (Number 0) ∈ parts (A ∪ spies evs) ⟶
Key (sesK K) ∉ A ⟶
(∃n run X.
Says n run 5 X (Card n) (Crypt (sesK K) (Passwd n)) ∈ set evs ∧
Says n run 5 (Card n) X (Crypt (sesK K) (Number 0)) ∈ set evs)"
(is "_ ⟹ _ ⟶ _ ⟶ ?P K evs")
using [[simproc del: defined_all]]
proof (erule protocol.induct, simp, subst parts_simp, simp, blast+,
simp_all add: parts_simp_insert parts_auth_data parts_crypt parts_mpair,
rule_tac [3] conjI, (rule_tac [!] impI)+, simp_all, blast+)
fix evsFR5 S A U c f
assume
A: "Crypt (sesK (c * f)) (Number 0) ∈ parts (A ∪ spies evsFR5) ⟶
?P (c * f) evsFR5" and
B: "(evsFR5, S, A, U) ∈ protocol" and
C: "Key (sesK (c * f)) ∉ A" and
D: "Crypt (sesK (c * f)) (Number 0) ∈ synth (analz (A ∪ spies evsFR5))"
show "?P (c * f) evsFR5"
proof -
have "Crypt (sesK (c * f)) (Number 0) ∈ analz (A ∪ spies evsFR5) ∨
Number 0 ∈ synth (analz (A ∪ spies evsFR5)) ∧
Key (sesK (c * f)) ∈ analz (A ∪ spies evsFR5)"
using D by (rule synth_crypt)
moreover have "Key (sesK (c * f)) ∉ analz (A ∪ spies evsFR5)"
using B and C by (simp add: pr_key_analz)
ultimately have "Crypt (sesK (c * f)) (Number 0) ∈ analz (A ∪ spies evsFR5)"
by simp
hence "Crypt (sesK (c * f)) (Number 0) ∈ parts (A ∪ spies evsFR5)"
by (rule subsetD [OF analz_parts_subset])
with A show ?thesis ..
qed
qed
lemma pr_confirm_says [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Says n run 5 X Spy (Crypt (sesK K) (Number 0)) ∈ set evs ⟶
Says n run 5 Spy (Card n) (Crypt (sesK K) (Passwd n)) ∈ set evs"
by (erule protocol.induct, simp_all)
lemma pr_passwd_says [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Says n run 5 X (Card n) (Crypt (sesK K) (Passwd m)) ∈ set evs ⟶
X = User m ∨ X = Spy"
by (erule protocol.induct, simp_all)
lemma pr_unique_run_5 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
⦃Key (sesK K), Agent (User m'), Number n', Number run'⦄ ∈ U ⟶
⦃Key (sesK K), Agent (User m), Number n, Number run⦄ ∈ U ⟶
m = m' ∧ n = n' ∧ run = run'"
using [[simproc del: defined_all]]
proof (erule protocol.induct, simp_all, blast, (rule conjI, rule impI)+,
rule_tac [2] impI, (rule_tac [3] impI)+, rule_tac [4] conjI, (rule_tac [4-5] impI)+,
simp_all, blast, rule_tac [!] ccontr)
fix evsR3 S A U s a b c d
assume
"(evsR3, S, A, U) ∈ protocol" and
"⦃Key (sesK (c * d * (s + a * b))), Agent (User m), Number n, Number run⦄ ∈ U"
hence "Key (sesK (c * d * (s + a * b))) ∈ U"
by (rule pr_sesk_user_2)
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show False
by contradiction
next
fix evsR3 S A U s a b c d
assume
"(evsR3, S, A, U) ∈ protocol" and
"⦃Key (sesK (c * d * (s + a * b))), Agent (User m'), Number n', Number run'⦄ ∈ U"
hence "Key (sesK (c * d * (s + a * b))) ∈ U"
by (rule pr_sesk_user_2)
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show False
by contradiction
next
fix evsFR3 S A U s a b c d
assume
"(evsFR3, S, A, U) ∈ protocol" and
"⦃Key (sesK (c * d * (s + a * b))), Agent (User m), Number n, Number run⦄ ∈ U"
hence "Key (sesK (c * d * (s + a * b))) ∈ U"
by (rule pr_sesk_user_2)
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show False
by contradiction
next
fix evsFR3 S A U s a b c d
assume
"(evsFR3, S, A, U) ∈ protocol" and
"⦃Key (sesK (c * d * (s + a * b))), Agent (User m'), Number n', Number run'⦄ ∈ U"
hence "Key (sesK (c * d * (s + a * b))) ∈ U"
by (rule pr_sesk_user_2)
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show False
by contradiction
qed
lemma pr_unique_run_6:
"(evs, S, A, U) ∈ protocol ⟹
⦃Key (sesK (c * f)), Agent (User m'), Number n', Number run'⦄ ∈ U ⟹
IntAgrK (S (User m, n, run)) = Some c ⟹
ExtAgrK (S (User m, n, run)) = Some f ⟹
m = m' ∧ n = n' ∧ run = run'"
proof (frule pr_sesk_user_1, assumption+)
qed (rule pr_unique_run_5)
lemma pr_unique_run_7 [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Says n' run' 5 (User m') (Card n') (Crypt (sesK K) (Passwd m')) ∈ set evs ⟶
⦃Key (sesK K), Agent (User m), Number n, Number run⦄ ∈ U ⟶
Key (sesK K) ∉ A ⟶
m' = m ∧ n' = n ∧ run' = run"
proof (erule protocol.induct, simp_all, (rule impI)+, (rule_tac [2-3] impI)+,
(erule_tac [3] conjE)+, (drule_tac [3] sym [of m'])+, drule_tac [3] sym [of 0],
simp_all)
fix evsR3 S A U n run s a b c d
assume
"(evsR3, S, A, U) ∈ protocol" and
"Says n' run' 5 (User m') (Card n')
(Crypt (sesK (c * d * (s + a * b))) (Passwd m')) ∈ set evsR3"
hence "Key (sesK (c * d * (s + a * b))) ∈ U"
by (rule pr_sesk_passwd)
moreover assume "Key (sesK (c * d * (s + a * b))) ∉ U"
ultimately show "m' = m ∧ n' = n ∧ run' = run"
by contradiction
next
fix evsC5 S A U m' n' run' c f
assume
"(evsC5, S, A, U) ∈ protocol" and
"⦃Key (sesK (c * f)), Agent (User m), Number n, Number run⦄ ∈ U" and
"IntAgrK (S (User m', n', run')) = Some c" and
"ExtAgrK (S (User m', n', run')) = Some f"
thus "m' = m ∧ n' = n ∧ run' = run"
by (rule pr_unique_run_6)
next
fix evsFC5 S A U run' d e
assume
A: "Says 0 run' 5 Spy (Card 0) (Crypt (sesK (d * e)) (Passwd 0)) ∈ set evsFC5 ⟶
m = 0 ∧ n = 0 ∧ run' = run" and
B: "(evsFC5, S, A, U) ∈ protocol" and
C: "IntAgrK (S (Card 0, 0, run')) = Some d" and
D: "ExtAgrK (S (Card 0, 0, run')) = Some e" and
E: "Crypt (sesK (d * e)) (Passwd 0) ∈ synth (analz (A ∪ spies evsFC5))" and
F: "Key (sesK (d * e)) ∉ A"
have "Crypt (sesK (d * e)) (Passwd 0) ∈ analz (A ∪ spies evsFC5) ∨
Passwd 0 ∈ synth (analz (A ∪ spies evsFC5)) ∧
Key (sesK (d * e)) ∈ analz (A ∪ spies evsFC5)"
using E by (rule synth_crypt)
moreover have "Key (sesK (d * e)) ∉ analz (A ∪ spies evsFC5)"
using B and F by (simp add: pr_key_analz)
ultimately have "Crypt (sesK (d * e)) (Passwd 0) ∈ analz (A ∪ spies evsFC5)"
by simp
hence "Crypt (sesK (d * e)) (Passwd 0) ∈ parts (A ∪ spies evsFC5)"
by (rule subsetD [OF analz_parts_subset])
with B have
"(∃n run. Says n run 5 Spy (Card n) (Crypt (sesK (d * e)) (Passwd 0))
∈ set evsFC5) ∨
(∃run. Says 0 run 5 Spy (Card 0) (Crypt (sesK (d * e)) (Passwd 0))
∈ set evsFC5)"
(is "(∃n run. ?P n run) ∨ (∃run. ?Q run)")
by (rule pr_passwd_parts)
moreover {
assume "∃n run. ?P n run"
then obtain n'' and run'' where "?P n'' run''"
by blast
moreover from this have "n'' = 0 ∧ run'' = run'"
by (rule pr_unique_run_4 [OF B _ C D])
ultimately have "?P 0 run'"
by simp
}
moreover {
assume "∃run. ?Q run"
then obtain run'' where "?Q run''" ..
hence "∃n. ?P n run''" ..
then obtain n'' where "?P n'' run''" ..
moreover from this have "n'' = 0 ∧ run'' = run'"
by (rule pr_unique_run_4 [OF B _ C D])
ultimately have "?P 0 run'"
by simp
}
ultimately have "?P 0 run'" ..
with A show "m = 0 ∧ n = 0 ∧ run' = run" ..
qed
lemma pr_unique_run_8:
"(evs, S, A, U) ∈ protocol ⟹
Says n' run' 5 (User m') (Card n') (Crypt (sesK (c * f)) (Passwd m')) ∈ set evs ⟹
IntAgrK (S (User m, n, run)) = Some c ⟹
ExtAgrK (S (User m, n, run)) = Some f ⟹
Key (sesK (c * f)) ∉ A ⟹
m' = m ∧ n' = n ∧ run' = run"
proof (frule pr_sesk_user_1, assumption+)
qed (rule pr_unique_run_7)
lemma pr_unique_passwd_parts [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Crypt (sesK K) (Passwd m') ∈ parts (A ∪ spies evs) ⟶
Crypt (sesK K) (Passwd m) ∈ parts (A ∪ spies evs) ⟶
m' = m"
using [[simproc del: defined_all]]
proof (erule protocol.induct, simp, subst parts_simp, simp, blast+,
simp_all add: parts_simp_insert parts_auth_data parts_crypt parts_mpair,
rule_tac [!] conjI, (rule_tac [!] impI)+, erule_tac [!] conjE, simp_all)
fix evsC5 S A U m'' n run s a b c f g X
assume
A: "(evsC5, S, A, U) ∈ protocol" and
B: "NonceS (S (User m'', n, run)) = Some s" and
C: "IntMapK (S (User m'', n, run)) = Some a" and
D: "ExtMapK (S (User m'', n, run)) = Some b" and
E: "IntAgrK (S (User m'', n, run)) = Some c" and
F: "ExtAgrK (S (User m'', n, run)) = Some f" and
G: "Crypt (sesK (c * f)) (Passwd m) ∈ parts (A ∪ spies evsC5)" and
H: "m' = m''" and
I: "Says n run 4 X (User m'') (Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄) ∈ set evsC5"
show "m'' = m"
proof (cases "m'' = 0", rule classical)
case True
moreover assume "m'' ≠ m"
ultimately have J: "User m ≠ Spy"
using H by simp
have
"(∃n run. Says n run 5 (User m) (Card n) (Crypt (sesK (c * f)) (Passwd m))
∈ set evsC5) ∨
(∃run. Says m run 5 Spy (Card m) (Crypt (sesK (c * f)) (Passwd m))
∈ set evsC5)"
(is "(∃n run. ?P n run) ∨ (∃run. ?Q run)")
using A and G by (rule pr_passwd_parts)
moreover {
assume "∃n run. ?P n run"
then obtain n' and run' where K: "?P n' run'"
by blast
with A and J have "Key (sesK (c * f)) ∉ analz (A ∪ spies evsC5)"
by (rule pr_key_secrecy)
hence "Key (sesK (c * f)) ∉ A"
using A by (simp add: pr_key_analz)
hence "m = m'' ∧ n' = n ∧ run' = run"
by (rule pr_unique_run_8 [OF A K E F])
hence ?thesis
by simp
}
moreover {
assume "∃run. ?Q run"
then obtain run' where "?Q run'" ..
with A have K: "?P m run'"
by (rule pr_user_authenticity)
with A and J have "Key (sesK (c * f)) ∉ analz (A ∪ spies evsC5)"
by (rule pr_key_secrecy)
hence "Key (sesK (c * f)) ∉ A"
using A by (simp add: pr_key_analz)
hence "m = m'' ∧ m = n ∧ run' = run"
by (rule pr_unique_run_8 [OF A K E F])
hence ?thesis
by simp
}
ultimately show ?thesis ..
next
case False
hence "User m'' ≠ Spy"
by simp
hence J: "Key (sesK (c * f)) ∉ A"
by (rule pr_key_secrecy_aux [OF A _ B C D E F I])
have
"(∃n run. Says n run 5 (User m) (Card n) (Crypt (sesK (c * f)) (Passwd m))
∈ set evsC5) ∨
(∃run. Says m run 5 Spy (Card m) (Crypt (sesK (c * f)) (Passwd m))
∈ set evsC5)"
(is "(∃n run. ?P n run) ∨ (∃run. ?Q run)")
using A and G by (rule pr_passwd_parts)
moreover {
assume "∃n run. ?P n run"
then obtain n' and run' where "?P n' run'"
by blast
hence "m = m'' ∧ n' = n ∧ run' = run"
by (rule pr_unique_run_8 [OF A _ E F J])
hence ?thesis
by simp
}
moreover {
assume "∃run. ?Q run"
then obtain run' where "?Q run'" ..
with A have "?P m run'"
by (rule pr_user_authenticity)
hence "m = m'' ∧ m = n ∧ run' = run"
by (rule pr_unique_run_8 [OF A _ E F J])
hence ?thesis
by simp
}
ultimately show ?thesis ..
qed
next
fix evsC5 S A U m'' n run s a b c f g X
assume
A: "(evsC5, S, A, U) ∈ protocol" and
B: "NonceS (S (User m'', n, run)) = Some s" and
C: "IntMapK (S (User m'', n, run)) = Some a" and
D: "ExtMapK (S (User m'', n, run)) = Some b" and
E: "IntAgrK (S (User m'', n, run)) = Some c" and
F: "ExtAgrK (S (User m'', n, run)) = Some f" and
G: "Crypt (sesK (c * f)) (Passwd m') ∈ parts (A ∪ spies evsC5)" and
H: "m = m''" and
I: "Says n run 4 X (User m'') (Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄) ∈ set evsC5"
show "m' = m''"
proof (cases "m'' = 0", rule classical)
case True
moreover assume "m' ≠ m''"
ultimately have J: "User m' ≠ Spy"
using H by simp
have
"(∃n run. Says n run 5 (User m') (Card n) (Crypt (sesK (c * f)) (Passwd m'))
∈ set evsC5) ∨
(∃run. Says m' run 5 Spy (Card m') (Crypt (sesK (c * f)) (Passwd m'))
∈ set evsC5)"
(is "(∃n run. ?P n run) ∨ (∃run. ?Q run)")
using A and G by (rule pr_passwd_parts)
moreover {
assume "∃n run. ?P n run"
then obtain n' and run' where K: "?P n' run'"
by blast
with A and J have "Key (sesK (c * f)) ∉ analz (A ∪ spies evsC5)"
by (rule pr_key_secrecy)
hence "Key (sesK (c * f)) ∉ A"
using A by (simp add: pr_key_analz)
hence "m' = m'' ∧ n' = n ∧ run' = run"
by (rule pr_unique_run_8 [OF A K E F])
hence ?thesis
by simp
}
moreover {
assume "∃run. ?Q run"
then obtain run' where "?Q run'" ..
with A have K: "?P m' run'"
by (rule pr_user_authenticity)
with A and J have "Key (sesK (c * f)) ∉ analz (A ∪ spies evsC5)"
by (rule pr_key_secrecy)
hence "Key (sesK (c * f)) ∉ A"
using A by (simp add: pr_key_analz)
hence "m' = m'' ∧ m' = n ∧ run' = run"
by (rule pr_unique_run_8 [OF A K E F])
hence ?thesis
by simp
}
ultimately show ?thesis ..
next
case False
hence "User m'' ≠ Spy"
by simp
hence J: "Key (sesK (c * f)) ∉ A"
by (rule pr_key_secrecy_aux [OF A _ B C D E F I])
have
"(∃n run. Says n run 5 (User m') (Card n) (Crypt (sesK (c * f)) (Passwd m'))
∈ set evsC5) ∨
(∃run. Says m' run 5 Spy (Card m') (Crypt (sesK (c * f)) (Passwd m'))
∈ set evsC5)"
(is "(∃n run. ?P n run) ∨ (∃run. ?Q run)")
using A and G by (rule pr_passwd_parts)
moreover {
assume "∃n run. ?P n run"
then obtain n' and run' where "?P n' run'"
by blast
hence "m' = m'' ∧ n' = n ∧ run' = run"
by (rule pr_unique_run_8 [OF A _ E F J])
hence ?thesis
by simp
}
moreover {
assume "∃run. ?Q run"
then obtain run' where "?Q run'" ..
with A have "?P m' run'"
by (rule pr_user_authenticity)
hence "m' = m'' ∧ m' = n ∧ run' = run"
by (rule pr_unique_run_8 [OF A _ E F J])
hence ?thesis
by simp
}
ultimately show ?thesis ..
qed
next
fix evsFC5 S A U n d e
assume
A: "Crypt (sesK (d * e)) (Passwd n) ∈ parts (A ∪ spies evsFC5) ⟶
n = m" and
B: "(evsFC5, S, A, U) ∈ protocol" and
C: "Crypt (sesK (d * e)) (Passwd n) ∈ synth (analz (A ∪ spies evsFC5))" and
D: "Crypt (sesK (d * e)) (Passwd m) ∈ parts (A ∪ spies evsFC5)"
show "n = m"
proof (rule classical)
assume E: "n ≠ m"
have F: "Crypt (sesK (d * e)) (Passwd n) ∈ analz (A ∪ spies evsFC5) ∨
Passwd n ∈ synth (analz (A ∪ spies evsFC5)) ∧
Key (sesK (d * e)) ∈ analz (A ∪ spies evsFC5)"
using C by (rule synth_crypt)
have "Crypt (sesK (d * e)) (Passwd n) ∈ analz (A ∪ spies evsFC5)"
proof (rule disjE [OF F], assumption, erule conjE, cases "n = 0")
case True
hence G: "User m ≠ Spy"
using E by simp
have
"(∃n run. Says n run 5 (User m) (Card n) (Crypt (sesK (d * e)) (Passwd m))
∈ set evsFC5) ∨
(∃run. Says m run 5 Spy (Card m) (Crypt (sesK (d * e)) (Passwd m))
∈ set evsFC5)"
(is "(∃n run. ?P n run) ∨ (∃run. ?Q run)")
using B and D by (rule pr_passwd_parts)
moreover {
assume "∃n run. ?P n run"
then obtain n' and run where "?P n' run"
by blast
with B and G have "Key (sesK (d * e)) ∉ analz (A ∪ spies evsFC5)"
by (rule pr_key_secrecy)
}
moreover {
assume "∃run. ?Q run"
then obtain run where "?Q run" ..
with B have "?P m run"
by (rule pr_user_authenticity)
with B and G have "Key (sesK (d * e)) ∉ analz (A ∪ spies evsFC5)"
by (rule pr_key_secrecy)
}
ultimately have "Key (sesK (d * e)) ∉ analz (A ∪ spies evsFC5)" ..
moreover assume "Key (sesK (d * e)) ∈ analz (A ∪ spies evsFC5)"
ultimately show ?thesis
by contradiction
next
case False
hence "User n ≠ Spy"
by simp
with B have "Passwd n ∉ analz (A ∪ spies evsFC5)"
by (rule pr_passwd_secrecy)
moreover assume "Passwd n ∈ synth (analz (A ∪ spies evsFC5))"
hence "Passwd n ∈ analz (A ∪ spies evsFC5)"
by (rule synth_simp_intro, simp)
ultimately show ?thesis
by contradiction
qed
hence "Crypt (sesK (d * e)) (Passwd n) ∈ parts (A ∪ spies evsFC5)"
by (rule subsetD [OF analz_parts_subset])
with A show ?thesis ..
qed
next
fix evsFC5 S A U n d e
assume
A: "Crypt (sesK (d * e)) (Passwd n) ∈ parts (A ∪ spies evsFC5) ⟶
m' = n" and
B: "(evsFC5, S, A, U) ∈ protocol" and
C: "Crypt (sesK (d * e)) (Passwd n) ∈ synth (analz (A ∪ spies evsFC5))" and
D: "Crypt (sesK (d * e)) (Passwd m') ∈ parts (A ∪ spies evsFC5)"
show "m' = n"
proof (rule classical)
assume E: "m' ≠ n"
have F: "Crypt (sesK (d * e)) (Passwd n) ∈ analz (A ∪ spies evsFC5) ∨
Passwd n ∈ synth (analz (A ∪ spies evsFC5)) ∧
Key (sesK (d * e)) ∈ analz (A ∪ spies evsFC5)"
using C by (rule synth_crypt)
have "Crypt (sesK (d * e)) (Passwd n) ∈ analz (A ∪ spies evsFC5)"
proof (rule disjE [OF F], assumption, erule conjE, cases "n = 0")
case True
hence G: "User m' ≠ Spy"
using E by simp
have
"(∃n run. Says n run 5 (User m') (Card n) (Crypt (sesK (d * e)) (Passwd m'))
∈ set evsFC5) ∨
(∃run. Says m' run 5 Spy (Card m') (Crypt (sesK (d * e)) (Passwd m'))
∈ set evsFC5)"
(is "(∃n run. ?P n run) ∨ (∃run. ?Q run)")
using B and D by (rule pr_passwd_parts)
moreover {
assume "∃n run. ?P n run"
then obtain n' and run where "?P n' run"
by blast
with B and G have "Key (sesK (d * e)) ∉ analz (A ∪ spies evsFC5)"
by (rule pr_key_secrecy)
}
moreover {
assume "∃run. ?Q run"
then obtain run where "?Q run" ..
with B have "?P m' run"
by (rule pr_user_authenticity)
with B and G have "Key (sesK (d * e)) ∉ analz (A ∪ spies evsFC5)"
by (rule pr_key_secrecy)
}
ultimately have "Key (sesK (d * e)) ∉ analz (A ∪ spies evsFC5)" ..
moreover assume "Key (sesK (d * e)) ∈ analz (A ∪ spies evsFC5)"
ultimately show ?thesis
by contradiction
next
case False
hence "User n ≠ Spy"
by simp
with B have "Passwd n ∉ analz (A ∪ spies evsFC5)"
by (rule pr_passwd_secrecy)
moreover assume "Passwd n ∈ synth (analz (A ∪ spies evsFC5))"
hence "Passwd n ∈ analz (A ∪ spies evsFC5)"
by (rule synth_simp_intro, simp)
ultimately show ?thesis
by contradiction
qed
hence "Crypt (sesK (d * e)) (Passwd n) ∈ parts (A ∪ spies evsFC5)"
by (rule subsetD [OF analz_parts_subset])
with A show ?thesis ..
qed
qed
theorem pr_card_authenticity [rule_format]:
"(evs, S, A, U) ∈ protocol ⟹
Says n run 5 (User m) (Card n) (Crypt (sesK K) (Passwd m)) ∈ set evs ⟶
Says n run 5 X (User m) (Crypt (sesK K) (Number 0)) ∈ set evs ⟶
n = m ∧
(Says m run 5 (Card m) (User m) (Crypt (sesK K) (Number 0)) ∈ set evs ∨
Says m run 5 (Card m) Spy (Crypt (sesK K) (Number 0)) ∈ set evs)"
proof (erule protocol.induct, simp_all, (rule_tac [1-2] impI)+, (erule_tac [2] conjE)+,
(rule_tac [3] impI, rule_tac [3] conjI)+, rule_tac [4] disjI1, rule_tac [5] impI,
(rule_tac [6] impI)+, simp_all)
fix evsC5 S A U m n run s a b c f g X'
assume
A: "Says n run 5 (User m) (Card n) (Crypt (sesK (c * f)) (Passwd m))
∈ set evsC5 ⟶
n = m ∧
(Says m run 5 (Card m) (User m) (Crypt (sesK (c * f)) (Number 0))
∈ set evsC5 ∨
Says m run 5 (Card m) Spy (Crypt (sesK (c * f)) (Number 0))
∈ set evsC5)" and
B: "(evsC5, S, A, U) ∈ protocol" and
C: "NonceS (S (User m, n, run)) = Some s" and
D: "IntMapK (S (User m, n, run)) = Some a" and
E: "ExtMapK (S (User m, n, run)) = Some b" and
F: "IntAgrK (S (User m, n, run)) = Some c" and
G: "ExtAgrK (S (User m, n, run)) = Some f" and
H: "Says n run 4 X' (User m) (Crypt (sesK (c * f))
⦃pubAK (c * (s + a * b)), Auth_Data g b, pubAK g,
Crypt (priSK CA) (Hash (pubAK g))⦄) ∈ set evsC5" and
I: "Says n run 5 X (User m) (Crypt (sesK (c * f)) (Number 0)) ∈ set evsC5"
show "n = m ∧
(Says m run 5 (Card m) (User m) (Crypt (sesK (c * f)) (Number 0)) ∈ set evsC5 ∨
Says m run 5 (Card m) Spy (Crypt (sesK (c * f)) (Number 0)) ∈ set evsC5)"
proof (cases "m = 0")
case True
hence "Says n run 5 X Spy (Crypt (sesK (c * f)) (Number 0)) ∈ set evsC5"
using I by simp
with B have "Says n run 5 Spy (Card n) (Crypt (sesK (c * f)) (Passwd n))
∈ set evsC5"
by (rule pr_confirm_says)
with B have J: "Says n run 5 (User n) (Card n) (Crypt (sesK (c * f)) (Passwd n))
∈ set evsC5"
by (rule pr_user_authenticity)
show ?thesis
proof (cases n)
case 0
hence "Says n run 5 (User m) (Card n) (Crypt (sesK (c * f)) (Passwd m))
∈ set evsC5"
using J and True by simp
with A show ?thesis ..
next
case Suc
hence "User n ≠ Spy"
by simp
with B have "Key (sesK (c * f)) ∉ analz (A ∪ spies evsC5)"
using J by (rule pr_key_secrecy)
hence "Key (sesK (c * f)) ∉ A"
using B by (simp add: pr_key_analz)
hence "n = m ∧ n = n ∧ run = run"
by (rule pr_unique_run_8 [OF B J F G])
hence "Says n run 5 (User m) (Card n) (Crypt (sesK (c * f)) (Passwd m))
∈ set evsC5"
using J by simp
with A show ?thesis ..
qed
next
case False
have "Crypt (sesK (c * f)) (Number 0) ∈ spies evsC5"
using I by (rule set_spies)
hence "Crypt (sesK (c * f)) (Number 0) ∈ A ∪ spies evsC5" ..
hence "Crypt (sesK (c * f)) (Number 0) ∈ parts (A ∪ spies evsC5)"
by (rule parts.Inj)
moreover have "User m ≠ Spy"
using False by simp
hence J: "Key (sesK (c * f)) ∉ A"
by (rule pr_key_secrecy_aux [OF B _ C D E F G H])
ultimately have "∃n run X.
Says n run 5 X (Card n) (Crypt (sesK (c * f)) (Passwd n)) ∈ set evsC5 ∧
Says n run 5 (Card n) X (Crypt (sesK (c * f)) (Number 0)) ∈ set evsC5"
by (rule pr_confirm_parts [OF B])
then obtain n' and run' and X where
"Says n' run' 5 X (Card n') (Crypt (sesK (c * f)) (Passwd n')) ∈ set evsC5"
by blast
with B have
"Says n' run' 5 (User n') (Card n') (Crypt (sesK (c * f)) (Passwd n')) ∈ set evsC5"
by (rule pr_user_authenticity)
moreover from this have "n' = m ∧ n' = n ∧ run' = run"
by (rule pr_unique_run_8 [OF B _ F G J])
ultimately have
"Says n run 5 (User m) (Card n) (Crypt (sesK (c * f)) (Passwd m)) ∈ set evsC5"
by auto
with A show ?thesis ..
qed
next
fix evsFC5 S A U run d e
assume
"Says 0 run 5 Spy (Card 0) (Crypt (sesK (d * e)) (Passwd 0)) ∈ set evsFC5 ⟶
Says 0 run 5 (Card 0) Spy (Crypt (sesK (d * e)) (Number 0)) ∈ set evsFC5"
moreover assume
"(evsFC5, S, A, U) ∈ protocol" and
"Says 0 run 5 X Spy (Crypt (sesK (d * e)) (Number 0)) ∈ set evsFC5"
hence "Says 0 run 5 Spy (Card 0) (Crypt (sesK (d * e)) (Passwd 0)) ∈ set evsFC5"
by (rule pr_confirm_says)
ultimately show
"Says 0 run 5 (Card 0) Spy (Crypt (sesK (d * e)) (Number 0)) ∈ set evsFC5" ..
next
fix evsR5 S A U n run d e X
assume "(evsR5, S, A, U) ∈ protocol"
moreover assume "Says n run 5 X (Card n) (Crypt (sesK (d * e)) (Passwd n))
∈ set evsR5"
hence "Crypt (sesK (d * e)) (Passwd n) ∈ spies evsR5"
by (rule set_spies)
hence "Crypt (sesK (d * e)) (Passwd n) ∈ A ∪ spies evsR5" ..
hence "Crypt (sesK (d * e)) (Passwd n) ∈ parts (A ∪ spies evsR5)"
by (rule parts.Inj)
moreover assume "Says n run 5 X (Card n) (Crypt (sesK (d * e)) (Passwd m))
∈ set evsR5"
hence "Crypt (sesK (d * e)) (Passwd m) ∈ spies evsR5"
by (rule set_spies)
hence "Crypt (sesK (d * e)) (Passwd m) ∈ A ∪ spies evsR5" ..
hence "Crypt (sesK (d * e)) (Passwd m) ∈ parts (A ∪ spies evsR5)"
by (rule parts.Inj)
ultimately show "n = m"
by (rule pr_unique_passwd_parts)
next
fix evsR5 S A U n run d e X
assume "(evsR5, S, A, U) ∈ protocol"
moreover assume "Says n run 5 X (Card n) (Crypt (sesK (d * e)) (Passwd m))
∈ set evsR5"
hence "Crypt (sesK (d * e)) (Passwd m) ∈ spies evsR5"
by (rule set_spies)
hence "Crypt (sesK (d * e)) (Passwd m) ∈ A ∪ spies evsR5" ..
hence "Crypt (sesK (d * e)) (Passwd m) ∈ parts (A ∪ spies evsR5)"
by (rule parts.Inj)
moreover assume "Says n run 5 X (Card n) (Crypt (sesK (d * e)) (Passwd n))
∈ set evsR5"
hence "Crypt (sesK (d * e)) (Passwd n) ∈ spies evsR5"
by (rule set_spies)
hence "Crypt (sesK (d * e)) (Passwd n) ∈ A ∪ spies evsR5" ..
hence "Crypt (sesK (d * e)) (Passwd n) ∈ parts (A ∪ spies evsR5)"
by (rule parts.Inj)
ultimately show "m = n"
by (rule pr_unique_passwd_parts)
next
fix evsR5 n' run' d e X
assume "n = m ∧
(Says m run 5 (Card m) (User m) (Crypt (sesK K) (Number 0)) ∈ set evsR5 ∨
Says m run 5 (Card m) Spy (Crypt (sesK K) (Number 0)) ∈ set evsR5)"
thus
"m = n' ∧ run = run' ∧ m = n' ∧ User m = X ∧ sesK K = sesK (d * e) ∨
Says m run 5 (Card m) (User m) (Crypt (sesK K) (Number 0)) ∈ set evsR5 ∨
m = n' ∧ run = run' ∧ m = n' ∧ Spy = X ∧ sesK K = sesK (d * e) ∨
Says m run 5 (Card m) Spy (Crypt (sesK K) (Number 0)) ∈ set evsR5"
by blast
next
fix evsFR5 S A U m n run c f
assume
A: "(evsFR5, S, A, U) ∈ protocol" and
B: "0 < m" and
C: "IntAgrK (S (User m, n, run)) = Some c" and
D: "ExtAgrK (S (User m, n, run)) = Some f" and
E: "Crypt (sesK (c * f)) (Number 0) ∈ synth (analz (A ∪ spies evsFR5))" and
F: "Says n run 5 (User m) (Card n) (Crypt (sesK (c * f)) (Passwd m)) ∈ set evsFR5"
have "User m ≠ Spy"
using B by simp
with A have G: "Key (sesK (c * f)) ∉ analz (A ∪ spies evsFR5)"
using F by (rule pr_key_secrecy)
moreover have "Crypt (sesK (c * f)) (Number 0) ∈ analz (A ∪ spies evsFR5) ∨
Number 0 ∈ synth (analz (A ∪ spies evsFR5)) ∧
Key (sesK (c * f)) ∈ analz (A ∪ spies evsFR5)"
using E by (rule synth_crypt)
ultimately have "Crypt (sesK (c * f)) (Number 0) ∈ analz (A ∪ spies evsFR5)"
by simp
hence "Crypt (sesK (c * f)) (Number 0) ∈ parts (A ∪ spies evsFR5)"
by (rule subsetD [OF analz_parts_subset])
moreover have H: "Key (sesK (c * f)) ∉ A"
using A and G by (simp add: pr_key_analz)
ultimately have "∃n run X.
Says n run 5 X (Card n) (Crypt (sesK (c * f)) (Passwd n)) ∈ set evsFR5 ∧
Says n run 5 (Card n) X (Crypt (sesK (c * f)) (Number 0)) ∈ set evsFR5"
by (rule pr_confirm_parts [OF A])
then obtain n' and run' and X where I:
"Says n' run' 5 X (Card n') (Crypt (sesK (c * f)) (Passwd n')) ∈ set evsFR5 ∧
Says n' run' 5 (Card n') X (Crypt (sesK (c * f)) (Number 0)) ∈ set evsFR5"
by blast
hence
"Says n' run' 5 X (Card n') (Crypt (sesK (c * f)) (Passwd n')) ∈ set evsFR5" ..
with A have J:
"Says n' run' 5 (User n') (Card n') (Crypt (sesK (c * f)) (Passwd n'))
∈ set evsFR5"
by (rule pr_user_authenticity)
hence "Crypt (sesK (c * f)) (Passwd n') ∈ spies evsFR5"
by (rule set_spies)
hence "Crypt (sesK (c * f)) (Passwd n') ∈ A ∪ spies evsFR5" ..
hence "Crypt (sesK (c * f)) (Passwd n') ∈ parts (A ∪ spies evsFR5)"
by (rule parts.Inj)
moreover have "Crypt (sesK (c * f)) (Passwd m) ∈ spies evsFR5"
using F by (rule set_spies)
hence "Crypt (sesK (c * f)) (Passwd m) ∈ A ∪ spies evsFR5" ..
hence "Crypt (sesK (c * f)) (Passwd m) ∈ parts (A ∪ spies evsFR5)"
by (rule parts.Inj)
ultimately have "n' = m"
by (rule pr_unique_passwd_parts [OF A])
moreover from this have
"Says m run' 5 (User m) (Card m) (Crypt (sesK (c * f)) (Passwd m))
∈ set evsFR5"
using J by simp
hence "m = m ∧ m = n ∧ run' = run"
by (rule pr_unique_run_8 [OF A _ C D H])
hence K: "n = m ∧ run' = run"
by simp
ultimately have L:
"Says m run 5 X (Card m) (Crypt (sesK (c * f)) (Passwd m)) ∈ set evsFR5 ∧
Says m run 5 (Card m) X (Crypt (sesK (c * f)) (Number 0)) ∈ set evsFR5"
using I by simp
moreover from this have
"Says m run 5 X (Card m) (Crypt (sesK (c * f)) (Passwd m)) ∈ set evsFR5" ..
with A have "X = User m ∨ X = Spy"
by (rule pr_passwd_says)
thus "n = m ∧
(Says m run 5 (Card m) (User m) (Crypt (sesK (c * f)) (Number 0)) ∈ set evsFR5 ∨
Says m run 5 (Card m) Spy (Crypt (sesK (c * f)) (Number 0)) ∈ set evsFR5)"
by (rule disjE, insert L, simp_all add: K)
qed
end