src/HOL/Auth/ZhouGollmann.thy

--- a/src/HOL/Auth/ZhouGollmann.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -35,7 +35,7 @@
   Nil:  "[] \<in> zg"
 
 | Fake: "[| evsf \<in> zg;  X \<in> synth (analz (spies evsf)) |]
-	 ==> Says Spy B X  # evsf \<in> zg"
+         ==> Says Spy B X  # evsf \<in> zg"
 
 | Reception:  "[| evsr \<in> zg; Says A B X \<in> set evsr |] ==> Gets B X # evsr \<in> zg"
 
@@ -44,26 +44,26 @@
     We just assume that the protocol's objective is to deliver K fairly,
     rather than to keep M secret.*)
 | ZG1: "[| evs1 \<in> zg;  Nonce L \<notin> used evs1; C = Crypt K (Number m);
-	   K \<in> symKeys;
-	   NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|]
+           K \<in> symKeys;
+           NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|]
        ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} # evs1 \<in> zg"
 
   (*B must check that NRO is A's signature to learn the sender's name*)
 | ZG2: "[| evs2 \<in> zg;
-	   Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs2;
-	   NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
-	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|]
+           Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs2;
+           NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+           NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|]
        ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} # evs2  \<in>  zg"
 
   (*A must check that NRR is B's signature to learn the sender's name;
     without spy, the matching label would be enough*)
 | ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys;
-	   Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3;
-	   Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3;
-	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
-	   sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}|]
+           Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3;
+           Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3;
+           NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+           sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}|]
        ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
-	     # evs3 \<in> zg"
+             # evs3 \<in> zg"
 
  (*TTP checks that sub_K is A's signature to learn who issued K, then
    gives credentials to A and B.  The Notes event models the availability of
@@ -72,15 +72,15 @@
    also allowing lemma @{text Crypt_used_imp_spies} to omit the condition
    @{term "K \<noteq> priK TTP"}. *)
 | ZG4: "[| evs4 \<in> zg; K \<in> symKeys;
-	   Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
-	     \<in> set evs4;
-	   sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
-	   con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
-				      Nonce L, Key K|}|]
+           Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
+             \<in> set evs4;
+           sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+           con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
+                                      Nonce L, Key K|}|]
        ==> Says TTP Spy con_K
            #
-	   Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
-	   # evs4 \<in> zg"
+           Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+           # evs4 \<in> zg"
 
 
 declare Says_imp_knows_Spy [THEN analz.Inj, dest]