better presentation
authorpaulson
Fri Oct 10 11:13:29 2003 +0200 (2003-10-10)
changeset 142256d1026266e2b
parent 14224 442c097c1437
child 14226 7afe0e5bcc83
better presentation
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_Bad.thy
     1.1 --- a/src/HOL/Auth/OtwayRees.thy	Thu Oct 09 18:20:14 2003 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.thy	Fri Oct 10 11:13:29 2003 +0200
     1.3 @@ -107,8 +107,6 @@
     1.4  done
     1.5  
     1.6  
     1.7 -(**** Inductive proofs about otway ****)
     1.8 -
     1.9  (** For reasoning about the encrypted portion of messages **)
    1.10  
    1.11  lemma OR2_analz_knows_Spy:
    1.12 @@ -131,10 +129,10 @@
    1.13    some reason proofs work without them!*)
    1.14  
    1.15  
    1.16 -(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
    1.17 -    sends messages containing X! **)
    1.18 +text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that
    1.19 +NOBODY sends messages containing X! *}
    1.20  
    1.21 -(*Spy never sees a good agent's shared key!*)
    1.22 +text{*Spy never sees a good agent's shared key!*}
    1.23  lemma Spy_see_shrK [simp]:
    1.24       "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
    1.25  by (erule otway.induct, force,
    1.26 @@ -173,7 +171,7 @@
    1.27  
    1.28  text{*Session keys are not used to encrypt other session keys*}
    1.29  
    1.30 -(*The equality makes the induction hypothesis easier to apply*)
    1.31 +text{*The equality makes the induction hypothesis easier to apply*}
    1.32  lemma analz_image_freshK [rule_format]:
    1.33   "evs \<in> otway ==>
    1.34     \<forall>K KK. KK <= -(range shrK) -->
    1.35 @@ -185,7 +183,6 @@
    1.36  apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto) 
    1.37  done
    1.38  
    1.39 -
    1.40  lemma analz_insert_freshK:
    1.41    "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
    1.42        (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
    1.43 @@ -193,8 +190,7 @@
    1.44  by (simp only: analz_image_freshK analz_image_freshK_simps)
    1.45  
    1.46  
    1.47 -(*** The Key K uniquely identifies the Server's  message. **)
    1.48 -
    1.49 +text{*The Key K uniquely identifies the Server's  message. *}
    1.50  lemma unique_session_keys:
    1.51       "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   \<in> set evs;
    1.52           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs;
    1.53 @@ -202,23 +198,21 @@
    1.54  apply (erule rev_mp)
    1.55  apply (erule rev_mp)
    1.56  apply (erule otway.induct, simp_all)
    1.57 -(*Remaining cases: OR3 and OR4*)
    1.58 -apply blast+
    1.59 +apply blast+  --{*OR3 and OR4*}
    1.60  done
    1.61  
    1.62  
    1.63  subsection{*Authenticity properties relating to NA*}
    1.64  
    1.65 -(*Only OR1 can have caused such a part of a message to appear.*)
    1.66 +text{*Only OR1 can have caused such a part of a message to appear.*}
    1.67  lemma Crypt_imp_OR1 [rule_format]:
    1.68   "[| A \<notin> bad;  evs \<in> otway |]
    1.69    ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
    1.70        Says A B {|NA, Agent A, Agent B,
    1.71                   Crypt (shrK A) {|NA, Agent A, Agent B|}|}
    1.72          \<in> set evs"
    1.73 -apply (erule otway.induct, force,
    1.74 -       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    1.75 -done
    1.76 +by (erule otway.induct, force,
    1.77 +    drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    1.78  
    1.79  lemma Crypt_imp_OR1_Gets:
    1.80       "[| Gets B {|NA, Agent A, Agent B,
    1.81 @@ -242,9 +236,9 @@
    1.82  done
    1.83  
    1.84  
    1.85 -(*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
    1.86 +text{*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
    1.87    OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
    1.88 -  over-simplified version of this protocol: see OtwayRees_Bad.*)
    1.89 +  over-simplified version of this protocol: see OtwayRees_Bad.*}
    1.90  lemma no_nonce_OR1_OR2:
    1.91     "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs);
    1.92         A \<notin> bad;  evs \<in> otway |]
    1.93 @@ -254,8 +248,8 @@
    1.94         drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    1.95  done
    1.96  
    1.97 -(*Crucial property: If the encrypted message appears, and A has used NA
    1.98 -  to start a run, then it originated with the Server!*)
    1.99 +text{*Crucial property: If the encrypted message appears, and A has used NA
   1.100 +  to start a run, then it originated with the Server!*}
   1.101  lemma NA_Crypt_imp_Server_msg [rule_format]:
   1.102       "[| A \<notin> bad;  evs \<in> otway |]
   1.103        ==> Says A B {|NA, Agent A, Agent B,
   1.104 @@ -267,19 +261,16 @@
   1.105                             Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
   1.106  apply (erule otway.induct, force,
   1.107         drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
   1.108 -(*OR1: it cannot be a new Nonce, contradiction.*)
   1.109 -apply blast
   1.110 -(*OR3*)
   1.111 -apply (blast dest!: no_nonce_OR1_OR2 intro: unique_NA)
   1.112 -(*OR4*)
   1.113 -apply (blast intro!: Crypt_imp_OR1)
   1.114 +apply blast  --{*OR1: by freshness*}
   1.115 +apply (blast dest!: no_nonce_OR1_OR2 intro: unique_NA)  --{*OR3*}
   1.116 +apply (blast intro!: Crypt_imp_OR1)  --{*OR4*}
   1.117  done
   1.118  
   1.119  
   1.120 -(*Corollary: if A receives B's OR4 message and the nonce NA agrees
   1.121 +text{*Corollary: if A receives B's OR4 message and the nonce NA agrees
   1.122    then the key really did come from the Server!  CANNOT prove this of the
   1.123    bad form of this protocol, even though we can prove
   1.124 -  Spy_not_see_encrypted_key*)
   1.125 +  Spy_not_see_encrypted_key*}
   1.126  lemma A_trusts_OR4:
   1.127       "[| Says A  B {|NA, Agent A, Agent B,
   1.128                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
   1.129 @@ -293,10 +284,9 @@
   1.130  by (blast intro!: NA_Crypt_imp_Server_msg)
   1.131  
   1.132  
   1.133 -(** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   1.134 +text{*Crucial secrecy property: Spy does not see the keys sent in msg OR3
   1.135      Does not in itself guarantee security: an attack could violate
   1.136 -    the premises, e.g. by having A=Spy **)
   1.137 -
   1.138 +    the premises, e.g. by having @{term "A=Spy"}*}
   1.139  lemma secrecy_lemma:
   1.140   "[| A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   1.141    ==> Says Server B
   1.142 @@ -308,9 +298,9 @@
   1.143  apply (frule_tac [7] Says_Server_message_form)
   1.144  apply (drule_tac [6] OR4_analz_knows_Spy)
   1.145  apply (drule_tac [4] OR2_analz_knows_Spy)
   1.146 -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
   1.147 -(*OR3, OR4, Oops*)
   1.148 -apply (blast dest: unique_session_keys)+
   1.149 +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
   1.150 +apply spy_analz  --{*Fake*}
   1.151 +apply (blast dest: unique_session_keys)+  --{*OR3, OR4, Oops*}
   1.152  done
   1.153  
   1.154  theorem Spy_not_see_encrypted_key:
   1.155 @@ -339,8 +329,8 @@
   1.156  by (blast dest: Spy_not_see_encrypted_key)
   1.157  
   1.158  
   1.159 -(*A's guarantee.  The Oops premise quantifies over NB because A cannot know
   1.160 -  what it is.*)
   1.161 +text{*A's guarantee.  The Oops premise quantifies over NB because A cannot know
   1.162 +  what it is.*}
   1.163  lemma A_gets_good_key:
   1.164       "[| Says A  B {|NA, Agent A, Agent B,
   1.165                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
   1.166 @@ -354,8 +344,8 @@
   1.167  
   1.168  subsection{*Authenticity properties relating to NB*}
   1.169  
   1.170 -(*Only OR2 can have caused such a part of a message to appear.  We do not
   1.171 -  know anything about X: it does NOT have to have the right form.*)
   1.172 +text{*Only OR2 can have caused such a part of a message to appear.  We do not
   1.173 +  know anything about X: it does NOT have to have the right form.*}
   1.174  lemma Crypt_imp_OR2:
   1.175       "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \<in> parts (knows Spy evs);
   1.176           B \<notin> bad;  evs \<in> otway |]
   1.177 @@ -378,12 +368,11 @@
   1.178  apply (erule rev_mp, erule rev_mp)
   1.179  apply (erule otway.induct, force,
   1.180         drule_tac [4] OR2_parts_knows_Spy, simp_all)
   1.181 -(*Fake, OR2*)
   1.182 -apply blast+
   1.183 +apply blast+  --{*Fake, OR2*}
   1.184  done
   1.185  
   1.186 -(*If the encrypted message appears, and B has used Nonce NB,
   1.187 -  then it originated with the Server!  Quite messy proof.*)
   1.188 +text{*If the encrypted message appears, and B has used Nonce NB,
   1.189 +  then it originated with the Server!  Quite messy proof.*}
   1.190  lemma NB_Crypt_imp_Server_msg [rule_format]:
   1.191   "[| B \<notin> bad;  evs \<in> otway |]
   1.192    ==> Crypt (shrK B) {|NB, Key K|} \<in> parts (knows Spy evs)
   1.193 @@ -397,14 +386,11 @@
   1.194                      \<in> set evs)"
   1.195  apply simp
   1.196  apply (erule otway.induct, force,
   1.197 -       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
   1.198 -(*OR1: it cannot be a new Nonce, contradiction.*)
   1.199 -(*OR2*)
   1.200 -apply blast
   1.201 -(*OR3: needs elim: MPair_parts or it takes forever!*)
   1.202 -apply (blast dest: unique_NB dest!: no_nonce_OR1_OR2)
   1.203 -(*OR4*)
   1.204 -apply (blast dest!: Crypt_imp_OR2)
   1.205 +       drule_tac [4] OR2_parts_knows_Spy, simp_all)
   1.206 +apply blast  --{*Fake*}
   1.207 +apply blast  --{*OR2*}
   1.208 +apply (blast dest: unique_NB dest!: no_nonce_OR1_OR2)  --{*OR3*}
   1.209 +apply (blast dest!: Crypt_imp_OR2)  --{*OR4*}
   1.210  done
   1.211  
   1.212  
   1.213 @@ -424,7 +410,8 @@
   1.214  by (blast intro!: NB_Crypt_imp_Server_msg)
   1.215  
   1.216  
   1.217 -(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
   1.218 +text{*The obvious combination of @{text B_trusts_OR3} with 
   1.219 +      @{text Spy_not_see_encrypted_key}*}
   1.220  lemma B_gets_good_key:
   1.221       "[| Says B Server {|NA, Agent A, Agent B, X',
   1.222                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
     2.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Thu Oct 09 18:20:14 2003 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Fri Oct 10 11:13:29 2003 +0200
     2.3 @@ -22,39 +22,39 @@
     2.4  consts  otway   :: "event list set"
     2.5  inductive "otway"
     2.6    intros
     2.7 -         (*Initial trace is empty*)
     2.8 -   Nil:  "[] \<in> otway"
     2.9 +   Nil: --{*The empty trace*}
    2.10 +        "[] \<in> otway"
    2.11  
    2.12 -         (*The spy MAY say anything he CAN say.  We do not expect him to
    2.13 -           invent new nonces here, but he can also use NS1.  Common to
    2.14 -           all similar protocols.*)
    2.15 -   Fake: "[| evsf \<in> otway;  X \<in> synth (analz (knows Spy evsf)) |]
    2.16 +   Fake: --{*The Spy may say anything he can say.  The sender field is correct,
    2.17 +            but agents don't use that information.*}
    2.18 +         "[| evsf \<in> otway;  X \<in> synth (analz (knows Spy evsf)) |]
    2.19            ==> Says Spy B X  # evsf \<in> otway"
    2.20  
    2.21 -         (*A message that has been sent can be received by the
    2.22 -           intended recipient.*)
    2.23 -   Reception: "[| evsr \<in> otway;  Says A B X \<in>set evsr |]
    2.24 +        
    2.25 +   Reception: --{*A message that has been sent can be received by the
    2.26 +                  intended recipient.*}
    2.27 +	      "[| evsr \<in> otway;  Says A B X \<in>set evsr |]
    2.28                 ==> Gets B X # evsr \<in> otway"
    2.29  
    2.30 -         (*Alice initiates a protocol run*)
    2.31 -   OR1:  "[| evs1 \<in> otway;  Nonce NA \<notin> used evs1 |]
    2.32 +   OR1:  --{*Alice initiates a protocol run*}
    2.33 +	 "[| evs1 \<in> otway;  Nonce NA \<notin> used evs1 |]
    2.34            ==> Says A B {|Nonce NA, Agent A, Agent B,
    2.35                           Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
    2.36                   # evs1 \<in> otway"
    2.37  
    2.38 -         (*Bob's response to Alice's message.
    2.39 -           This variant of the protocol does NOT encrypt NB.*)
    2.40 -   OR2:  "[| evs2 \<in> otway;  Nonce NB \<notin> used evs2;
    2.41 +   OR2:  --{*Bob's response to Alice's message.
    2.42 +             This variant of the protocol does NOT encrypt NB.*}
    2.43 +	 "[| evs2 \<in> otway;  Nonce NB \<notin> used evs2;
    2.44               Gets B {|Nonce NA, Agent A, Agent B, X|} \<in> set evs2 |]
    2.45            ==> Says B Server
    2.46                    {|Nonce NA, Agent A, Agent B, X, Nonce NB,
    2.47                      Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
    2.48                   # evs2 \<in> otway"
    2.49  
    2.50 -         (*The Server receives Bob's message and checks that the three NAs
    2.51 +   OR3:  --{*The Server receives Bob's message and checks that the three NAs
    2.52             match.  Then he sends a new session key to Bob with a packet for
    2.53 -           forwarding to Alice.*)
    2.54 -   OR3:  "[| evs3 \<in> otway;  Key KAB \<notin> used evs3;
    2.55 +           forwarding to Alice.*}
    2.56 +	 "[| evs3 \<in> otway;  Key KAB \<notin> used evs3;
    2.57               Gets Server
    2.58                    {|Nonce NA, Agent A, Agent B,
    2.59                      Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
    2.60 @@ -67,10 +67,10 @@
    2.61                      Crypt (shrK B) {|Nonce NB, Key KAB|}|}
    2.62                   # evs3 \<in> otway"
    2.63  
    2.64 -         (*Bob receives the Server's (?) message and compares the Nonces with
    2.65 -	   those in the message he previously sent the Server.
    2.66 -           Need B ~= Server because we allow messages to self.*)
    2.67 -   OR4:  "[| evs4 \<in> otway;  B ~= Server;
    2.68 +   OR4:  --{*Bob receives the Server's (?) message and compares the Nonces with
    2.69 +	     those in the message he previously sent the Server.
    2.70 +             Need @{term "B \<noteq> Server"} because we allow messages to self.*}
    2.71 +	 "[| evs4 \<in> otway;  B \<noteq> Server;
    2.72               Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
    2.73                               Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
    2.74                 \<in> set evs4;
    2.75 @@ -78,9 +78,9 @@
    2.76                 \<in> set evs4 |]
    2.77            ==> Says B A {|Nonce NA, X|} # evs4 \<in> otway"
    2.78  
    2.79 -         (*This message models possible leaks of session keys.  The nonces
    2.80 -           identify the protocol run.*)
    2.81 -   Oops: "[| evso \<in> otway;
    2.82 +   Oops: --{*This message models possible leaks of session keys.  The nonces
    2.83 +             identify the protocol run.*}
    2.84 +	 "[| evso \<in> otway;
    2.85               Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    2.86                 \<in> set evso |]
    2.87            ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway"
    2.88 @@ -91,7 +91,7 @@
    2.89  declare analz_into_parts [dest]
    2.90  declare Fake_parts_insert_in_Un  [dest]
    2.91  
    2.92 -(*A "possibility property": there are traces that reach the end*)
    2.93 +text{*A "possibility property": there are traces that reach the end*}
    2.94  lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
    2.95        ==> \<exists>NA. \<exists>evs \<in> otway.
    2.96              Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
    2.97 @@ -111,10 +111,7 @@
    2.98  done
    2.99  
   2.100  
   2.101 -(**** Inductive proofs about otway ****)
   2.102 -
   2.103 -
   2.104 -(** For reasoning about the encrypted portion of messages **)
   2.105 +subsection{*For reasoning about the encrypted portion of messages *}
   2.106  
   2.107  lemma OR2_analz_knows_Spy:
   2.108       "[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs;  evs \<in> otway |]
   2.109 @@ -131,20 +128,20 @@
   2.110        ==> K \<in> parts (knows Spy evs)"
   2.111  by blast
   2.112  
   2.113 -(*Forwarding lemma: see comments in OtwayRees.thy*)
   2.114 +text{*Forwarding lemma: see comments in OtwayRees.thy*}
   2.115  lemmas OR2_parts_knows_Spy =
   2.116      OR2_analz_knows_Spy [THEN analz_into_parts, standard]
   2.117  
   2.118  
   2.119 -(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
   2.120 -    sends messages containing X! **)
   2.121 +text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that
   2.122 +NOBODY sends messages containing X! *}
   2.123  
   2.124 -(*Spy never sees a good agent's shared key!*)
   2.125 +text{*Spy never sees a good agent's shared key!*}
   2.126  lemma Spy_see_shrK [simp]:
   2.127       "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   2.128 -apply (erule otway.induct, force,
   2.129 -       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   2.130 -done
   2.131 +by (erule otway.induct, force,
   2.132 +    drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   2.133 +
   2.134  
   2.135  lemma Spy_analz_shrK [simp]:
   2.136       "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   2.137 @@ -155,10 +152,10 @@
   2.138  by (blast dest: Spy_see_shrK)
   2.139  
   2.140  
   2.141 -(*** Proofs involving analz ***)
   2.142 +subsection{*Proofs involving analz *}
   2.143  
   2.144 -(*Describes the form of K and NA when the Server sends this message.  Also
   2.145 -  for Oops case.*)
   2.146 +text{*Describes the form of K and NA when the Server sends this message.  Also
   2.147 +  for Oops case.*}
   2.148  lemma Says_Server_message_form:
   2.149       "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
   2.150           evs \<in> otway |]
   2.151 @@ -178,9 +175,9 @@
   2.152  ****)
   2.153  
   2.154  
   2.155 -(** Session keys are not used to encrypt other session keys **)
   2.156 +text{*Session keys are not used to encrypt other session keys*}
   2.157  
   2.158 -(*The equality makes the induction hypothesis easier to apply*)
   2.159 +text{*The equality makes the induction hypothesis easier to apply*}
   2.160  lemma analz_image_freshK [rule_format]:
   2.161   "evs \<in> otway ==>
   2.162     \<forall>K KK. KK <= -(range shrK) -->
   2.163 @@ -199,8 +196,7 @@
   2.164  by (simp only: analz_image_freshK analz_image_freshK_simps)
   2.165  
   2.166  
   2.167 -(*** The Key K uniquely identifies the Server's  message. **)
   2.168 -
   2.169 +text{*The Key K uniquely identifies the Server's  message. *}
   2.170  lemma unique_session_keys:
   2.171       "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   \<in> set evs;
   2.172           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs;
   2.173 @@ -208,14 +204,13 @@
   2.174  apply (erule rev_mp)
   2.175  apply (erule rev_mp)
   2.176  apply (erule otway.induct, simp_all)
   2.177 -(*Remaining cases: OR3 and OR4*)
   2.178 -apply blast+
   2.179 +apply blast+  --{*OR3 and OR4*}
   2.180  done
   2.181  
   2.182  
   2.183 -(** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   2.184 +subsection{*Crucial secrecy property: Spy does not see the keys sent in msg OR3
   2.185      Does not in itself guarantee security: an attack could violate
   2.186 -    the premises, e.g. by having A=Spy **)
   2.187 +    the premises, e.g. by having @{term "A=Spy"} *}
   2.188  
   2.189  lemma secrecy_lemma:
   2.190   "[| A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   2.191 @@ -228,9 +223,9 @@
   2.192  apply (frule_tac [7] Says_Server_message_form)
   2.193  apply (drule_tac [6] OR4_analz_knows_Spy)
   2.194  apply (drule_tac [4] OR2_analz_knows_Spy)
   2.195 -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
   2.196 -(*OR3, OR4, Oops*)
   2.197 -apply (blast dest: unique_session_keys)+
   2.198 +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
   2.199 +apply spy_analz  --{*Fake*}
   2.200 +apply (blast dest: unique_session_keys)+  --{*OR3, OR4, Oops*}
   2.201  done
   2.202  
   2.203  
   2.204 @@ -244,26 +239,25 @@
   2.205  by (blast dest: Says_Server_message_form secrecy_lemma)
   2.206  
   2.207  
   2.208 -(*** Attempting to prove stronger properties ***)
   2.209 +subsection{*Attempting to prove stronger properties *}
   2.210  
   2.211 -(*Only OR1 can have caused such a part of a message to appear.
   2.212 -  The premise A \<noteq> B prevents OR2's similar-looking cryptogram from being
   2.213 -  picked up.  Original Otway-Rees doesn't need it.*)
   2.214 +text{*Only OR1 can have caused such a part of a message to appear. The premise
   2.215 +  @{term "A \<noteq> B"} prevents OR2's similar-looking cryptogram from being picked 
   2.216 +  up. Original Otway-Rees doesn't need it.*}
   2.217  lemma Crypt_imp_OR1 [rule_format]:
   2.218       "[| A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   2.219        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
   2.220            Says A B {|NA, Agent A, Agent B,
   2.221                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \<in> set evs"
   2.222 -apply (erule otway.induct, force,
   2.223 -       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   2.224 -done
   2.225 +by (erule otway.induct, force,
   2.226 +    drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   2.227  
   2.228  
   2.229 -(*Crucial property: If the encrypted message appears, and A has used NA
   2.230 +text{*Crucial property: If the encrypted message appears, and A has used NA
   2.231    to start a run, then it originated with the Server!
   2.232 -  The premise A \<noteq> B allows use of Crypt_imp_OR1*)
   2.233 -(*Only it is FALSE.  Somebody could make a fake message to Server
   2.234 -          substituting some other nonce NA' for NB.*)
   2.235 +  The premise @{term "A \<noteq> B"} allows use of @{text Crypt_imp_OR1}*}
   2.236 +text{*Only it is FALSE.  Somebody could make a fake message to Server
   2.237 +          substituting some other nonce NA' for NB.*}
   2.238  lemma "[| A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   2.239         ==> Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs) -->
   2.240             Says A B {|NA, Agent A, Agent B,
   2.241 @@ -275,15 +269,12 @@
   2.242                    Crypt (shrK B) {|NB, Key K|}|}  \<in> set evs)"
   2.243  apply (erule otway.induct, force,
   2.244         drule_tac [4] OR2_parts_knows_Spy, simp_all)
   2.245 -(*Fake*)
   2.246 -apply blast
   2.247 -(*OR1: it cannot be a new Nonce, contradiction.*)
   2.248 -apply blast
   2.249 -(*OR3 and OR4*)
   2.250 +apply blast  --{*Fake*}
   2.251 +apply blast  --{*OR1: it cannot be a new Nonce, contradiction.*}
   2.252 +txt{*OR3 and OR4*}
   2.253  apply (simp_all add: ex_disj_distrib)
   2.254 -(*OR4*)
   2.255 -prefer 2 apply (blast intro!: Crypt_imp_OR1)
   2.256 -(*OR3*)
   2.257 + prefer 2 apply (blast intro!: Crypt_imp_OR1)  --{*OR4*}
   2.258 +txt{*OR3*}
   2.259  apply clarify
   2.260  (*The hypotheses at this point suggest an attack in which nonce NB is used
   2.261    in two different roles: