# HG changeset patch
# User paulson
# Date 1052151721 -7200
# Node ID 8fe7e12290e1637008f826500ab5db681a13b330
# Parent  8ab1d3e73bb1afb75a645db659e92e466ca89ee1
improved presentation of HOL/Auth theories

diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/CertifiedEmail.thy
--- a/src/HOL/Auth/CertifiedEmail.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy	Mon May 05 18:22:01 2003 +0200
@@ -1,27 +1,19 @@
 (*  Title:      HOL/Auth/CertifiedEmail
     ID:         $Id$
     Author:     Giampaolo Bella, Christiano Longo and Lawrence C Paulson
+*)
 
-The certified electronic mail protocol by Abadi et al.
-*)
+header{*The Certified Electronic Mail Protocol by Abadi et al.*}
 
 theory CertifiedEmail = Public:
 
 syntax
   TTP        :: agent
   RPwd       :: "agent => key"
-  TTPDecKey  :: key
-  TTPEncKey  :: key
-  TTPSigKey  :: key
-  TTPVerKey  :: key
 
 translations
   "TTP"   == "Server "
   "RPwd"  == "shrK "
-  "TTPDecKey" == "priEK Server"
-  "TTPEncKey" == "pubEK Server" 
-  "TTPSigKey" == "priSK Server"
-  "TTPVerKey" == "pubSK Server" 
 
  
 (*FIXME: the four options should be represented by pairs of 0 or 1.
@@ -48,7 +40,7 @@
 Fake: --{*The Spy may say anything he can say.  The sender field is correct,
           but agents don't use that information.*}
       "[| evsf \<in> certified_mail; X \<in> synth(analz(knows Spy evsf))|] 
-       ==> Says Spy B X #evsf \<in> certified_mail"
+       ==> Says Spy B X # evsf \<in> certified_mail"
 
 FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent
     equipped with the necessary credentials to serve as an SSL server.*}
@@ -61,7 +53,7 @@
    K \<in> symKeys;
    Nonce q \<notin> used evs1;
    hs = Hash {|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
-   S2TTP = Crypt TTPEncKey {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
+   S2TTP = Crypt (pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
  ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 
                 Number cleartext, Nonce q, S2TTP|} # evs1 
        \<in> certified_mail"
@@ -84,13 +76,13 @@
          He replies over the established SSL channel.*}
  "[|evs3 \<in> certified_mail;
     Notes TTP {|Agent R', Agent TTP, S2TTP'', Key(RPwd R'), hr'|} \<in> set evs3;
-    S2TTP'' = Crypt TTPEncKey 
+    S2TTP'' = Crypt (pubEK TTP) 
                      {|Agent S, Number BothAuth, Key k', Agent R', hs'|};
     TTP \<noteq> R';  hs' = hr';  k' \<in> symKeys|]
  ==> 
   Notes R' {|Agent TTP, Agent R', Key k', hr'|} # 
-  Gets S (Crypt TTPSigKey S2TTP'') # 
-  Says TTP S (Crypt TTPSigKey S2TTP'') # evs3 \<in> certified_mail"
+  Gets S (Crypt (priSK TTP) S2TTP'') # 
+  Says TTP S (Crypt (priSK TTP) S2TTP'') # evs3 \<in> certified_mail"
 
 Reception:
  "[|evsr \<in> certified_mail; Says A B X \<in> set evsr|]
@@ -99,7 +91,7 @@
 
 (*A "possibility property": there are traces that reach the end*)
 lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail.
-           Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs"
+           Says TTP S (Crypt (priSK TTP) S2TTP) \<in> set evs"
 apply (rule bexE [OF Key_supply1]) 
 apply (intro exI bexI)
 apply (rule_tac [2] certified_mail.Nil
@@ -176,33 +168,23 @@
      ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
 by (blast intro: Spy_dont_know_private_keys parts.Inj)
 
-lemma Spy_dont_know_TTPDecKey [simp]:
-     "evs \<in> certified_mail ==> Key TTPDecKey \<notin> parts(knows Spy evs)"
-by auto
+lemma Spy_dont_know_TTPKey_parts [simp]:
+     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(knows Spy evs)" 
+by simp
 
-lemma Spy_dont_know_TTPDecKey_analz [simp]:
-     "evs \<in> certified_mail ==> Key TTPDecKey \<notin> analz(knows Spy evs)" 
-by (force dest!: analz_subset_parts[THEN subsetD])
-
-lemma Spy_dont_know_TTPSigKey [simp]:
-     "evs \<in> certified_mail ==> Key TTPSigKey \<notin> parts(knows Spy evs)"
-by auto
-
-lemma Spy_dont_know_TTPSigKey_analz [simp]:
-     "evs \<in> certified_mail ==> Key TTPSigKey \<notin> analz(knows Spy evs)" 
+lemma Spy_dont_know_TTPKey_analz [simp]:
+     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(knows Spy evs)" 
 by (force dest!: analz_subset_parts[THEN subsetD])
 
 text{*Thus, prove any goal that assumes that @{term Spy} knows a private key
 belonging to @{term TTP}*}
-declare Spy_dont_know_TTPDecKey [THEN [2] rev_notE, elim!]
-declare Spy_dont_know_TTPSigKey [THEN [2] rev_notE, elim!]
-
+declare Spy_dont_know_TTPKey_parts [THEN [2] rev_notE, elim!]
 
 
 lemma CM3_k_parts_knows_Spy:
  "[| evs \<in> certified_mail;
      Notes TTP {|Agent A, Agent TTP,
-                 Crypt TTPEncKey {|Agent S, Number AO, Key K, 
+                 Crypt (pubEK TTP) {|Agent S, Number AO, Key K, 
                  Agent R, hs|}, Key (RPwd R), hs|} \<in> set evs|]
   ==> Key K \<in> parts(spies evs)"
 apply (rotate_tac 1)
@@ -250,8 +232,8 @@
 
 text{*Unused, but a guarantee of sorts*}
 theorem CertAutenticity:
-     "[|Crypt TTPSigKey X \<in> parts (spies evs); evs \<in> certified_mail|] 
-      ==> \<exists>A. Says TTP A (Crypt TTPSigKey X) \<in> set evs"
+     "[|Crypt (priSK TTP) X \<in> parts (spies evs); evs \<in> certified_mail|] 
+      ==> \<exists>A. Says TTP A (Crypt (priSK TTP) X) \<in> set evs"
 apply (erule rev_mp)
 apply (erule certified_mail.induct, simp_all) 
 txt{*Fake*}
@@ -272,7 +254,7 @@
 
 lemma analz_image_freshK [rule_format]:
  "evs \<in> certified_mail ==>
-   \<forall>K KK. invKey TTPEncKey \<notin> KK -->
+   \<forall>K KK. invKey (pubEK TTP) \<notin> KK -->
           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
 apply (erule certified_mail.induct)
@@ -289,7 +271,7 @@
 
 
 lemma analz_insert_freshK:
-  "[| evs \<in> certified_mail;  KAB \<noteq> invKey TTPEncKey |] ==>
+  "[| evs \<in> certified_mail;  KAB \<noteq> invKey (pubEK TTP) |] ==>
       (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
       (K = KAB | Key K \<in> analz (knows Spy evs))"
 by (simp only: analz_image_freshK analz_image_freshK_simps)
@@ -307,14 +289,14 @@
 lemma S2TTP_sender_lemma [rule_format]:
  "evs \<in> certified_mail ==>
     Key K \<notin> analz (knows Spy evs) -->
-    (\<forall>AO. Crypt TTPEncKey
+    (\<forall>AO. Crypt (pubEK TTP)
 	   {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs -->
     (\<exists>m ctxt q. 
         hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
 	Says S R
 	   {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
 	     Number ctxt, Nonce q,
-	     Crypt TTPEncKey
+	     Crypt (pubEK TTP)
 	      {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs))" 
 apply (erule certified_mail.induct, analz_mono_contra)
 apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp)
@@ -324,10 +306,9 @@
              dest!: analz_subset_parts[THEN subsetD])  
 txt{*Fake SSL*}
 apply (blast dest: Fake_parts_sing[THEN subsetD]
-            dest: analz_subset_parts[THEN subsetD])  
+             dest: analz_subset_parts[THEN subsetD])  
 txt{*Message 1*}
-apply clarsimp
-apply blast 
+apply (clarsimp, blast)
 txt{*Message 2*}
 apply (simp add: parts_insert2, clarify) 
 apply (drule parts_cut, assumption, simp) 
@@ -337,7 +318,7 @@
 done 
 
 lemma S2TTP_sender:
- "[|Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
+ "[|Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
     Key K \<notin> analz (knows Spy evs);
     evs \<in> certified_mail|]
   ==> \<exists>m ctxt q. 
@@ -345,7 +326,7 @@
 	Says S R
 	   {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
 	     Number ctxt, Nonce q,
-	     Crypt TTPEncKey
+	     Crypt (pubEK TTP)
 	      {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs" 
 by (blast intro: S2TTP_sender_lemma) 
 
@@ -377,13 +358,13 @@
         Says S R
            {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
              Number cleartext, Nonce q,
-             Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}|}
+             Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}|}
           \<in> set evs -->
        (\<forall>m' cleartext' q' hs'.
        Says S' R'
            {|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
              Number cleartext', Nonce q',
-             Crypt TTPEncKey {|Agent S', Number AO', Key K, Agent R', hs'|}|}
+             Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
           \<in> set evs --> R' = R & S' = S & AO' = AO & hs' = hs))" 
 apply (erule certified_mail.induct, analz_mono_contra, simp_all)
 txt{*Fake*} 
@@ -397,12 +378,12 @@
       "[|Says S R
            {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
              Number cleartext, Nonce q,
-             Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}|}
+             Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}|}
           \<in> set evs;
          Says S' R'
            {|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
              Number cleartext', Nonce q',
-             Crypt TTPEncKey {|Agent S', Number AO', Key K, Agent R', hs'|}|}
+             Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
           \<in> set evs;
          Key K \<notin> analz (knows Spy evs);
          evs \<in> certified_mail|]
@@ -418,14 +399,14 @@
 theorem Spy_see_encrypted_key_imp:
       "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
                      Number cleartext, Nonce q, S2TTP|} \<in> set evs;
+         S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
          Key K \<in> analz(knows Spy evs);
-         S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
 	 evs \<in> certified_mail;
          S\<noteq>Spy|]
-      ==> R \<in> bad & Gets S (Crypt TTPSigKey S2TTP) \<in> set evs"
-apply (erule rev_mp)
+      ==> R \<in> bad & Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
 apply (erule rev_mp)
 apply (erule ssubst)
+apply (erule rev_mp)
 apply (erule certified_mail.induct, simp_all)
 txt{*Fake*}
 apply spy_analz
@@ -446,7 +427,7 @@
 theorem Spy_not_see_encrypted_key:
       "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
                      Number cleartext, Nonce q, S2TTP|} \<in> set evs;
-         S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
+         S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
 	 evs \<in> certified_mail;
          S\<noteq>Spy; R \<notin> bad|]
       ==> Key K \<notin> analz(knows Spy evs)"
@@ -456,18 +437,15 @@
 text{*Agent @{term R}, who may be the Spy, doesn't receive the key
  until @{term S} has access to the return receipt.*} 
 theorem S_guarantee:
-      "[|Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs;
-         Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
+      "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
                      Number cleartext, Nonce q, S2TTP|} \<in> set evs;
-         S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
-         hs = Hash {|Number cleartext, Nonce q, response S R q, 
-                     Crypt K (Number m)|};
+         S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
+         Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs;
          S\<noteq>Spy;  evs \<in> certified_mail|]
-      ==> Gets S (Crypt TTPSigKey S2TTP) \<in> set evs"
-apply (erule rev_mp)
+      ==> Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
 apply (erule rev_mp)
 apply (erule ssubst)
-apply (erule ssubst)
+apply (erule rev_mp)
 apply (erule certified_mail.induct, simp_all)
 txt{*Message 1*}
 apply (blast dest: Notes_imp_used) 
@@ -481,8 +459,8 @@
      a delivery certificate exists, then @{term R}
      receives the necessary key.*}
 theorem R_guarantee:
-  "[|Crypt TTPSigKey S2TTP \<in> used evs;
-     S2TTP = Crypt TTPEncKey
+  "[|Crypt (priSK TTP) S2TTP \<in> used evs;
+     S2TTP = Crypt (pubEK TTP)
                {|Agent S, Number AO, Key K, Agent R, 
                  Hash {|Number cleartext, Nonce q, r, em|}|};
      hr = Hash {|Number cleartext, Nonce q, r, em|};
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/Event.thy	Mon May 05 18:22:01 2003 +0200
@@ -3,14 +3,14 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
-Theory of events for security protocols
-
 Datatype of events; function "spies"; freshness
 
 "bad" agents have been broken by the Spy; their private keys and internal
     stores are visible to him
 *)
 
+header{*Theory of Events for Security Protocols*}
+
 theory Event = Message:
 
 consts  (*Initial states of agents -- parameter of the construction*)
@@ -99,10 +99,9 @@
 
 subsection{*Function @{term knows}*}
 
-text{*Simplifying   @term{"parts (insert X (knows Spy evs))
-      = parts {X} \<union> parts (knows Spy evs)"}.  The general case loops.*)
-
-text{*This version won't loop with the simplifier.*}
+(*Simplifying   
+ parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
+  This version won't loop with the simplifier.*)
 lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
 
 lemma knows_Spy_Says [simp]:
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/Message.thy	Mon May 05 18:22:01 2003 +0200
@@ -7,6 +7,8 @@
 Inductive relations "parts", "analz" and "synth"
 *)
 
+header{*Theory of Agents and Messages for Security Protocols*}
+
 theory Message = Main:
 
 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/NS_Public.thy
--- a/src/HOL/Auth/NS_Public.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Mon May 05 18:22:01 2003 +0200
@@ -7,6 +7,8 @@
 Version incorporating Lowe's fix (inclusion of B's identity in round 2).
 *)
 
+header{*Verifying the Needham-Schroeder-Lowe Public-Key Protocol*}
+
 theory NS_Public = Public:
 
 consts  ns_public  :: "event list set"
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/NS_Public_Bad.thy
--- a/src/HOL/Auth/NS_Public_Bad.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Mon May 05 18:22:01 2003 +0200
@@ -11,6 +11,8 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
+header{*Verifying the Needham-Schroeder Public-Key Protocol*}
+
 theory NS_Public_Bad = Public:
 
 consts  ns_public  :: "event list set"
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Mon May 05 18:22:01 2003 +0200
@@ -240,7 +240,7 @@
 
 subsubsection{*Crucial secrecy property: Spy does not see the keys sent in msg NS2*}
 
-text{*Beware of [rule_format] and the universal quantifier!*}
+text{*Beware of @{text "[rule_format]"} and the universal quantifier!*}
 lemma secrecy_lemma:
      "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
                                       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/Public.thy	Mon May 05 18:22:01 2003 +0200
@@ -314,7 +314,7 @@
 apply (rule someI, fast)
 done
 
-subsection{*Specialized rewriting for the analz_image_... theorems*}
+subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
 
 lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
 by blast
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/Recur.thy	Mon May 05 18:22:01 2003 +0200
@@ -392,7 +392,8 @@
 apply blast
 txt{*Inductive step of respond*}
 apply (intro allI conjI impI, simp_all)
-txt{*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*}   
+txt{*by unicity, either @{term "B=Aa"} or @{term "B=A'"}, a contradiction
+     if @{term "B \<in> bad"}*}   
 apply (blast dest: unique_session_keys respond_certificate)
 apply (blast dest!: respond_certificate)
 apply (blast dest!: resp_analz_insert)
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/Shared.thy	Mon May 05 18:22:01 2003 +0200
@@ -242,7 +242,7 @@
      REPEAT_FIRST (resolve_tac [refl, conjI]))
 *}
 
-subsection{*Specialized rewriting for analz_insert_freshK*}
+subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
 
 lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x \<notin> A"
 by blast
@@ -250,7 +250,7 @@
 lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
 by blast
 
-lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
+lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key`(insert K KK) \<union> C"
 by blast
 
 (** Reverse the normal simplification of "image" to build up (not break down)
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/TLS.thy	Mon May 05 18:22:01 2003 +0200
@@ -39,6 +39,8 @@
 	Notes A {|Agent B, Nonce PMS|}.
 *)
 
+header{*The TLS Protocol: Transport Layer Security*}
+
 theory TLS = Public:
 
 constdefs
@@ -95,7 +97,8 @@
          "[| evsf \<in> tls;  X \<in> synth (analz (spies evsf)) |]
           ==> Says Spy B X # evsf \<in> tls"
 
-   SpyKeys: --{*The spy may apply PRF & sessionK to available nonces*}
+   SpyKeys: --{*The spy may apply @{term PRF} and @{term sessionK}
+                to available nonces*}
          "[| evsSK \<in> tls;
 	     {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
           ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
@@ -103,21 +106,21 @@
 
    ClientHello:
 	 --{*(7.4.1.2)
-	   PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
+	   PA represents @{text CLIENT_VERSION}, @{text CIPHER_SUITES} and @{text COMPRESSION_METHODS}.
 	   It is uninterpreted but will be confirmed in the FINISHED messages.
-	   NA is CLIENT RANDOM, while SID is SESSION_ID.
+	   NA is CLIENT RANDOM, while SID is @{text SESSION_ID}.
            UNIX TIME is omitted because the protocol doesn't use it.
-           May assume NA \<notin> range PRF because CLIENT RANDOM is 28 bytes
-	   while MASTER SECRET is 48 bytes*}
+           May assume @{term "NA \<notin> range PRF"} because CLIENT RANDOM is 
+           28 bytes while MASTER SECRET is 48 bytes*}
          "[| evsCH \<in> tls;  Nonce NA \<notin> used evsCH;  NA \<notin> range PRF |]
           ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
 	        # evsCH  \<in>  tls"
 
    ServerHello:
          --{*7.4.1.3 of the TLS Internet-Draft
-	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
+	   PB represents @{text CLIENT_VERSION}, @{text CIPHER_SUITE} and @{text COMPRESSION_METHOD}.
            SERVER CERTIFICATE (7.4.2) is always present.
-           CERTIFICATE_REQUEST (7.4.4) is implied.*}
+           @{text CERTIFICATE_REQUEST} (7.4.4) is implied.*}
          "[| evsSH \<in> tls;  Nonce NB \<notin> used evsSH;  NB \<notin> range PRF;
              Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
 	       \<in> set evsSH |]
@@ -131,7 +134,7 @@
          --{*CLIENT KEY EXCHANGE (7.4.7).
            The client, A, chooses PMS, the PREMASTER SECRET.
            She encrypts PMS using the supplied KB, which ought to be pubK B.
-           We assume PMS \<notin> range PRF because a clash betweem the PMS
+           We assume @{term "PMS \<notin> range PRF"} because a clash betweem the PMS
            and another MASTER SECRET is highly unlikely (even though
 	   both items have the same length, 48 bytes).
            The Note event records in the trace that she knows PMS
@@ -163,7 +166,7 @@
           rule's applying when the Spy has satisfied the "Says A B" by
           repaying messages sent by the true client; in that case, the
           Spy does not know PMS and could not send ClientFinished.  One
-          could simply put A\<noteq>Spy into the rule, but one should not
+          could simply put @{term "A\<noteq>Spy"} into the rule, but one should not
           expect the spy to be well-behaved.*}
          "[| evsCF \<in> tls;
 	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
@@ -196,7 +199,7 @@
 	--{*Having transmitted ClientFinished and received an identical
           message encrypted with serverK, the client stores the parameters
           needed to resume this session.  The "Notes A ..." premise is
-          used to prove Notes_master_imp_Crypt_PMS.*}
+          used to prove @{text Notes_master_imp_Crypt_PMS}.*}
          "[| evsCA \<in> tls;
 	     Notes A {|Agent B, Nonce PMS|} \<in> set evsCA;
 	     M = PRF(PMS,NA,NB);
@@ -212,7 +215,7 @@
 	--{*Having transmitted ServerFinished and received an identical
           message encrypted with clientK, the server stores the parameters
           needed to resume this session.  The "Says A'' B ..." premise is
-          used to prove Notes_master_imp_Crypt_PMS.*}
+          used to prove @{text Notes_master_imp_Crypt_PMS}.*}
          "[| evsSA \<in> tls;
 	     A \<noteq> B;
              Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSA;
@@ -226,8 +229,8 @@
              Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  \<in>  tls"
 
    ClientResume:
-         --{*If A recalls the SESSION_ID, then she sends a FINISHED message
-           using the new nonces and stored MASTER SECRET.*}
+         --{*If A recalls the @{text SESSION_ID}, then she sends a FINISHED
+             message using the new nonces and stored MASTER SECRET.*}
          "[| evsCR \<in> tls;
 	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
              Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCR;
@@ -239,8 +242,8 @@
               # evsCR  \<in>  tls"
 
    ServerResume:
-         --{*Resumption (7.3):  If B finds the SESSION_ID then he can send
-           a FINISHED message using the recovered MASTER SECRET*}
+         --{*Resumption (7.3):  If B finds the @{text SESSION_ID} then he can 
+             send a FINISHED message using the recovered MASTER SECRET*}
          "[| evsSR \<in> tls;
 	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
 	     Says B  A {|Nonce NB, Number SID, Number PB|} \<in> set evsSR;
@@ -254,8 +257,9 @@
    Oops:
          --{*The most plausible compromise is of an old session key.  Losing
            the MASTER SECRET or PREMASTER SECRET is more serious but
-           rather unlikely.  The assumption A \<noteq> Spy is essential: otherwise
-           the Spy could learn session keys merely by replaying messages!*}
+           rather unlikely.  The assumption @{term "A\<noteq>Spy"} is essential: 
+           otherwise the Spy could learn session keys merely by 
+           replaying messages!*}
          "[| evso \<in> tls;  A \<noteq> Spy;
 	     Says A B (Crypt (sessionK((NA,NB,M),role)) X) \<in> set evso |]
           ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso  \<in>  tls"
@@ -546,7 +550,7 @@
 
 subsection{*Secrecy Theorems*}
 
-text{*Key compromise lemma needed to prove analz_image_keys.
+text{*Key compromise lemma needed to prove @{term analz_image_keys}.
   No collection of keys can help the spy get new private keys.*}
 lemma analz_image_priK [rule_format]:
      "evs \<in> tls
@@ -647,7 +651,7 @@
   Converse fails; betraying M doesn't force the keys to be sent!
   The strong Oops condition can be weakened later by unicity reasoning,
   with some effort.
-  NO LONGER USED: see clientK_not_spied and serverK_not_spied*}
+  NO LONGER USED: see @{text clientK_not_spied} and @{text serverK_not_spied}*}
 lemma sessionK_not_spied:
      "[| \<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \<notin> set evs;
          Nonce M \<notin> analz (spies evs);  evs \<in> tls |]
@@ -676,7 +680,7 @@
 apply (blast dest: Notes_Crypt_parts_spies)
 apply (blast dest: Notes_Crypt_parts_spies)
 apply (blast dest: Notes_Crypt_parts_spies)
-txt{*ClientAccepts and ServerAccepts: because PMS \<notin> range PRF*}
+txt{*ClientAccepts and ServerAccepts: because @{term "PMS \<notin> range PRF"}*}
 apply force+
 done
 
@@ -787,8 +791,7 @@
 
 subsubsection{*Protocol goals: if A receives ServerFinished, then B is present
      and has used the quoted values PA, PB, etc.  Note that it is up to A
-     to compare PA with what she originally sent.
-***)
+     to compare PA with what she originally sent.*}
 
 text{*The mention of her name (A) in X assures A that B knows who she is.*}
 lemma TrustServerFinished [rule_format]:
@@ -861,8 +864,7 @@
 
 subsubsection{*Protocol goal: if B receives ClientFinished, and if B is able to
      check a CertVerify from A, then A has used the quoted
-     values PA, PB, etc.  Even this one requires A to be uncompromised.
-*}
+     values PA, PB, etc.  Even this one requires A to be uncompromised.*}
 lemma AuthClientFinished:
      "[| M = PRF(PMS,NA,NB);
          Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs;
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Mon May 05 18:22:01 2003 +0200
@@ -12,6 +12,8 @@
 This theory has the prototypical example of a secrecy relation, KeyCryptNonce.
 *)
 
+header{*The Yahalom Protocol*}
+
 theory Yahalom = Shared:
 
 consts  yahalom   :: "event list set"
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/Yahalom2.thy
--- a/src/HOL/Auth/Yahalom2.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/Yahalom2.thy	Mon May 05 18:22:01 2003 +0200
@@ -11,7 +11,7 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
-header{*Inductive Analysis of the Yahalom protocol, Variant 2*}
+header{*The Yahalom Protocol, Variant 2*}
 
 theory Yahalom2 = Shared:
 
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/Yahalom_Bad.thy
--- a/src/HOL/Auth/Yahalom_Bad.thy	Mon May 05 15:55:56 2003 +0200
+++ b/src/HOL/Auth/Yahalom_Bad.thy	Mon May 05 18:22:01 2003 +0200
@@ -10,6 +10,8 @@
 The issues are discussed in lcp's LICS 2000 invited lecture.
 *)
 
+header{*The Yahalom Protocol: A Flawed Version*}
+
 theory Yahalom_Bad = Shared:
 
 consts  yahalom   :: "event list set"
diff -r 8ab1d3e73bb1 -r 8fe7e12290e1 src/HOL/Auth/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/document/root.tex	Mon May 05 18:22:01 2003 +0200
@@ -0,0 +1,27 @@
+\documentclass[10pt,a4paper,twoside]{article}
+\usepackage{graphicx}
+\usepackage{latexsym,theorem}
+\usepackage{isabelle,isabellesym}
+\usepackage{pdfsetup}\urlstyle{rm}
+
+\begin{document}
+
+\pagestyle{headings}
+\pagenumbering{arabic}
+
+\title{Security Protocols}
+\author{Giampaolo Bella, Frederic Blanqui, Lawrence C. Paulson et al.}
+\maketitle
+
+\tableofcontents
+
+\begin{center}
+  \includegraphics[scale=0.5]{session_graph}  
+\end{center}
+
+\newpage
+
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+\end{document}