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