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