src/HOL/Auth/NS_Public_Bad.thy
author huffman
Sat Jun 06 09:11:12 2009 -0700 (2009-06-06)
changeset 31488 5691ccb8d6b5
parent 23746 a455e69c31cc
child 32960 69916a850301
permissions -rw-r--r--
generalize tendsto to class topological_space
     1 (*  Title:      HOL/Auth/NS_Public_Bad
     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 Flawed version, vulnerable to Lowe's attack.
     8 
     9 From page 260 of
    10   Burrows, Abadi and Needham.  A Logic of Authentication.
    11   Proc. Royal Soc. 426 (1989)
    12 *)
    13 
    14 header{*Verifying the Needham-Schroeder Public-Key Protocol*}
    15 
    16 theory NS_Public_Bad imports Public begin
    17 
    18 inductive_set ns_public :: "event list set"
    19   where
    20          (*Initial trace is empty*)
    21    Nil:  "[] \<in> ns_public"
    22 
    23          (*The spy MAY say anything he CAN say.  We do not expect him to
    24            invent new nonces here, but he can also use NS1.  Common to
    25            all similar protocols.*)
    26  | Fake: "\<lbrakk>evsf \<in> ns_public;  X \<in> synth (analz (spies evsf))\<rbrakk>
    27           \<Longrightarrow> Says Spy B X  # evsf \<in> ns_public"
    28 
    29          (*Alice initiates a protocol run, sending a nonce to Bob*)
    30  | NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
    31           \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
    32                 # evs1  \<in>  ns_public"
    33 
    34          (*Bob responds to Alice's message with a further nonce*)
    35  | NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
    36            Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
    37           \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
    38                 # evs2  \<in>  ns_public"
    39 
    40          (*Alice proves her existence by sending NB back to Bob.*)
    41  | NS3:  "\<lbrakk>evs3 \<in> ns_public;
    42            Says A  B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
    43            Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
    44           \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
    45 
    46 declare knows_Spy_partsEs [elim]
    47 declare analz_into_parts [dest]
    48 declare Fake_parts_insert_in_Un  [dest]
    49 declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    50 
    51 (*A "possibility property": there are traces that reach the end*)
    52 lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
    53 apply (intro exI bexI)
    54 apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, 
    55                                    THEN ns_public.NS3])
    56 by possibility
    57 
    58 
    59 (**** Inductive proofs about ns_public ****)
    60 
    61 (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
    62     sends messages containing X! **)
    63 
    64 (*Spy never sees another agent's private key! (unless it's bad at start)*)
    65 lemma Spy_see_priEK [simp]: 
    66       "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> parts (spies evs)) = (A \<in> bad)"
    67 by (erule ns_public.induct, auto)
    68 
    69 lemma Spy_analz_priEK [simp]: 
    70       "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> analz (spies evs)) = (A \<in> bad)"
    71 by auto
    72 
    73 
    74 (*** Authenticity properties obtained from NS2 ***)
    75 
    76 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
    77   is secret.  (Honest users generate fresh nonces.)*)
    78 lemma no_nonce_NS1_NS2 [rule_format]: 
    79       "evs \<in> ns_public 
    80        \<Longrightarrow> Crypt (pubEK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies evs) \<longrightarrow>
    81            Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>  
    82            Nonce NA \<in> analz (spies evs)"
    83 apply (erule ns_public.induct, simp_all)
    84 apply (blast intro: analz_insertI)+
    85 done
    86 
    87 
    88 (*Unicity for NS1: nonce NA identifies agents A and B*)
    89 lemma unique_NA: 
    90      "\<lbrakk>Crypt(pubEK B)  \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs);  
    91        Crypt(pubEK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs);  
    92        Nonce NA \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
    93       \<Longrightarrow> A=A' \<and> B=B'"
    94 apply (erule rev_mp, erule rev_mp, erule rev_mp)   
    95 apply (erule ns_public.induct, simp_all)
    96 (*Fake, NS1*)
    97 apply (blast intro!: analz_insertI)+
    98 done
    99 
   100 
   101 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure
   102   The major premise "Says A B ..." makes it a dest-rule, so we use
   103   (erule rev_mp) rather than rule_format. *)
   104 theorem Spy_not_see_NA: 
   105       "\<lbrakk>Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
   106         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
   107        \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
   108 apply (erule rev_mp)   
   109 apply (erule ns_public.induct, simp_all, spy_analz)
   110 apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
   111 done
   112 
   113 
   114 (*Authentication for A: if she receives message 2 and has used NA
   115   to start a run, then B has sent message 2.*)
   116 lemma A_trusts_NS2_lemma [rule_format]: 
   117    "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
   118     \<Longrightarrow> Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   119 	Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
   120 	Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
   121 apply (erule ns_public.induct)
   122 apply (auto dest: Spy_not_see_NA unique_NA)
   123 done
   124 
   125 theorem A_trusts_NS2: 
   126      "\<lbrakk>Says A  B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;   
   127        Says B' A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
   128        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
   129       \<Longrightarrow> Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
   130 by (blast intro: A_trusts_NS2_lemma)
   131 
   132 
   133 (*If the encrypted message appears then it originated with Alice in NS1*)
   134 lemma B_trusts_NS1 [rule_format]:
   135      "evs \<in> ns_public                                         
   136       \<Longrightarrow> Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   137 	  Nonce NA \<notin> analz (spies evs) \<longrightarrow>
   138 	  Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
   139 apply (erule ns_public.induct, simp_all)
   140 (*Fake*)
   141 apply (blast intro!: analz_insertI)
   142 done
   143 
   144 
   145 
   146 (*** Authenticity properties obtained from NS2 ***)
   147 
   148 (*Unicity for NS2: nonce NB identifies nonce NA and agent A
   149   [proof closely follows that for unique_NA] *)
   150 lemma unique_NB [dest]: 
   151      "\<lbrakk>Crypt(pubEK A)  \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts(spies evs);
   152        Crypt(pubEK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies evs);
   153        Nonce NB \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
   154      \<Longrightarrow> A=A' \<and> NA=NA'"
   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 (*NB remains secret PROVIDED Alice never responds with round 3*)
   163 theorem Spy_not_see_NB [dest]:
   164      "\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;   
   165        \<forall>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<notin> set evs;       
   166        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                      
   167      \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
   168 apply (erule rev_mp, erule rev_mp)
   169 apply (erule ns_public.induct, simp_all, spy_analz)
   170 apply (simp_all add: all_conj_distrib) (*speeds up the next step*)
   171 apply (blast intro: no_nonce_NS1_NS2)+
   172 done
   173 
   174 
   175 (*Authentication for B: if he receives message 3 and has used NB
   176   in message 2, then A has sent message 3--to somebody....*)
   177 
   178 lemma B_trusts_NS3_lemma [rule_format]:
   179      "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                    
   180       \<Longrightarrow> Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   181           Says B A  (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow>
   182           (\<exists>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<in> set evs)"
   183 apply (erule ns_public.induct, auto)
   184 by (blast intro: no_nonce_NS1_NS2)+
   185 
   186 theorem B_trusts_NS3:
   187      "\<lbrakk>Says B A  (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
   188        Says A' B (Crypt (pubEK B) (Nonce NB)) \<in> set evs;             
   189        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                    
   190       \<Longrightarrow> \<exists>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<in> set evs"
   191 by (blast intro: B_trusts_NS3_lemma)
   192 
   193 
   194 (*Can we strengthen the secrecy theorem Spy_not_see_NB?  NO*)
   195 lemma "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>            
   196        \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs  
   197            \<longrightarrow> Nonce NB \<notin> analz (spies evs)"
   198 apply (erule ns_public.induct, simp_all, spy_analz)
   199 (*NS1: by freshness*)
   200 apply blast
   201 (*NS2: by freshness and unicity of NB*)
   202 apply (blast intro: no_nonce_NS1_NS2)
   203 (*NS3: unicity of NB identifies A and NA, but not B*)
   204 apply clarify
   205 apply (frule_tac A' = A in 
   206        Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
   207 apply (rename_tac C B' evs3)
   208 txt{*This is the attack!
   209 @{subgoals[display,indent=0,margin=65]}
   210 *}
   211 oops
   212 
   213 (*
   214 THIS IS THE ATTACK!
   215 Level 8
   216 !!evs. \<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
   217        \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow>
   218            Nonce NB \<notin> analz (spies evs)
   219  1. !!C B' evs3.
   220        \<lbrakk>A \<notin> bad; B \<notin> bad; evs3 \<in> ns_public
   221         Says A C (Crypt (pubEK C) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
   222         Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3; 
   223         C \<in> bad;
   224         Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3;
   225         Nonce NB \<notin> analz (spies evs3)\<rbrakk>
   226        \<Longrightarrow> False
   227 *)
   228 
   229 end