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