Theory Protocol

(*  Title:       Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method
    Author:      Pasquale Noce
                 Security Certification Specialist at Arjo Systems, Italy
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at arjosystems dot com
*)

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)) (