src/HOL/Auth/NS_Public.thy
author paulson
Sat Aug 17 14:55:08 2002 +0200 (2002-08-17)
changeset 13507 febb8e5d2a9d
parent 11366 b42287eb20cf
child 13922 75ae4244a596
permissions -rw-r--r--
tidying of Isar scripts
     1 (*  Title:      HOL/Auth/NS_Public
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
     7 Version incorporating Lowe's fix (inclusion of B's identity in round 2).
     8 *)
     9 
    10 theory NS_Public = Public:
    11 
    12 consts  ns_public  :: "event list set"
    13 
    14 inductive ns_public
    15   intros 
    16          (*Initial trace is empty*)
    17    Nil:  "[] \<in> ns_public"
    18 
    19          (*The spy MAY say anything he CAN say.  We do not expect him to
    20            invent new nonces here, but he can also use NS1.  Common to
    21            all similar protocols.*)
    22    Fake: "\<lbrakk>evsf \<in> ns_public;  X \<in> synth (analz (spies evsf))\<rbrakk>
    23           \<Longrightarrow> Says Spy B X  # evsf \<in> ns_public"
    24 
    25          (*Alice initiates a protocol run, sending a nonce to Bob*)
    26    NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
    27           \<Longrightarrow> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
    28                  # evs1  \<in>  ns_public"
    29 
    30          (*Bob responds to Alice's message with a further nonce*)
    31    NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
    32            Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
    33           \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
    34                 # evs2  \<in>  ns_public"
    35 
    36          (*Alice proves her existence by sending NB back to Bob.*)
    37    NS3:  "\<lbrakk>evs3 \<in> ns_public;
    38            Says A  B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
    39            Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
    40               \<in> set evs3\<rbrakk>
    41           \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public"
    42 
    43 declare knows_Spy_partsEs [elim]
    44 declare analz_subset_parts [THEN subsetD, dest]
    45 declare Fake_parts_insert [THEN subsetD, dest]
    46 declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    47 
    48 (*A "possibility property": there are traces that reach the end*)
    49 lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
    50 apply (intro exI bexI)
    51 apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, 
    52                                    THEN ns_public.NS3])
    53 by possibility
    54 
    55 
    56 (**** Inductive proofs about ns_public ****)
    57 
    58 (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
    59     sends messages containing X! **)
    60 
    61 (*Spy never sees another agent's private key! (unless it's bad at start)*)
    62 lemma Spy_see_priK [simp]: 
    63       "evs \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
    64 by (erule ns_public.induct, auto)
    65 
    66 lemma Spy_analz_priK [simp]: 
    67       "evs \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
    68 by auto
    69 
    70 
    71 (*** Authenticity properties obtained from NS2 ***)
    72 
    73 
    74 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
    75   is secret.  (Honest users generate fresh nonces.)*)
    76 lemma no_nonce_NS1_NS2 [rule_format]: 
    77       "evs \<in> ns_public 
    78        \<Longrightarrow> Crypt (pubK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (spies evs) \<longrightarrow>
    79            Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>  
    80            Nonce NA \<in> analz (spies evs)"
    81 apply (erule ns_public.induct, simp_all)
    82 apply (blast intro: analz_insertI)+
    83 done
    84 
    85 (*Unicity for NS1: nonce NA identifies agents A and B*)
    86 lemma unique_NA: 
    87      "\<lbrakk>Crypt(pubK B)  \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs);  
    88        Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs);  
    89        Nonce NA \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
    90       \<Longrightarrow> A=A' \<and> B=B'"
    91 apply (erule rev_mp, erule rev_mp, erule rev_mp)   
    92 apply (erule ns_public.induct, simp_all)
    93 (*Fake, NS1*)
    94 apply (blast intro: analz_insertI)+
    95 done
    96 
    97 
    98 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure
    99   The major premise "Says A B ..." makes it a dest-rule, so we use
   100   (erule rev_mp) rather than rule_format. *)
   101 theorem Spy_not_see_NA: 
   102       "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
   103         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
   104        \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
   105 apply (erule rev_mp)   
   106 apply (erule ns_public.induct, simp_all, spy_analz)
   107 apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
   108 done
   109 
   110 
   111 (*Authentication for A: if she receives message 2 and has used NA
   112   to start a run, then B has sent message 2.*)
   113 lemma A_trusts_NS2_lemma [rule_format]: 
   114    "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
   115     \<Longrightarrow> Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   116 	Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
   117 	Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
   118 apply (erule ns_public.induct, simp_all)
   119 (*Fake, NS1*)
   120 apply (blast dest: Spy_not_see_NA)+
   121 done
   122 
   123 theorem A_trusts_NS2: 
   124      "\<lbrakk>Says A  B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;   
   125        Says B' A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
   126        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
   127       \<Longrightarrow> Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
   128 by (blast intro: A_trusts_NS2_lemma)
   129 
   130 
   131 (*If the encrypted message appears then it originated with Alice in NS1*)
   132 lemma B_trusts_NS1 [rule_format]:
   133      "evs \<in> ns_public                                         
   134       \<Longrightarrow> Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   135 	  Nonce NA \<notin> analz (spies evs) \<longrightarrow>
   136 	  Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
   137 apply (erule ns_public.induct, simp_all)
   138 (*Fake*)
   139 apply (blast intro!: analz_insertI)
   140 done
   141 
   142 
   143 
   144 (*** Authenticity properties obtained from NS2 ***)
   145 
   146 (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B 
   147   [unicity of B makes Lowe's fix work]
   148   [proof closely follows that for unique_NA] *)
   149 
   150 lemma unique_NB [dest]: 
   151      "\<lbrakk>Crypt(pubK A)  \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts(spies evs);
   152        Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace> \<in> parts(spies evs);
   153        Nonce NB \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
   154       \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B'"
   155 apply (erule rev_mp, erule rev_mp, erule rev_mp)   
   156 apply (erule ns_public.induct, simp_all)
   157 (*Fake, NS2*)
   158 apply (blast intro: analz_insertI)+
   159 done
   160 
   161 
   162 (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
   163 theorem Spy_not_see_NB [dest]:
   164      "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
   165        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
   166       \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
   167 apply (erule rev_mp)
   168 apply (erule ns_public.induct, simp_all, spy_analz)
   169 apply (blast intro: no_nonce_NS1_NS2)+
   170 done
   171 
   172 
   173 (*Authentication for B: if he receives message 3 and has used NB
   174   in message 2, then A has sent message 3.*)
   175 lemma B_trusts_NS3_lemma [rule_format]:
   176      "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk> \<Longrightarrow>
   177       Crypt (pubK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   178       Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
   179       Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
   180 by (erule ns_public.induct, auto)
   181 
   182 theorem B_trusts_NS3:
   183      "\<lbrakk>Says B A  (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
   184        Says A' B (Crypt (pubK B) (Nonce NB)) \<in> set evs;             
   185        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                    
   186       \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
   187 by (blast intro: B_trusts_NS3_lemma)
   188 
   189 (*** Overall guarantee for B ***)
   190 
   191 
   192 (*If NS3 has been sent and the nonce NB agrees with the nonce B joined with
   193   NA, then A initiated the run using NA.*)
   194 theorem B_trusts_protocol:
   195      "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk> \<Longrightarrow>
   196       Crypt (pubK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   197       Says B A  (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
   198       Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
   199 by (erule ns_public.induct, auto)
   200 
   201 end