src/HOL/Auth/NS_Shared.thy
changeset 13926 6e62e5357a10
parent 13507 febb8e5d2a9d
child 13935 4822d9597d1e
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Sat Apr 26 12:38:17 2003 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Sat Apr 26 12:38:42 2003 +0200
     1.3 @@ -16,60 +16,60 @@
     1.4  inductive "ns_shared"
     1.5   intros
     1.6  	(*Initial trace is empty*)
     1.7 -  Nil:  "[] \\<in> ns_shared"
     1.8 +  Nil:  "[] \<in> ns_shared"
     1.9  	(*The spy MAY say anything he CAN say.  We do not expect him to
    1.10  	  invent new nonces here, but he can also use NS1.  Common to
    1.11  	  all similar protocols.*)
    1.12 -  Fake: "\\<lbrakk>evsf \\<in> ns_shared;  X \\<in> synth (analz (spies evsf))\\<rbrakk>
    1.13 -	 \\<Longrightarrow> Says Spy B X # evsf \\<in> ns_shared"
    1.14 +  Fake: "\<lbrakk>evsf \<in> ns_shared;  X \<in> synth (analz (spies evsf))\<rbrakk>
    1.15 +	 \<Longrightarrow> Says Spy B X # evsf \<in> ns_shared"
    1.16  
    1.17  	(*Alice initiates a protocol run, requesting to talk to any B*)
    1.18 -  NS1:  "\\<lbrakk>evs1 \\<in> ns_shared;  Nonce NA \\<notin> used evs1\\<rbrakk>
    1.19 -	 \\<Longrightarrow> Says A Server \\<lbrace>Agent A, Agent B, Nonce NA\\<rbrace> # evs1  \\<in>  ns_shared"
    1.20 +  NS1:  "\<lbrakk>evs1 \<in> ns_shared;  Nonce NA \<notin> used evs1\<rbrakk>
    1.21 +	 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1  \<in>  ns_shared"
    1.22  
    1.23  	(*Server's response to Alice's message.
    1.24  	  !! It may respond more than once to A's request !!
    1.25  	  Server doesn't know who the true sender is, hence the A' in
    1.26  	      the sender field.*)
    1.27 -  NS2:  "\\<lbrakk>evs2 \\<in> ns_shared;  Key KAB \\<notin> used evs2;
    1.28 -	  Says A' Server \\<lbrace>Agent A, Agent B, Nonce NA\\<rbrace> \\<in> set evs2\\<rbrakk>
    1.29 -	 \\<Longrightarrow> Says Server A
    1.30 +  NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;
    1.31 +	  Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
    1.32 +	 \<Longrightarrow> Says Server A
    1.33  	       (Crypt (shrK A)
    1.34 -		  \\<lbrace>Nonce NA, Agent B, Key KAB,
    1.35 -		    (Crypt (shrK B) \\<lbrace>Key KAB, Agent A\\<rbrace>)\\<rbrace>)
    1.36 -	       # evs2 \\<in> ns_shared"
    1.37 +		  \<lbrace>Nonce NA, Agent B, Key KAB,
    1.38 +		    (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>)
    1.39 +	       # evs2 \<in> ns_shared"
    1.40  
    1.41  	 (*We can't assume S=Server.  Agent A "remembers" her nonce.
    1.42 -	   Need A \\<noteq> Server because we allow messages to self.*)
    1.43 -  NS3:  "\\<lbrakk>evs3 \\<in> ns_shared;  A \\<noteq> Server;
    1.44 -	  Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs3;
    1.45 -	  Says A Server \\<lbrace>Agent A, Agent B, Nonce NA\\<rbrace> \\<in> set evs3\\<rbrakk>
    1.46 -	 \\<Longrightarrow> Says A B X # evs3 \\<in> ns_shared"
    1.47 +	   Need A \<noteq> Server because we allow messages to self.*)
    1.48 +  NS3:  "\<lbrakk>evs3 \<in> ns_shared;  A \<noteq> Server;
    1.49 +	  Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3;
    1.50 +	  Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk>
    1.51 +	 \<Longrightarrow> Says A B X # evs3 \<in> ns_shared"
    1.52  
    1.53  	(*Bob's nonce exchange.  He does not know who the message came
    1.54  	  from, but responds to A because she is mentioned inside.*)
    1.55 -  NS4:  "\\<lbrakk>evs4 \\<in> ns_shared;  Nonce NB \\<notin> used evs4;
    1.56 -	  Says A' B (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>) \\<in> set evs4\\<rbrakk>
    1.57 -	 \\<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \\<in> ns_shared"
    1.58 +  NS4:  "\<lbrakk>evs4 \<in> ns_shared;  Nonce NB \<notin> used evs4;
    1.59 +	  Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
    1.60 +	 \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
    1.61  
    1.62  	(*Alice responds with Nonce NB if she has seen the key before.
    1.63  	  Maybe should somehow check Nonce NA again.
    1.64  	  We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    1.65  	  Letting the Spy add or subtract 1 lets him send all nonces.
    1.66  	  Instead we distinguish the messages by sending the nonce twice.*)
    1.67 -  NS5:  "\\<lbrakk>evs5 \\<in> ns_shared;
    1.68 -	  Says B' A (Crypt K (Nonce NB)) \\<in> set evs5;
    1.69 -	  Says S  A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>)
    1.70 -	    \\<in> set evs5\\<rbrakk>
    1.71 -	 \\<Longrightarrow> Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) # evs5 \\<in> ns_shared"
    1.72 +  NS5:  "\<lbrakk>evs5 \<in> ns_shared;
    1.73 +	  Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
    1.74 +	  Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    1.75 +	    \<in> set evs5\<rbrakk>
    1.76 +	 \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared"
    1.77  
    1.78  	(*This message models possible leaks of session keys.
    1.79  	  The two Nonces identify the protocol run: the rule insists upon
    1.80  	  the true senders in order to make them accurate.*)
    1.81 -  Oops: "\\<lbrakk>evso \\<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \\<in> set evso;
    1.82 -	  Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>)
    1.83 -	      \\<in> set evso\\<rbrakk>
    1.84 -	 \\<Longrightarrow> Notes Spy \\<lbrace>Nonce NA, Nonce NB, Key K\\<rbrace> # evso \\<in> ns_shared"
    1.85 +  Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
    1.86 +	  Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    1.87 +	      \<in> set evso\<rbrakk>
    1.88 +	 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
    1.89  
    1.90  
    1.91  declare Says_imp_knows_Spy [THEN parts.Inj, dest]
    1.92 @@ -79,9 +79,9 @@
    1.93  declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    1.94  
    1.95  
    1.96 -(*A "possibility property": there are traces that reach the end*)
    1.97 -lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>N K. \\<exists>evs \\<in> ns_shared.
    1.98 -                              Says A B (Crypt K \\<lbrace>Nonce N, Nonce N\\<rbrace>) \\<in> set evs"
    1.99 +text{*A "possibility property": there are traces that reach the end*}
   1.100 +lemma "A \<noteq> Server \<Longrightarrow> \<exists>N K. \<exists>evs \<in> ns_shared.
   1.101 +                              Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
   1.102  apply (intro exI bexI)
   1.103  apply (rule_tac [2] ns_shared.Nil
   1.104         [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
   1.105 @@ -89,94 +89,94 @@
   1.106  done
   1.107  
   1.108  (*This version is similar, while instantiating ?K and ?N to epsilon-terms
   1.109 -lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>evs \\<in> ns_shared.
   1.110 -                Says A B (Crypt ?K \\<lbrace>Nonce ?N, Nonce ?N\\<rbrace>) \\<in> set evs"
   1.111 +lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
   1.112 +                Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
   1.113  *)
   1.114  
   1.115  
   1.116 -(**** Inductive proofs about ns_shared ****)
   1.117 +subsection{*Inductive proofs about @{term ns_shared}*}
   1.118  
   1.119 -(** Forwarding lemmas, to aid simplification **)
   1.120 +subsubsection{*Forwarding lemmas, to aid simplification*}
   1.121  
   1.122 -(*For reasoning about the encrypted portion of message NS3*)
   1.123 +text{*For reasoning about the encrypted portion of message NS3*}
   1.124  lemma NS3_msg_in_parts_spies:
   1.125 -     "Says S A (Crypt KA \\<lbrace>N, B, K, X\\<rbrace>) \\<in> set evs \\<Longrightarrow> X \\<in> parts (spies evs)"
   1.126 +     "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
   1.127  by blast
   1.128  
   1.129 -(*For reasoning about the Oops message*)
   1.130 +text{*For reasoning about the Oops message*}
   1.131  lemma Oops_parts_spies:
   1.132 -     "Says Server A (Crypt (shrK A) \\<lbrace>NA, B, K, X\\<rbrace>) \\<in> set evs
   1.133 -            \\<Longrightarrow> K \\<in> parts (spies evs)"
   1.134 +     "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
   1.135 +            \<Longrightarrow> K \<in> parts (spies evs)"
   1.136  by blast
   1.137  
   1.138 -(** Theorems of the form X \\<notin> parts (spies evs) imply that NOBODY
   1.139 -    sends messages containing X! **)
   1.140 +text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that NOBODY
   1.141 +    sends messages containing @{term X}*}
   1.142  
   1.143 -(*Spy never sees another agent's shared key! (unless it's bad at start)*)
   1.144 +text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
   1.145  lemma Spy_see_shrK [simp]:
   1.146 -     "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"
   1.147 +     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   1.148  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
   1.149  done
   1.150  
   1.151  lemma Spy_analz_shrK [simp]:
   1.152 -     "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)"
   1.153 +     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   1.154  by auto
   1.155  
   1.156  
   1.157 -(*Nobody can have used non-existent keys!*)
   1.158 +text{*Nobody can have used non-existent keys!*}
   1.159  lemma new_keys_not_used [rule_format, simp]:
   1.160 -    "evs \\<in> ns_shared \\<Longrightarrow> Key K \\<notin> used evs \\<longrightarrow> K \\<notin> keysFor (parts (spies evs))"
   1.161 +    "evs \<in> ns_shared \<Longrightarrow> Key K \<notin> used evs \<longrightarrow> K \<notin> keysFor (parts (spies evs))"
   1.162  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
   1.163 -(*Fake, NS2, NS4, NS5*)
   1.164 -apply (blast dest!: keysFor_parts_insert)+
   1.165 +txt{*Fake, NS2, NS4, NS5*}
   1.166 +apply (force dest!: keysFor_parts_insert, blast+)
   1.167  done
   1.168  
   1.169  
   1.170 -(** Lemmas concerning the form of items passed in messages **)
   1.171 +subsubsection{*Lemmas concerning the form of items passed in messages*}
   1.172  
   1.173 -(*Describes the form of K, X and K' when the Server sends this message.*)
   1.174 +text{*Describes the form of K, X and K' when the Server sends this message.*}
   1.175  lemma Says_Server_message_form:
   1.176 -     "\\<lbrakk>Says Server A (Crypt K' \\<lbrace>N, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
   1.177 -       evs \\<in> ns_shared\\<rbrakk>
   1.178 -      \\<Longrightarrow> K \\<notin> range shrK \\<and>
   1.179 -          X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>) \\<and>
   1.180 +     "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.181 +       evs \<in> ns_shared\<rbrakk>
   1.182 +      \<Longrightarrow> K \<notin> range shrK \<and>
   1.183 +          X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
   1.184            K' = shrK A"
   1.185  by (erule rev_mp, erule ns_shared.induct, auto)
   1.186  
   1.187  
   1.188 -(*If the encrypted message appears then it originated with the Server*)
   1.189 +text{*If the encrypted message appears then it originated with the Server*}
   1.190  lemma A_trusts_NS2:
   1.191 -     "\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs);
   1.192 -       A \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.193 -      \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs"
   1.194 +     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   1.195 +       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.196 +      \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
   1.197  apply (erule rev_mp)
   1.198  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
   1.199  done
   1.200  
   1.201  lemma cert_A_form:
   1.202 -     "\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs);
   1.203 -       A \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.204 -      \\<Longrightarrow> K \\<notin> range shrK \\<and>  X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>)"
   1.205 +     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   1.206 +       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.207 +      \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
   1.208  by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   1.209  
   1.210  (*EITHER describes the form of X when the following message is sent,
   1.211    OR     reduces it to the Fake case.
   1.212    Use Says_Server_message_form if applicable.*)
   1.213  lemma Says_S_message_form:
   1.214 -     "\\<lbrakk>Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
   1.215 -       evs \\<in> ns_shared\\<rbrakk>
   1.216 -      \\<Longrightarrow> (K \\<notin> range shrK \\<and> X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>))
   1.217 -          \\<or> X \\<in> analz (spies evs)"
   1.218 +     "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.219 +       evs \<in> ns_shared\<rbrakk>
   1.220 +      \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
   1.221 +          \<or> X \<in> analz (spies evs)"
   1.222  by (blast dest: Says_imp_knows_Spy cert_A_form analz.Inj)
   1.223  
   1.224  
   1.225  (*Alternative version also provable
   1.226  lemma Says_S_message_form2:
   1.227 -  "\\<lbrakk>Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
   1.228 -    evs \\<in> ns_shared\\<rbrakk>
   1.229 -   \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs
   1.230 -       \\<or> X \\<in> analz (spies evs)"
   1.231 -apply (case_tac "A \\<in> bad")
   1.232 +  "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.233 +    evs \<in> ns_shared\<rbrakk>
   1.234 +   \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
   1.235 +       \<or> X \<in> analz (spies evs)"
   1.236 +apply (case_tac "A \<in> bad")
   1.237  apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
   1.238  by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   1.239  *)
   1.240 @@ -185,35 +185,35 @@
   1.241  (****
   1.242   SESSION KEY COMPROMISE THEOREM.  To prove theorems of the form
   1.243  
   1.244 -  Key K \\<in> analz (insert (Key KAB) (spies evs)) \\<Longrightarrow>
   1.245 -  Key K \\<in> analz (spies evs)
   1.246 +  Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
   1.247 +  Key K \<in> analz (spies evs)
   1.248  
   1.249   A more general formula must be proved inductively.
   1.250  ****)
   1.251  
   1.252 -(*NOT useful in this form, but it says that session keys are not used
   1.253 +text{*NOT useful in this form, but it says that session keys are not used
   1.254    to encrypt messages containing other keys, in the actual protocol.
   1.255 -  We require that agents should behave like this subsequently also.*)
   1.256 -lemma  "\\<lbrakk>evs \\<in> ns_shared;  Kab \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
   1.257 -         (Crypt KAB X) \\<in> parts (spies evs) \\<and>
   1.258 -         Key K \\<in> parts {X} \\<longrightarrow> Key K \\<in> parts (spies evs)"
   1.259 +  We require that agents should behave like this subsequently also.*}
   1.260 +lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
   1.261 +         (Crypt KAB X) \<in> parts (spies evs) \<and>
   1.262 +         Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
   1.263  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
   1.264 -(*Fake*)
   1.265 +txt{*Fake*}
   1.266  apply (blast dest: parts_insert_subset_Un)
   1.267 -(*Base, NS4 and NS5*)
   1.268 +txt{*Base, NS4 and NS5*}
   1.269  apply auto
   1.270  done
   1.271  
   1.272  
   1.273 -(** Session keys are not used to encrypt other session keys **)
   1.274 +subsubsection{*Session keys are not used to encrypt other session keys*}
   1.275  
   1.276 -(*The equality makes the induction hypothesis easier to apply*)
   1.277 +text{*The equality makes the induction hypothesis easier to apply*}
   1.278  
   1.279  lemma analz_image_freshK [rule_format]:
   1.280 - "evs \\<in> ns_shared \\<Longrightarrow>
   1.281 -   \\<forall>K KK. KK \\<subseteq> - (range shrK) \\<longrightarrow>
   1.282 -             (Key K \\<in> analz (Key`KK \\<union> (spies evs))) =
   1.283 -             (K \\<in> KK \\<or> Key K \\<in> analz (spies evs))"
   1.284 + "evs \<in> ns_shared \<Longrightarrow>
   1.285 +   \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
   1.286 +             (Key K \<in> analz (Key`KK \<union> (spies evs))) =
   1.287 +             (K \<in> KK \<or> Key K \<in> analz (spies evs))"
   1.288  apply (erule ns_shared.induct, force)
   1.289  apply (drule_tac [7] Says_Server_message_form)
   1.290  apply (erule_tac [4] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
   1.291 @@ -221,97 +221,100 @@
   1.292  
   1.293  
   1.294  lemma analz_insert_freshK:
   1.295 -     "\\<lbrakk>evs \\<in> ns_shared;  KAB \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
   1.296 -       (Key K \\<in> analz (insert (Key KAB) (spies evs))) =
   1.297 -       (K = KAB \\<or> Key K \\<in> analz (spies evs))"
   1.298 +     "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
   1.299 +       (Key K \<in> analz (insert (Key KAB) (spies evs))) =
   1.300 +       (K = KAB \<or> Key K \<in> analz (spies evs))"
   1.301  by (simp only: analz_image_freshK analz_image_freshK_simps)
   1.302  
   1.303  
   1.304 -(** The session key K uniquely identifies the message **)
   1.305 +subsubsection{*The session key K uniquely identifies the message*}
   1.306  
   1.307 -(*In messages of this form, the session key uniquely identifies the rest*)
   1.308 +text{*In messages of this form, the session key uniquely identifies the rest*}
   1.309  lemma unique_session_keys:
   1.310 -     "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
   1.311 -       Says Server A' (Crypt (shrK A') \\<lbrace>NA', Agent B', Key K, X'\\<rbrace>) \\<in> set evs;
   1.312 -       evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow> A=A' \\<and> NA=NA' \\<and> B=B' \\<and> X = X'"
   1.313 +     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.314 +       Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
   1.315 +       evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
   1.316  apply (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
   1.317  done
   1.318  
   1.319  
   1.320 -(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
   1.321 +subsubsection{*Crucial secrecy property: Spy does not see the keys sent in msg NS2*}
   1.322  
   1.323 -(*Beware of [rule_format] and the universal quantifier!*)
   1.324 +text{*Beware of [rule_format] and the universal quantifier!*}
   1.325  lemma secrecy_lemma:
   1.326 -     "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K,
   1.327 -                                      Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>)
   1.328 -              \\<in> set evs;
   1.329 -         A \\<notin> bad;  B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.330 -      \\<Longrightarrow> (\\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs) \\<longrightarrow>
   1.331 -         Key K \\<notin> analz (spies evs)"
   1.332 +     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   1.333 +                                      Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   1.334 +              \<in> set evs;
   1.335 +         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.336 +      \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
   1.337 +         Key K \<notin> analz (spies evs)"
   1.338  apply (erule rev_mp)
   1.339  apply (erule ns_shared.induct, force)
   1.340  apply (frule_tac [7] Says_Server_message_form)
   1.341  apply (frule_tac [4] Says_S_message_form)
   1.342  apply (erule_tac [5] disjE)
   1.343 -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)  (*Fake*)
   1.344 -apply blast      (*NS2*)
   1.345 -(*NS3, Server sub-case*) (**LEVEL 8 **)
   1.346 +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)  
   1.347 +txt{*NS2*}
   1.348 +apply blast
   1.349 +txt{*NS3, Server sub-case*} 
   1.350  apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
   1.351  	     dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
   1.352 -(*NS3, Spy sub-case; also Oops*)
   1.353 +txt{*NS3, Spy sub-case; also Oops*}
   1.354  apply (blast dest: unique_session_keys)+
   1.355  done
   1.356  
   1.357  
   1.358  
   1.359 -(*Final version: Server's message in the most abstract form*)
   1.360 +text{*Final version: Server's message in the most abstract form*}
   1.361  lemma Spy_not_see_encrypted_key:
   1.362 -     "\\<lbrakk>Says Server A (Crypt K' \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
   1.363 -       \\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs;
   1.364 -       A \\<notin> bad;  B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.365 -      \\<Longrightarrow> Key K \\<notin> analz (spies evs)"
   1.366 +     "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.367 +       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   1.368 +       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.369 +      \<Longrightarrow> Key K \<notin> analz (spies evs)"
   1.370  by (blast dest: Says_Server_message_form secrecy_lemma)
   1.371  
   1.372  
   1.373 -(**** Guarantees available at various stages of protocol ***)
   1.374 +subsection{*Guarantees available at various stages of protocol*}
   1.375  
   1.376 -(*If the encrypted message appears then it originated with the Server*)
   1.377 +text{*If the encrypted message appears then it originated with the Server*}
   1.378  lemma B_trusts_NS3:
   1.379 -     "\\<lbrakk>Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace> \\<in> parts (spies evs);
   1.380 -       B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.381 -      \\<Longrightarrow> \\<exists>NA. Says Server A
   1.382 -               (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K,
   1.383 -                                 Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>)
   1.384 -              \\<in> set evs"
   1.385 +     "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   1.386 +       B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.387 +      \<Longrightarrow> \<exists>NA. Says Server A
   1.388 +               (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   1.389 +                                 Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   1.390 +              \<in> set evs"
   1.391  apply (erule rev_mp)
   1.392  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
   1.393  done
   1.394  
   1.395  
   1.396  lemma A_trusts_NS4_lemma [rule_format]:
   1.397 -   "evs \\<in> ns_shared \\<Longrightarrow>
   1.398 -      Key K \\<notin> analz (spies evs) \\<longrightarrow>
   1.399 -      Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow>
   1.400 -      Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
   1.401 -      Says B A (Crypt K (Nonce NB)) \\<in> set evs"
   1.402 +   "evs \<in> ns_shared \<Longrightarrow>
   1.403 +      Key K \<notin> analz (spies evs) \<longrightarrow>
   1.404 +      Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   1.405 +      Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   1.406 +      Says B A (Crypt K (Nonce NB)) \<in> set evs"
   1.407  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.408 -apply (analz_mono_contra, simp_all, blast)     (*Fake*)
   1.409 +apply (analz_mono_contra, simp_all, blast) 
   1.410  (*NS2: contradiction from the assumptions
   1.411 -  Key K \\<notin> used evs2  and Crypt K (Nonce NB) \\<in> parts (spies evs2) *)
   1.412 -apply (force dest!: Crypt_imp_keysFor, blast)     (*NS3*)
   1.413 -(*NS4*)
   1.414 +  Key K \<notin> used evs2  and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
   1.415 +apply (force dest!: Crypt_imp_keysFor)     
   1.416 +txt{*NS3*}
   1.417 +apply blast 
   1.418 +txt{*NS4*}
   1.419  apply (blast dest!: B_trusts_NS3
   1.420  	     dest: Says_imp_knows_Spy [THEN analz.Inj]
   1.421                     Crypt_Spy_analz_bad unique_session_keys)
   1.422  done
   1.423  
   1.424 -(*This version no longer assumes that K is secure*)
   1.425 +text{*This version no longer assumes that K is secure*}
   1.426  lemma A_trusts_NS4:
   1.427 -     "\\<lbrakk>Crypt K (Nonce NB) \\<in> parts (spies evs);
   1.428 -       Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs);
   1.429 -       \\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs;
   1.430 -       A \\<notin> bad;  B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.431 -      \\<Longrightarrow> Says B A (Crypt K (Nonce NB)) \\<in> set evs"
   1.432 +     "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
   1.433 +       Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   1.434 +       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   1.435 +       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.436 +      \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
   1.437  by (blast intro: A_trusts_NS4_lemma
   1.438            dest: A_trusts_NS2 Spy_not_see_encrypted_key)
   1.439  
   1.440 @@ -319,16 +322,18 @@
   1.441    component X in some instance of NS4.  Perhaps an interesting property,
   1.442    but not needed (after all) for the proofs below.*)
   1.443  theorem NS4_implies_NS3 [rule_format]:
   1.444 -  "evs \\<in> ns_shared \\<Longrightarrow>
   1.445 -     Key K \\<notin> analz (spies evs) \\<longrightarrow>
   1.446 -     Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow>
   1.447 -     Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
   1.448 -     (\\<exists>A'. Says A' B X \\<in> set evs)"
   1.449 +  "evs \<in> ns_shared \<Longrightarrow>
   1.450 +     Key K \<notin> analz (spies evs) \<longrightarrow>
   1.451 +     Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   1.452 +     Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   1.453 +     (\<exists>A'. Says A' B X \<in> set evs)"
   1.454  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra)
   1.455 -apply (simp_all add: ex_disj_distrib, blast)  (*Fake*)
   1.456 -apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   1.457 -apply blast  (*NS3*)
   1.458 -(*NS4*)
   1.459 +apply (simp_all add: ex_disj_distrib, blast)
   1.460 +txt{*NS2*}
   1.461 +apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  
   1.462 +txt{*NS3*}
   1.463 +apply blast
   1.464 +txt{*NS4*}
   1.465  apply (blast dest!: B_trusts_NS3
   1.466  	     dest: Says_imp_knows_Spy [THEN analz.Inj]
   1.467                     unique_session_keys Crypt_Spy_analz_bad)
   1.468 @@ -336,30 +341,32 @@
   1.469  
   1.470  
   1.471  lemma B_trusts_NS5_lemma [rule_format]:
   1.472 -  "\\<lbrakk>B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow>
   1.473 -     Key K \\<notin> analz (spies evs) \\<longrightarrow>
   1.474 +  "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
   1.475 +     Key K \<notin> analz (spies evs) \<longrightarrow>
   1.476       Says Server A
   1.477 -	  (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K,
   1.478 -			    Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) \\<in> set evs \\<longrightarrow>
   1.479 -     Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs) \\<longrightarrow>
   1.480 -     Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs"
   1.481 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)  (*Fake*)
   1.482 -apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   1.483 -apply (blast dest!: cert_A_form) (*NS3*)
   1.484 -(*NS5*)
   1.485 +	  (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   1.486 +			    Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
   1.487 +     Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   1.488 +     Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   1.489 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)
   1.490 +txt{*NS2*}
   1.491 +apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  
   1.492 +txt{*NS3*}
   1.493 +apply (blast dest!: cert_A_form) 
   1.494 +txt{*NS5*}
   1.495  apply (blast dest!: A_trusts_NS2
   1.496  	     dest: Says_imp_knows_Spy [THEN analz.Inj]
   1.497                     unique_session_keys Crypt_Spy_analz_bad)
   1.498  done
   1.499  
   1.500  
   1.501 -(*Very strong Oops condition reveals protocol's weakness*)
   1.502 +text{*Very strong Oops condition reveals protocol's weakness*}
   1.503  lemma B_trusts_NS5:
   1.504 -     "\\<lbrakk>Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs);
   1.505 -       Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace> \\<in> parts (spies evs);
   1.506 -       \\<forall>NA NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs;
   1.507 -       A \\<notin> bad;  B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.508 -      \\<Longrightarrow> Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs"
   1.509 +     "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
   1.510 +       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   1.511 +       \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   1.512 +       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.513 +      \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   1.514  by (blast intro: B_trusts_NS5_lemma
   1.515            dest: B_trusts_NS3 Spy_not_see_encrypted_key)
   1.516