src/HOL/Auth/NS_Public.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
     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 header{*Verifying the Needham-Schroeder-Lowe Public-Key Protocol*}
    11 
    12 theory NS_Public imports Public begin
    13 
    14 inductive_set ns_public :: "event list set"
    15   where 
    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 (pubEK 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 (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
    33           \<Longrightarrow> Says B A (Crypt (pubEK 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 (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
    39            Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
    40               \<in> set evs3\<rbrakk>
    41           \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
    42 
    43 declare knows_Spy_partsEs [elim]
    44 declare knows_Spy_partsEs [elim]
    45 declare analz_into_parts [dest]
    46 declare Fake_parts_insert_in_Un  [dest]
    47 declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    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], possibility)
    54 done
    55 
    56 (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
    57     sends messages containing X! **)
    58 
    59 (*Spy never sees another agent's private key! (unless it's bad at start)*)
    60 lemma Spy_see_priEK [simp]: 
    61       "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> parts (spies evs)) = (A \<in> bad)"
    62 by (erule ns_public.induct, auto)
    63 
    64 lemma Spy_analz_priEK [simp]: 
    65       "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> analz (spies evs)) = (A \<in> bad)"
    66 by auto
    67 
    68 subsection{*Authenticity properties obtained from NS2*}
    69 
    70 
    71 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
    72   is secret.  (Honest users generate fresh nonces.)*)
    73 lemma no_nonce_NS1_NS2 [rule_format]: 
    74       "evs \<in> ns_public 
    75        \<Longrightarrow> Crypt (pubEK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (spies evs) \<longrightarrow>
    76            Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>  
    77            Nonce NA \<in> analz (spies evs)"
    78 apply (erule ns_public.induct, simp_all)
    79 apply (blast intro: analz_insertI)+
    80 done
    81 
    82 (*Unicity for NS1: nonce NA identifies agents A and B*)
    83 lemma unique_NA: 
    84      "\<lbrakk>Crypt(pubEK B)  \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs);  
    85        Crypt(pubEK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs);  
    86        Nonce NA \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
    87       \<Longrightarrow> A=A' \<and> B=B'"
    88 apply (erule rev_mp, erule rev_mp, erule rev_mp)   
    89 apply (erule ns_public.induct, simp_all)
    90 (*Fake, NS1*)
    91 apply (blast intro: analz_insertI)+
    92 done
    93 
    94 
    95 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure
    96   The major premise "Says A B ..." makes it a dest-rule, so we use
    97   (erule rev_mp) rather than rule_format. *)
    98 theorem Spy_not_see_NA: 
    99       "\<lbrakk>Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
   100         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
   101        \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
   102 apply (erule rev_mp)   
   103 apply (erule ns_public.induct, simp_all, spy_analz)
   104 apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
   105 done
   106 
   107 
   108 (*Authentication for A: if she receives message 2 and has used NA
   109   to start a run, then B has sent message 2.*)
   110 lemma A_trusts_NS2_lemma [rule_format]: 
   111    "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
   112     \<Longrightarrow> Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   113 	Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
   114 	Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
   115 apply (erule ns_public.induct, simp_all)
   116 (*Fake, NS1*)
   117 apply (blast dest: Spy_not_see_NA)+
   118 done
   119 
   120 theorem A_trusts_NS2: 
   121      "\<lbrakk>Says A  B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;   
   122        Says B' A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
   123        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
   124       \<Longrightarrow> Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
   125 by (blast intro: A_trusts_NS2_lemma)
   126 
   127 
   128 (*If the encrypted message appears then it originated with Alice in NS1*)
   129 lemma B_trusts_NS1 [rule_format]:
   130      "evs \<in> ns_public                                         
   131       \<Longrightarrow> Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   132 	  Nonce NA \<notin> analz (spies evs) \<longrightarrow>
   133 	  Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
   134 apply (erule ns_public.induct, simp_all)
   135 (*Fake*)
   136 apply (blast intro!: analz_insertI)
   137 done
   138 
   139 
   140 subsection{*Authenticity properties obtained from NS2*}
   141 
   142 (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B 
   143   [unicity of B makes Lowe's fix work]
   144   [proof closely follows that for unique_NA] *)
   145 
   146 lemma unique_NB [dest]: 
   147      "\<lbrakk>Crypt(pubEK A)  \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts(spies evs);
   148        Crypt(pubEK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace> \<in> parts(spies evs);
   149        Nonce NB \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
   150       \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B'"
   151 apply (erule rev_mp, erule rev_mp, erule rev_mp)   
   152 apply (erule ns_public.induct, simp_all)
   153 (*Fake, NS2*)
   154 apply (blast intro: analz_insertI)+
   155 done
   156 
   157 
   158 (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
   159 theorem Spy_not_see_NB [dest]:
   160      "\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
   161        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
   162       \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
   163 apply (erule rev_mp)
   164 apply (erule ns_public.induct, simp_all, spy_analz)
   165 apply (blast intro: no_nonce_NS1_NS2)+
   166 done
   167 
   168 
   169 (*Authentication for B: if he receives message 3 and has used NB
   170   in message 2, then A has sent message 3.*)
   171 lemma B_trusts_NS3_lemma [rule_format]:
   172      "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk> \<Longrightarrow>
   173       Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   174       Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
   175       Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
   176 by (erule ns_public.induct, auto)
   177 
   178 theorem B_trusts_NS3:
   179      "\<lbrakk>Says B A  (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
   180        Says A' B (Crypt (pubEK B) (Nonce NB)) \<in> set evs;             
   181        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                    
   182       \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
   183 by (blast intro: B_trusts_NS3_lemma)
   184 
   185 subsection{*Overall guarantee for B*}
   186 
   187 (*If NS3 has been sent and the nonce NB agrees with the nonce B joined with
   188   NA, then A initiated the run using NA.*)
   189 theorem B_trusts_protocol:
   190      "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk> \<Longrightarrow>
   191       Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   192       Says B A  (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
   193       Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
   194 by (erule ns_public.induct, auto)
   195 
   196 end