src/HOL/Auth/NS_Shared.thy
changeset 11465 45d156ede468
parent 11280 6fdc4c4ccec1
child 11655 923e4d0d36d5
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Mon Aug 06 13:43:24 2001 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Mon Aug 06 15:46:20 2001 +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 \<forall>nonces.
    1.66 +	  Letting the Spy add or subtract 1 lets him send all nonces.
    1.67  	  Instead we distinguish the messages by sending the nonce twice.*)
    1.68 -  NS5:  "\<lbrakk>evs5 \<in> ns_shared;
    1.69 -	  Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
    1.70 -	  Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    1.71 -	    \<in> set evs5\<rbrakk>
    1.72 -	 \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared"
    1.73 +  NS5:  "\\<lbrakk>evs5 \\<in> ns_shared;
    1.74 +	  Says B' A (Crypt K (Nonce NB)) \\<in> set evs5;
    1.75 +	  Says S  A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>)
    1.76 +	    \\<in> set evs5\\<rbrakk>
    1.77 +	 \\<Longrightarrow> Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) # evs5 \\<in> ns_shared"
    1.78  
    1.79  	(*This message models possible leaks of session keys.
    1.80  	  The two Nonces identify the protocol run: the rule insists upon
    1.81  	  the true senders in order to make them accurate.*)
    1.82 -  Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
    1.83 -	  Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    1.84 -	      \<in> set evso\<rbrakk>
    1.85 -	 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
    1.86 +  Oops: "\\<lbrakk>evso \\<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \\<in> set evso;
    1.87 +	  Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>)
    1.88 +	      \\<in> set evso\\<rbrakk>
    1.89 +	 \\<Longrightarrow> Notes Spy \\<lbrace>Nonce NA, Nonce NB, Key K\\<rbrace> # evso \\<in> ns_shared"
    1.90  
    1.91  
    1.92  declare Says_imp_knows_Spy [THEN parts.Inj, dest]
    1.93 @@ -80,8 +80,8 @@
    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 +lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>N K. \\<exists>evs \\<in> ns_shared.
   1.100 +                              Says A B (Crypt K \\<lbrace>Nonce N, Nonce N\\<rbrace>) \\<in> set evs"
   1.101  apply (intro exI bexI)
   1.102  apply (rule_tac [2] ns_shared.Nil
   1.103         [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
   1.104 @@ -90,8 +90,8 @@
   1.105  done
   1.106  
   1.107  (*This version is similar, while instantiating ?K and ?N to epsilon-terms
   1.108 -lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
   1.109 -                Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
   1.110 +lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>evs \\<in> ns_shared.
   1.111 +                Says A B (Crypt ?K \\<lbrace>Nonce ?N, Nonce ?N\\<rbrace>) \\<in> set evs"
   1.112  *)
   1.113  
   1.114  
   1.115 @@ -101,34 +101,34 @@
   1.116  
   1.117  (*For reasoning about the encrypted portion of message NS3*)
   1.118  lemma NS3_msg_in_parts_spies:
   1.119 -     "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
   1.120 +     "Says S A (Crypt KA \\<lbrace>N, B, K, X\\<rbrace>) \\<in> set evs \\<Longrightarrow> X \\<in> parts (spies evs)"
   1.121  by blast
   1.122  
   1.123  (*For reasoning about the Oops message*)
   1.124  lemma Oops_parts_spies:
   1.125 -     "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
   1.126 -            \<Longrightarrow> K \<in> parts (spies evs)"
   1.127 +     "Says Server A (Crypt (shrK A) \\<lbrace>NA, B, K, X\\<rbrace>) \\<in> set evs
   1.128 +            \\<Longrightarrow> K \\<in> parts (spies evs)"
   1.129  by blast
   1.130  
   1.131 -(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
   1.132 +(** Theorems of the form X \\<notin> parts (spies evs) imply that NOBODY
   1.133      sends messages containing X! **)
   1.134  
   1.135  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
   1.136  lemma Spy_see_shrK [simp]:
   1.137 -     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   1.138 +     "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"
   1.139  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.140  apply simp_all
   1.141  apply blast+;
   1.142  done
   1.143  
   1.144  lemma Spy_analz_shrK [simp]:
   1.145 -     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   1.146 +     "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)"
   1.147  by auto
   1.148  
   1.149  
   1.150  (*Nobody can have used non-existent keys!*)
   1.151  lemma new_keys_not_used [rule_format, simp]:
   1.152 -    "evs \<in> ns_shared \<Longrightarrow> Key K \<notin> used evs \<longrightarrow> K \<notin> keysFor (parts (spies evs))"
   1.153 +    "evs \\<in> ns_shared \\<Longrightarrow> Key K \\<notin> used evs \\<longrightarrow> K \\<notin> keysFor (parts (spies evs))"
   1.154  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.155  apply simp_all
   1.156  (*Fake, NS2, NS4, NS5*)
   1.157 @@ -140,48 +140,48 @@
   1.158  
   1.159  (*Describes the form of K, X and K' when the Server sends this message.*)
   1.160  lemma Says_Server_message_form:
   1.161 -     "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.162 -       evs \<in> ns_shared\<rbrakk>
   1.163 -      \<Longrightarrow> K \<notin> range shrK \<and>
   1.164 -          X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
   1.165 +     "\\<lbrakk>Says Server A (Crypt K' \\<lbrace>N, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
   1.166 +       evs \\<in> ns_shared\\<rbrakk>
   1.167 +      \\<Longrightarrow> K \\<notin> range shrK \\<and>
   1.168 +          X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>) \\<and>
   1.169            K' = shrK A"
   1.170  by (erule rev_mp, erule ns_shared.induct, auto)
   1.171  
   1.172  
   1.173  (*If the encrypted message appears then it originated with the Server*)
   1.174  lemma A_trusts_NS2:
   1.175 -     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   1.176 -       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.177 -      \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
   1.178 +     "\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs);
   1.179 +       A \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.180 +      \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs"
   1.181  apply (erule rev_mp)
   1.182  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.183  apply auto
   1.184  done
   1.185  
   1.186  lemma cert_A_form:
   1.187 -     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   1.188 -       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.189 -      \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
   1.190 +     "\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs);
   1.191 +       A \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.192 +      \\<Longrightarrow> K \\<notin> range shrK \\<and>  X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>)"
   1.193  by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   1.194  
   1.195  (*EITHER describes the form of X when the following message is sent,
   1.196    OR     reduces it to the Fake case.
   1.197    Use Says_Server_message_form if applicable.*)
   1.198  lemma Says_S_message_form:
   1.199 -     "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.200 -       evs \<in> ns_shared\<rbrakk>
   1.201 -      \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
   1.202 -          \<or> X \<in> analz (spies evs)"
   1.203 +     "\\<lbrakk>Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
   1.204 +       evs \\<in> ns_shared\\<rbrakk>
   1.205 +      \\<Longrightarrow> (K \\<notin> range shrK \\<and> X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>))
   1.206 +          \\<or> X \\<in> analz (spies evs)"
   1.207  by (blast dest: Says_imp_knows_Spy cert_A_form analz.Inj)
   1.208  
   1.209  
   1.210  (*Alternative version also provable
   1.211  lemma Says_S_message_form2:
   1.212 -  "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.213 -    evs \<in> ns_shared\<rbrakk>
   1.214 -   \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
   1.215 -       \<or> X \<in> analz (spies evs)"
   1.216 -apply (case_tac "A \<in> bad")
   1.217 +  "\\<lbrakk>Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
   1.218 +    evs \\<in> ns_shared\\<rbrakk>
   1.219 +   \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs
   1.220 +       \\<or> X \\<in> analz (spies evs)"
   1.221 +apply (case_tac "A \\<in> bad")
   1.222  apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj]);
   1.223  by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   1.224  *)
   1.225 @@ -190,8 +190,8 @@
   1.226  (****
   1.227   SESSION KEY COMPROMISE THEOREM.  To prove theorems of the form
   1.228  
   1.229 -  Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
   1.230 -  Key K \<in> analz (spies evs)
   1.231 +  Key K \\<in> analz (insert (Key KAB) (spies evs)) \\<Longrightarrow>
   1.232 +  Key K \\<in> analz (spies evs)
   1.233  
   1.234   A more general formula must be proved inductively.
   1.235  ****)
   1.236 @@ -199,9 +199,9 @@
   1.237  (*NOT useful in this form, but it says that session keys are not used
   1.238    to encrypt messages containing other keys, in the actual protocol.
   1.239    We require that agents should behave like this subsequently also.*)
   1.240 -lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
   1.241 -         (Crypt KAB X) \<in> parts (spies evs) \<and>
   1.242 -         Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
   1.243 +lemma  "\\<lbrakk>evs \\<in> ns_shared;  Kab \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
   1.244 +         (Crypt KAB X) \\<in> parts (spies evs) \\<and>
   1.245 +         Key K \\<in> parts {X} \\<longrightarrow> Key K \\<in> parts (spies evs)"
   1.246  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.247  apply simp_all
   1.248  (*Fake*)
   1.249 @@ -216,10 +216,10 @@
   1.250  (*The equality makes the induction hypothesis easier to apply*)
   1.251  
   1.252  lemma analz_image_freshK [rule_format]:
   1.253 - "evs \<in> ns_shared \<Longrightarrow>
   1.254 -   \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
   1.255 -             (Key K \<in> analz (Key`KK \<union> (spies evs))) =
   1.256 -             (K \<in> KK \<or> Key K \<in> analz (spies evs))"
   1.257 + "evs \\<in> ns_shared \\<Longrightarrow>
   1.258 +   \\<forall>K KK. KK \\<subseteq> - (range shrK) \\<longrightarrow>
   1.259 +             (Key K \\<in> analz (Key`KK \\<union> (spies evs))) =
   1.260 +             (K \\<in> KK \\<or> Key K \\<in> analz (spies evs))"
   1.261  apply (erule ns_shared.induct, force)
   1.262  apply (drule_tac [7] Says_Server_message_form)
   1.263  apply (erule_tac [4] Says_S_message_form [THEN disjE])
   1.264 @@ -229,9 +229,9 @@
   1.265  
   1.266  
   1.267  lemma analz_insert_freshK:
   1.268 -     "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
   1.269 -       Key K \<in> analz (insert (Key KAB) (spies evs)) =
   1.270 -       (K = KAB \<or> Key K \<in> analz (spies evs))"
   1.271 +     "\\<lbrakk>evs \\<in> ns_shared;  KAB \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
   1.272 +       Key K \\<in> analz (insert (Key KAB) (spies evs)) =
   1.273 +       (K = KAB \\<or> Key K \\<in> analz (spies evs))"
   1.274  by (simp only: analz_image_freshK analz_image_freshK_simps)
   1.275  
   1.276  
   1.277 @@ -239,9 +239,9 @@
   1.278  
   1.279  (*In messages of this form, the session key uniquely identifies the rest*)
   1.280  lemma unique_session_keys:
   1.281 -     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.282 -       Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
   1.283 -       evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
   1.284 +     "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
   1.285 +       Says Server A' (Crypt (shrK A') \\<lbrace>NA', Agent B', Key K, X'\\<rbrace>) \\<in> set evs;
   1.286 +       evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow> A=A' \\<and> NA=NA' \\<and> B=B' \\<and> X = X'"
   1.287  apply (erule rev_mp, erule rev_mp, erule ns_shared.induct)
   1.288  apply simp_all
   1.289  apply blast+
   1.290 @@ -252,12 +252,12 @@
   1.291  
   1.292  (*Beware of [rule_format] and the universal quantifier!*)
   1.293  lemma secrecy_lemma:
   1.294 -     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   1.295 -                                      Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   1.296 -              \<in> set evs;
   1.297 -         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.298 -      \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
   1.299 -         Key K \<notin> analz (spies evs)"
   1.300 +     "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K,
   1.301 +                                      Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>)
   1.302 +              \\<in> set evs;
   1.303 +         A \\<notin> bad;  B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.304 +      \\<Longrightarrow> (\\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs) \\<longrightarrow>
   1.305 +         Key K \\<notin> analz (spies evs)"
   1.306  apply (erule rev_mp)
   1.307  apply (erule ns_shared.induct, force)
   1.308  apply (frule_tac [7] Says_Server_message_form)
   1.309 @@ -277,10 +277,10 @@
   1.310  
   1.311  (*Final version: Server's message in the most abstract form*)
   1.312  lemma Spy_not_see_encrypted_key:
   1.313 -     "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.314 -       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   1.315 -       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.316 -      \<Longrightarrow> Key K \<notin> analz (spies evs)"
   1.317 +     "\\<lbrakk>Says Server A (Crypt K' \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
   1.318 +       \\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs;
   1.319 +       A \\<notin> bad;  B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.320 +      \\<Longrightarrow> Key K \\<notin> analz (spies evs)"
   1.321  by (blast dest: Says_Server_message_form secrecy_lemma)
   1.322  
   1.323  
   1.324 @@ -288,12 +288,12 @@
   1.325  
   1.326  (*If the encrypted message appears then it originated with the Server*)
   1.327  lemma B_trusts_NS3:
   1.328 -     "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   1.329 -       B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.330 -      \<Longrightarrow> \<exists>NA. Says Server A
   1.331 -               (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   1.332 -                                 Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   1.333 -              \<in> set evs"
   1.334 +     "\\<lbrakk>Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace> \\<in> parts (spies evs);
   1.335 +       B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.336 +      \\<Longrightarrow> \\<exists>NA. Says Server A
   1.337 +               (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K,
   1.338 +                                 Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>)
   1.339 +              \\<in> set evs"
   1.340  apply (erule rev_mp)
   1.341  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.342  apply auto
   1.343 @@ -301,16 +301,16 @@
   1.344  
   1.345  
   1.346  lemma A_trusts_NS4_lemma [rule_format]:
   1.347 -   "evs \<in> ns_shared \<Longrightarrow>
   1.348 -      Key K \<notin> analz (spies evs) \<longrightarrow>
   1.349 -      Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   1.350 -      Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   1.351 -      Says B A (Crypt K (Nonce NB)) \<in> set evs"
   1.352 +   "evs \\<in> ns_shared \\<Longrightarrow>
   1.353 +      Key K \\<notin> analz (spies evs) \\<longrightarrow>
   1.354 +      Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow>
   1.355 +      Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
   1.356 +      Says B A (Crypt K (Nonce NB)) \\<in> set evs"
   1.357  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.358  apply (analz_mono_contra, simp_all)
   1.359  apply blast     (*Fake*)
   1.360  (*NS2: contradiction from the assumptions
   1.361 -  Key K \<notin> used evs2  and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
   1.362 +  Key K \\<notin> used evs2  and Crypt K (Nonce NB) \\<in> parts (spies evs2) *)
   1.363  apply (force dest!: Crypt_imp_keysFor)
   1.364  apply blast     (*NS3*)
   1.365  (*NS4*)
   1.366 @@ -321,11 +321,11 @@
   1.367  
   1.368  (*This version no longer assumes that K is secure*)
   1.369  lemma A_trusts_NS4:
   1.370 -     "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
   1.371 -       Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   1.372 -       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   1.373 -       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.374 -      \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
   1.375 +     "\\<lbrakk>Crypt K (Nonce NB) \\<in> parts (spies evs);
   1.376 +       Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs);
   1.377 +       \\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs;
   1.378 +       A \\<notin> bad;  B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.379 +      \\<Longrightarrow> Says B A (Crypt K (Nonce NB)) \\<in> set evs"
   1.380  by (blast intro: A_trusts_NS4_lemma
   1.381            dest: A_trusts_NS2 Spy_not_see_encrypted_key)
   1.382  
   1.383 @@ -333,11 +333,11 @@
   1.384    component X in some instance of NS4.  Perhaps an interesting property,
   1.385    but not needed (after all) for the proofs below.*)
   1.386  theorem NS4_implies_NS3 [rule_format]:
   1.387 -  "evs \<in> ns_shared \<Longrightarrow>
   1.388 -     Key K \<notin> analz (spies evs) \<longrightarrow>
   1.389 -     Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   1.390 -     Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   1.391 -     (\<exists>A'. Says A' B X \<in> set evs)"
   1.392 +  "evs \\<in> ns_shared \\<Longrightarrow>
   1.393 +     Key K \\<notin> analz (spies evs) \\<longrightarrow>
   1.394 +     Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow>
   1.395 +     Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
   1.396 +     (\\<exists>A'. Says A' B X \\<in> set evs)"
   1.397  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.398  apply analz_mono_contra
   1.399  apply (simp_all add: ex_disj_distrib)
   1.400 @@ -352,13 +352,13 @@
   1.401  
   1.402  
   1.403  lemma B_trusts_NS5_lemma [rule_format]:
   1.404 -  "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
   1.405 -     Key K \<notin> analz (spies evs) \<longrightarrow>
   1.406 +  "\\<lbrakk>B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow>
   1.407 +     Key K \\<notin> analz (spies evs) \\<longrightarrow>
   1.408       Says Server A
   1.409 -	  (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   1.410 -			    Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
   1.411 -     Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   1.412 -     Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   1.413 +	  (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K,
   1.414 +			    Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) \\<in> set evs \\<longrightarrow>
   1.415 +     Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs) \\<longrightarrow>
   1.416 +     Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs"
   1.417  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.418  apply analz_mono_contra
   1.419  apply simp_all
   1.420 @@ -374,11 +374,11 @@
   1.421  
   1.422  (*Very strong Oops condition reveals protocol's weakness*)
   1.423  lemma B_trusts_NS5:
   1.424 -     "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
   1.425 -       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   1.426 -       \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   1.427 -       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.428 -      \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   1.429 +     "\\<lbrakk>Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs);
   1.430 +       Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace> \\<in> parts (spies evs);
   1.431 +       \\<forall>NA NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs;
   1.432 +       A \\<notin> bad;  B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
   1.433 +      \\<Longrightarrow> Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs"
   1.434  by (blast intro: B_trusts_NS5_lemma
   1.435            dest: B_trusts_NS3 Spy_not_see_encrypted_key)
   1.436