src/HOL/Auth/Guard/Guard_NS_Public.thy
author wenzelm
Wed Sep 14 23:14:57 2005 +0200 (2005-09-14)
changeset 17394 a8c9ed3f9818
child 20768 1d478c2d621f
permissions -rw-r--r--
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
     1 (******************************************************************************
     2 incorporating Lowe's fix (inclusion of B's identity in round 2)
     3 
     4 date: march 2002
     5 author: Frederic Blanqui
     6 email: blanqui@lri.fr
     7 webpage: http://www.lri.fr/~blanqui/
     8 
     9 University of Cambridge, Computer Laboratory
    10 William Gates Building, JJ Thomson Avenue
    11 Cambridge CB3 0FD, United Kingdom
    12 ******************************************************************************)
    13 
    14 header{*Needham-Schroeder-Lowe Public-Key Protocol*}
    15 
    16 theory Guard_NS_Public imports Guard_Public begin
    17 
    18 subsection{*messages used in the protocol*}
    19 
    20 syntax ns1 :: "agent => agent => nat => event"
    21 
    22 translations "ns1 A B NA" => "Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
    23 
    24 syntax ns1' :: "agent => agent => agent => nat => event"
    25 
    26 translations "ns1' A' A B NA"
    27 => "Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
    28 
    29 syntax ns2 :: "agent => agent => nat => nat => event"
    30 
    31 translations "ns2 B A NA NB"
    32 => "Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
    33 
    34 syntax ns2' :: "agent => agent => agent => nat => nat => event"
    35 
    36 translations "ns2' B' B A NA NB"
    37 => "Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
    38 
    39 syntax ns3 :: "agent => agent => nat => event"
    40 
    41 translations "ns3 A B NB" => "Says A B (Crypt (pubK B) (Nonce NB))"
    42 
    43 subsection{*definition of the protocol*}
    44 
    45 consts nsp :: "event list set"
    46 
    47 inductive nsp
    48 intros
    49 
    50 Nil: "[]:nsp"
    51 
    52 Fake: "[| evs:nsp; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs : nsp"
    53 
    54 NS1: "[| evs1:nsp; Nonce NA ~:used evs1 |] ==> ns1 A B NA # evs1 : nsp"
    55 
    56 NS2: "[| evs2:nsp; Nonce NB ~:used evs2; ns1' A' A B NA:set evs2 |] ==>
    57 ns2 B A NA NB # evs2:nsp"
    58 
    59 NS3: "[| evs3:nsp; ns1 A B NA:set evs3; ns2' B' B A NA NB:set evs3 |] ==>
    60 ns3 A B NB # evs3:nsp"
    61 
    62 subsection{*declarations for tactics*}
    63 
    64 declare knows_Spy_partsEs [elim]
    65 declare Fake_parts_insert [THEN subsetD, dest]
    66 declare initState.simps [simp del]
    67 
    68 subsection{*general properties of nsp*}
    69 
    70 lemma nsp_has_no_Gets: "evs:nsp ==> ALL A X. Gets A X ~:set evs"
    71 by (erule nsp.induct, auto)
    72 
    73 lemma nsp_is_Gets_correct [iff]: "Gets_correct nsp"
    74 by (auto simp: Gets_correct_def dest: nsp_has_no_Gets)
    75 
    76 lemma nsp_is_one_step [iff]: "one_step nsp"
    77 by (unfold one_step_def, clarify, ind_cases "ev#evs:nsp", auto)
    78 
    79 lemma nsp_has_only_Says' [rule_format]: "evs:nsp ==>
    80 ev:set evs --> (EX A B X. ev=Says A B X)"
    81 by (erule nsp.induct, auto)
    82 
    83 lemma nsp_has_only_Says [iff]: "has_only_Says nsp"
    84 by (auto simp: has_only_Says_def dest: nsp_has_only_Says')
    85 
    86 lemma nsp_is_regular [iff]: "regular nsp"
    87 apply (simp only: regular_def, clarify)
    88 by (erule nsp.induct, auto simp: initState.simps knows.simps)
    89 
    90 subsection{*nonce are used only once*}
    91 
    92 lemma NA_is_uniq [rule_format]: "evs:nsp ==>
    93 Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
    94 --> Crypt (pubK B') {|Nonce NA, Agent A'|}:parts (spies evs)
    95 --> Nonce NA ~:analz (spies evs) --> A=A' & B=B'"
    96 apply (erule nsp.induct, simp_all)
    97 by (blast intro: analz_insertI)+
    98 
    99 lemma no_Nonce_NS1_NS2 [rule_format]: "evs:nsp ==>
   100 Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs)
   101 --> Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
   102 --> Nonce NA:analz (spies evs)"
   103 apply (erule nsp.induct, simp_all)
   104 by (blast intro: analz_insertI)+
   105 
   106 lemma no_Nonce_NS1_NS2' [rule_format]:
   107 "[| Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs);
   108 Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs); evs:nsp |]
   109 ==> Nonce NA:analz (spies evs)"
   110 by (rule no_Nonce_NS1_NS2, auto)
   111  
   112 lemma NB_is_uniq [rule_format]: "evs:nsp ==>
   113 Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
   114 --> Crypt (pubK A') {|Nonce NA', Nonce NB, Agent B'|}:parts (spies evs)
   115 --> Nonce NB ~:analz (spies evs) --> A=A' & B=B' & NA=NA'"
   116 apply (erule nsp.induct, simp_all)
   117 by (blast intro: analz_insertI)+
   118 
   119 subsection{*guardedness of NA*}
   120 
   121 lemma ns1_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
   122 ns1 A B NA:set evs --> Guard NA {priK A,priK B} (spies evs)"
   123 apply (erule nsp.induct)
   124 (* Nil *)
   125 apply simp_all
   126 (* Fake *)
   127 apply safe
   128 apply (erule in_synth_Guard, erule Guard_analz, simp)
   129 (* NS1 *)
   130 apply blast
   131 apply blast
   132 apply blast
   133 apply (drule Nonce_neq, simp+, rule No_Nonce, simp)
   134 (* NS2 *)
   135 apply (frule_tac A=A in Nonce_neq, simp+)
   136 apply (case_tac "NAa=NA")
   137 apply (drule Guard_Nonce_analz, simp+)
   138 apply (drule Says_imp_knows_Spy)+
   139 apply (drule_tac B=B and A'=Aa in NA_is_uniq, auto)
   140 (* NS3 *)
   141 apply (case_tac "NB=NA", clarify)
   142 apply (drule Guard_Nonce_analz, simp+)
   143 apply (drule Says_imp_knows_Spy)+
   144 by (drule no_Nonce_NS1_NS2, auto)
   145 
   146 subsection{*guardedness of NB*}
   147 
   148 lemma ns2_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
   149 ns2 B A NA NB:set evs --> Guard NB {priK A,priK B} (spies evs)" 
   150 apply (erule nsp.induct)
   151 (* Nil *)
   152 apply simp_all
   153 (* Fake *)
   154 apply safe
   155 apply (erule in_synth_Guard, erule Guard_analz, simp)
   156 (* NS1 *)
   157 apply (frule Nonce_neq, simp+, blast, rule No_Nonce, simp)
   158 (* NS2 *)
   159 apply blast
   160 apply blast
   161 apply blast
   162 apply (frule_tac A=B and n=NB in Nonce_neq, simp+)
   163 apply (case_tac "NAa=NB")
   164 apply (drule Guard_Nonce_analz, simp+)
   165 apply (drule Says_imp_knows_Spy)+
   166 apply (drule no_Nonce_NS1_NS2, auto)
   167 (* NS3 *)
   168 apply (case_tac "NBa=NB", clarify)
   169 apply (drule Guard_Nonce_analz, simp+)
   170 apply (drule Says_imp_knows_Spy)+
   171 by (drule_tac A=Aa and A'=A in NB_is_uniq, auto)
   172 
   173 subsection{*Agents' Authentication*}
   174 
   175 lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
   176 Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
   177 --> Nonce NA ~:analz (spies evs) --> ns1 A B NA:set evs"
   178 apply (erule nsp.induct, simp_all)
   179 by (blast intro: analz_insertI)+
   180 
   181 lemma A_trusts_NS2: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns1 A B NA:set evs
   182 --> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
   183 --> ns2 B A NA NB:set evs"
   184 apply (erule nsp.induct, simp_all, safe)
   185 apply (frule_tac B=B in ns1_imp_Guard, simp+)
   186 apply (drule Guard_Nonce_analz, simp+, blast)
   187 apply (frule_tac B=B in ns1_imp_Guard, simp+)
   188 apply (drule Guard_Nonce_analz, simp+, blast)
   189 apply (frule_tac B=B in ns1_imp_Guard, simp+)
   190 by (drule Guard_Nonce_analz, simp+, blast+)
   191 
   192 lemma B_trusts_NS3: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns2 B A NA NB:set evs
   193 --> Crypt (pubK B) (Nonce NB):parts (spies evs) --> ns3 A B NB:set evs"
   194 apply (erule nsp.induct, simp_all, safe)
   195 apply (frule_tac B=B in ns2_imp_Guard, simp+)
   196 apply (drule Guard_Nonce_analz, simp+, blast)
   197 apply (frule_tac B=B in ns2_imp_Guard, simp+)
   198 apply (drule Guard_Nonce_analz, simp+, blast)
   199 apply (frule_tac B=B in ns2_imp_Guard, simp+)
   200 apply (drule Guard_Nonce_analz, simp+, blast, blast)
   201 apply (frule_tac B=B in ns2_imp_Guard, simp+)
   202 by (drule Guard_Nonce_analz, auto dest: Says_imp_knows_Spy NB_is_uniq)
   203 
   204 end