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