src/HOL/Auth/ZhouGollmann.thy
changeset 14736 7104394df99a
parent 14207 f20fbb141673
child 14741 36582c356db7
     1.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Tue May 11 10:49:04 2004 +0200
     1.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Tue May 11 10:49:58 2004 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    broken :: "agent set"    
     1.5      --{*the compromised honest agents; TTP is included as it's not allowed to
     1.6          use the protocol*}
     1.7 -   "broken == insert TTP (bad - {Spy})"
     1.8 +   "broken == bad - {Spy}"
     1.9  
    1.10  declare broken_def [simp]
    1.11  
    1.12 @@ -49,8 +49,7 @@
    1.13    Fake: "[| evsf \<in> zg;  X \<in> synth (analz (spies evsf)) |]
    1.14  	 ==> Says Spy B X  # evsf \<in> zg"
    1.15  
    1.16 -Reception:  "[| evsr \<in> zg; A \<noteq> B; Says A B X \<in> set evsr |]
    1.17 -	     ==> Gets B X # evsr \<in> zg"
    1.18 +Reception:  "[| evsr \<in> zg; Says A B X \<in> set evsr |] ==> Gets B X # evsr \<in> zg"
    1.19  
    1.20    (*L is fresh for honest agents.
    1.21      We don't require K to be fresh because we don't bother to prove secrecy!
    1.22 @@ -68,9 +67,8 @@
    1.23  	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|]
    1.24         ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} # evs2  \<in>  zg"
    1.25  
    1.26 -  (*K is symmetric must be repeated IF there's spy*)
    1.27 -  (*A must check that NRR is B's signature to learn the sender's name*)
    1.28 -  (*without spy, the matching label would be enough*)
    1.29 +  (*A must check that NRR is B's signature to learn the sender's name;
    1.30 +    without spy, the matching label would be enough*)
    1.31    ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys;
    1.32  	   Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3;
    1.33  	   Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3;
    1.34 @@ -81,16 +79,20 @@
    1.35  
    1.36   (*TTP checks that sub_K is A's signature to learn who issued K, then
    1.37     gives credentials to A and B.  The Notes event models the availability of
    1.38 -   the credentials, but the act of fetching them is not modelled.*)
    1.39 - (*Also said TTP_prepare_ftp*)
    1.40 +   the credentials, but the act of fetching them is not modelled.  We also
    1.41 +   give con_K to the Spy. This makes the threat model more dangerous, while 
    1.42 +   also allowing lemma @{text Crypt_used_imp_spies} to omit the condition
    1.43 +   @{term "K \<noteq> priK TTP"}. *)
    1.44    ZG4: "[| evs4 \<in> zg; K \<in> symKeys;
    1.45  	   Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
    1.46  	     \<in> set evs4;
    1.47  	   sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
    1.48  	   con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
    1.49  				      Nonce L, Key K|}|]
    1.50 -       ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
    1.51 -	     # evs4 \<in> zg"
    1.52 +       ==> Says TTP Spy con_K
    1.53 +           #
    1.54 +	   Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
    1.55 +	   # evs4 \<in> zg"
    1.56  
    1.57  
    1.58  declare Says_imp_knows_Spy [THEN analz.Inj, dest]
    1.59 @@ -132,7 +134,7 @@
    1.60  text{*Lets us replace proofs about @{term "used evs"} by simpler proofs 
    1.61  about @{term "parts (spies evs)"}.*}
    1.62  lemma Crypt_used_imp_spies:
    1.63 -     "[| Crypt K X \<in> used evs;  K \<noteq> priK TTP; evs \<in> zg |]
    1.64 +     "[| Crypt K X \<in> used evs; evs \<in> zg |]
    1.65        ==> Crypt K X \<in> parts (spies evs)"
    1.66  apply (erule rev_mp)
    1.67  apply (erule zg.induct)
    1.68 @@ -205,13 +207,15 @@
    1.69  txt{*Fake*}
    1.70  apply (simp add: parts_insert_knows_A, blast) 
    1.71  txt{*ZG1*}
    1.72 -apply (auto intro!: exI)
    1.73 +apply (force intro!: exI)
    1.74 +txt{*ZG4*}
    1.75 +apply (auto ); 
    1.76  done
    1.77  
    1.78  theorem NRO_authenticity:
    1.79       "[| NRO \<in> used evs;
    1.80           NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    1.81 -         A \<notin> broken;  evs \<in> zg |]
    1.82 +         A \<notin> broken; evs \<in> zg |]
    1.83       ==> \<exists>C Y. Says A C Y \<in> set evs & NRO \<in> parts {Y}"
    1.84  apply auto
    1.85   apply (force dest!: Crypt_used_imp_spies NRO_authenticity_good)
    1.86 @@ -340,8 +344,8 @@
    1.87  done
    1.88  
    1.89  text{*If @{term TTP} holds @{term con_K} then @{term A} sent
    1.90 - @{term sub_K}.  We assume that @{term A} is not broken.  Nothing needs to
    1.91 - be assumed about the form of @{term con_K}!*}
    1.92 + @{term sub_K}.  We assume that @{term A} is not broken.  Importantly, nothing
    1.93 +  needs to be assumed about the form of @{term con_K}!*}
    1.94  lemma Notes_TTP_imp_Says_A:
    1.95       "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
    1.96             \<in> set evs;
    1.97 @@ -350,7 +354,8 @@
    1.98      ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
    1.99  by (blast dest!: Notes_TTP_imp_Gets [THEN Gets_imp_knows_Spy, THEN parts.Inj] intro: sub_K_authenticity)
   1.100  
   1.101 -text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.*}
   1.102 +text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.  We again
   1.103 +   assume that @{term A} is not broken. *}
   1.104  theorem B_sub_K_authenticity:
   1.105       "[|con_K \<in> used evs;
   1.106          con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,