src/HOL/Auth/NS_Shared.thy
changeset 32960 69916a850301
parent 32527 569e8d6729a1
child 36866 426d5781bb25
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -27,61 +27,61 @@
     1.4  
     1.5  inductive_set ns_shared :: "event list set"
     1.6   where
     1.7 -	(*Initial trace is empty*)
     1.8 +        (*Initial trace is empty*)
     1.9    Nil:  "[] \<in> ns_shared"
    1.10 -	(*The spy MAY say anything he CAN say.  We do not expect him to
    1.11 -	  invent new nonces here, but he can also use NS1.  Common to
    1.12 -	  all similar protocols.*)
    1.13 +        (*The spy MAY say anything he CAN say.  We do not expect him to
    1.14 +          invent new nonces here, but he can also use NS1.  Common to
    1.15 +          all similar protocols.*)
    1.16  | Fake: "\<lbrakk>evsf \<in> ns_shared;  X \<in> synth (analz (spies evsf))\<rbrakk>
    1.17 -	 \<Longrightarrow> Says Spy B X # evsf \<in> ns_shared"
    1.18 +         \<Longrightarrow> Says Spy B X # evsf \<in> ns_shared"
    1.19  
    1.20 -	(*Alice initiates a protocol run, requesting to talk to any B*)
    1.21 +        (*Alice initiates a protocol run, requesting to talk to any B*)
    1.22  | NS1:  "\<lbrakk>evs1 \<in> ns_shared;  Nonce NA \<notin> used evs1\<rbrakk>
    1.23 -	 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1  \<in>  ns_shared"
    1.24 +         \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1  \<in>  ns_shared"
    1.25  
    1.26 -	(*Server's response to Alice's message.
    1.27 -	  !! It may respond more than once to A's request !!
    1.28 -	  Server doesn't know who the true sender is, hence the A' in
    1.29 -	      the sender field.*)
    1.30 +        (*Server's response to Alice's message.
    1.31 +          !! It may respond more than once to A's request !!
    1.32 +          Server doesn't know who the true sender is, hence the A' in
    1.33 +              the sender field.*)
    1.34  | NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;  KAB \<in> symKeys;
    1.35 -	  Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
    1.36 -	 \<Longrightarrow> Says Server A
    1.37 -	       (Crypt (shrK A)
    1.38 -		  \<lbrace>Nonce NA, Agent B, Key KAB,
    1.39 -		    (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>)
    1.40 -	       # evs2 \<in> ns_shared"
    1.41 +          Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
    1.42 +         \<Longrightarrow> Says Server A
    1.43 +               (Crypt (shrK A)
    1.44 +                  \<lbrace>Nonce NA, Agent B, Key KAB,
    1.45 +                    (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>)
    1.46 +               # evs2 \<in> ns_shared"
    1.47  
    1.48 -	 (*We can't assume S=Server.  Agent A "remembers" her nonce.
    1.49 -	   Need A \<noteq> Server because we allow messages to self.*)
    1.50 +         (*We can't assume S=Server.  Agent A "remembers" her nonce.
    1.51 +           Need A \<noteq> Server because we allow messages to self.*)
    1.52  | NS3:  "\<lbrakk>evs3 \<in> ns_shared;  A \<noteq> Server;
    1.53 -	  Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3;
    1.54 -	  Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk>
    1.55 -	 \<Longrightarrow> Says A B X # evs3 \<in> ns_shared"
    1.56 +          Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3;
    1.57 +          Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk>
    1.58 +         \<Longrightarrow> Says A B X # evs3 \<in> ns_shared"
    1.59  
    1.60 -	(*Bob's nonce exchange.  He does not know who the message came
    1.61 -	  from, but responds to A because she is mentioned inside.*)
    1.62 +        (*Bob's nonce exchange.  He does not know who the message came
    1.63 +          from, but responds to A because she is mentioned inside.*)
    1.64  | NS4:  "\<lbrakk>evs4 \<in> ns_shared;  Nonce NB \<notin> used evs4;  K \<in> symKeys;
    1.65 -	  Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
    1.66 -	 \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
    1.67 +          Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
    1.68 +         \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
    1.69  
    1.70 -	(*Alice responds with Nonce NB if she has seen the key before.
    1.71 -	  Maybe should somehow check Nonce NA again.
    1.72 -	  We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    1.73 -	  Letting the Spy add or subtract 1 lets him send all nonces.
    1.74 -	  Instead we distinguish the messages by sending the nonce twice.*)
    1.75 +        (*Alice responds with Nonce NB if she has seen the key before.
    1.76 +          Maybe should somehow check Nonce NA again.
    1.77 +          We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    1.78 +          Letting the Spy add or subtract 1 lets him send all nonces.
    1.79 +          Instead we distinguish the messages by sending the nonce twice.*)
    1.80  | NS5:  "\<lbrakk>evs5 \<in> ns_shared;  K \<in> symKeys;
    1.81 -	  Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
    1.82 -	  Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    1.83 -	    \<in> set evs5\<rbrakk>
    1.84 -	 \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared"
    1.85 +          Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
    1.86 +          Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    1.87 +            \<in> set evs5\<rbrakk>
    1.88 +         \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared"
    1.89  
    1.90 -	(*This message models possible leaks of session keys.
    1.91 -	  The two Nonces identify the protocol run: the rule insists upon
    1.92 -	  the true senders in order to make them accurate.*)
    1.93 +        (*This message models possible leaks of session keys.
    1.94 +          The two Nonces identify the protocol run: the rule insists upon
    1.95 +          the true senders in order to make them accurate.*)
    1.96  | Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
    1.97 -	  Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    1.98 -	      \<in> set evso\<rbrakk>
    1.99 -	 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
   1.100 +          Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
   1.101 +              \<in> set evso\<rbrakk>
   1.102 +         \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
   1.103  
   1.104  
   1.105  declare Says_imp_knows_Spy [THEN parts.Inj, dest]
   1.106 @@ -98,7 +98,7 @@
   1.107  apply (intro exI bexI)
   1.108  apply (rule_tac [2] ns_shared.Nil
   1.109         [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
   1.110 -	THEN ns_shared.NS4, THEN ns_shared.NS5])
   1.111 +        THEN ns_shared.NS4, THEN ns_shared.NS5])
   1.112  apply (possibility, simp add: used_Cons)
   1.113  done
   1.114  
   1.115 @@ -275,7 +275,7 @@
   1.116  apply blast
   1.117  txt{*NS3*}
   1.118  apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
   1.119 -	     dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
   1.120 +             dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
   1.121  txt{*Oops*}
   1.122  apply (blast dest: unique_session_keys)
   1.123  done
   1.124 @@ -355,8 +355,8 @@
   1.125    "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
   1.126       Key K \<notin> analz (spies evs) \<longrightarrow>
   1.127       Says Server A
   1.128 -	  (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   1.129 -			    Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
   1.130 +          (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   1.131 +                            Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
   1.132       Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   1.133       Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   1.134  apply (erule ns_shared.induct, force)
   1.135 @@ -366,7 +366,7 @@
   1.136  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
   1.137  txt{*NS5*}
   1.138  apply (blast dest!: A_trusts_NS2
   1.139 -	     dest: Says_imp_knows_Spy [THEN analz.Inj]
   1.140 +             dest: Says_imp_knows_Spy [THEN analz.Inj]
   1.141                     unique_session_keys Crypt_Spy_analz_bad)
   1.142  done
   1.143