1.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Wed Jul 11 11:13:08 2007 +0200
     1.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Wed Jul 11 11:14:51 2007 +0200
     1.3 @@ -29,29 +29,27 @@
     1.4  
     1.5  declare broken_def [simp]
     1.6  
     1.7 -consts  zg  :: "event list set"
     1.8 -
     1.9 -inductive zg
    1.10 -  intros
    1.11 +inductive_set zg :: "event list set"
    1.12 +  where
    1.13  
    1.14    Nil:  "[] \<in> zg"
    1.15  
    1.16 -  Fake: "[| evsf \<in> zg;  X \<in> synth (analz (spies evsf)) |]
    1.17 +| Fake: "[| evsf \<in> zg;  X \<in> synth (analz (spies evsf)) |]
    1.18  	 ==> Says Spy B X  # evsf \<in> zg"
    1.19  
    1.20 -Reception:  "[| evsr \<in> zg; Says A B X \<in> set evsr |] ==> Gets B X # evsr \<in> zg"
    1.21 +| Reception:  "[| evsr \<in> zg; Says A B X \<in> set evsr |] ==> Gets B X # evsr \<in> zg"
    1.22  
    1.23    (*L is fresh for honest agents.
    1.24      We don't require K to be fresh because we don't bother to prove secrecy!
    1.25      We just assume that the protocol's objective is to deliver K fairly,
    1.26      rather than to keep M secret.*)
    1.27 -  ZG1: "[| evs1 \<in> zg;  Nonce L \<notin> used evs1; C = Crypt K (Number m);
    1.28 +| ZG1: "[| evs1 \<in> zg;  Nonce L \<notin> used evs1; C = Crypt K (Number m);
    1.29  	   K \<in> symKeys;
    1.30  	   NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|]
    1.31         ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} # evs1 \<in> zg"
    1.32  
    1.33    (*B must check that NRO is A's signature to learn the sender's name*)
    1.34 -  ZG2: "[| evs2 \<in> zg;
    1.35 +| ZG2: "[| evs2 \<in> zg;
    1.36  	   Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs2;
    1.37  	   NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    1.38  	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|]
    1.39 @@ -59,7 +57,7 @@
    1.40  
    1.41    (*A must check that NRR is B's signature to learn the sender's name;
    1.42      without spy, the matching label would be enough*)
    1.43 -  ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys;
    1.44 +| ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys;
    1.45  	   Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3;
    1.46  	   Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3;
    1.47  	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
    1.48 @@ -73,7 +71,7 @@
    1.49     give con_K to the Spy. This makes the threat model more dangerous, while 
    1.50     also allowing lemma @{text Crypt_used_imp_spies} to omit the condition
    1.51     @{term "K \<noteq> priK TTP"}. *)
    1.52 -  ZG4: "[| evs4 \<in> zg; K \<in> symKeys;
    1.53 +| ZG4: "[| evs4 \<in> zg; K \<in> symKeys;
    1.54  	   Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
    1.55  	     \<in> set evs4;
    1.56  	   sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};