src/HOL/Auth/Guard/Proto.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/Proto.thy
     2     Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
     3     Copyright   2002  University of Cambridge
     4 *)
     5 
     6 section{*Other Protocol-Independent Results*}
     7 
     8 theory Proto imports Guard_Public begin
     9 
    10 subsection{*protocols*}
    11 
    12 type_synonym rule = "event set * event"
    13 
    14 abbreviation
    15   msg' :: "rule => msg" where
    16   "msg' R == msg (snd R)"
    17 
    18 type_synonym proto = "rule set"
    19 
    20 definition wdef :: "proto => bool" where
    21 "wdef p == ALL R k. R:p --> Number k:parts {msg' R}
    22 --> Number k:parts (msg`(fst R))"
    23 
    24 subsection{*substitutions*}
    25 
    26 record subs =
    27   agent   :: "agent => agent"
    28   nonce :: "nat => nat"
    29   nb    :: "nat => msg"
    30   key   :: "key => key"
    31 
    32 primrec apm :: "subs => msg => msg" where
    33   "apm s (Agent A) = Agent (agent s A)"
    34 | "apm s (Nonce n) = Nonce (nonce s n)"
    35 | "apm s (Number n) = nb s n"
    36 | "apm s (Key K) = Key (key s K)"
    37 | "apm s (Hash X) = Hash (apm s X)"
    38 | "apm s (Crypt K X) = (
    39 if (EX A. K = pubK A) then Crypt (pubK (agent s (agt K))) (apm s X)
    40 else if (EX A. K = priK A) then Crypt (priK (agent s (agt K))) (apm s X)
    41 else Crypt (key s K) (apm s X))"
    42 | "apm s {|X,Y|} = {|apm s X, apm s Y|}"
    43 
    44 lemma apm_parts: "X:parts {Y} ==> apm s X:parts {apm s Y}"
    45 apply (erule parts.induct, simp_all, blast)
    46 apply (erule parts.Fst)
    47 apply (erule parts.Snd)
    48 by (erule parts.Body)+
    49 
    50 lemma Nonce_apm [rule_format]: "Nonce n:parts {apm s X} ==>
    51 (ALL k. Number k:parts {X} --> Nonce n ~:parts {nb s k}) -->
    52 (EX k. Nonce k:parts {X} & nonce s k = n)"
    53 by (induct X, simp_all, blast)
    54 
    55 lemma wdef_Nonce: "[| Nonce n:parts {apm s X}; R:p; msg' R = X; wdef p;
    56 Nonce n ~:parts (apm s `(msg `(fst R))) |] ==>
    57 (EX k. Nonce k:parts {X} & nonce s k = n)"
    58 apply (erule Nonce_apm, unfold wdef_def)
    59 apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp simp: image_eq_UN)
    60 apply (drule_tac x=x in bspec, simp)
    61 apply (drule_tac Y="msg x" and s=s in apm_parts, simp)
    62 by (blast dest: parts_parts)
    63 
    64 primrec ap :: "subs => event => event" where
    65   "ap s (Says A B X) = Says (agent s A) (agent s B) (apm s X)"
    66 | "ap s (Gets A X) = Gets (agent s A) (apm s X)"
    67 | "ap s (Notes A X) = Notes (agent s A) (apm s X)"
    68 
    69 abbreviation
    70   ap' :: "subs => rule => event" where
    71   "ap' s R == ap s (snd R)"
    72 
    73 abbreviation
    74   apm' :: "subs => rule => msg" where
    75   "apm' s R == apm s (msg' R)"
    76 
    77 abbreviation
    78   priK' :: "subs => agent => key" where
    79   "priK' s A == priK (agent s A)"
    80 
    81 abbreviation
    82   pubK' :: "subs => agent => key" where
    83   "pubK' s A == pubK (agent s A)"
    84 
    85 subsection{*nonces generated by a rule*}
    86 
    87 definition newn :: "rule => nat set" where
    88 "newn R == {n. Nonce n:parts {msg (snd R)} & Nonce n ~:parts (msg`(fst R))}"
    89 
    90 lemma newn_parts: "n:newn R ==> Nonce (nonce s n):parts {apm' s R}"
    91 by (auto simp: newn_def dest: apm_parts)
    92 
    93 subsection{*traces generated by a protocol*}
    94 
    95 definition ok :: "event list => rule => subs => bool" where
    96 "ok evs R s == ((ALL x. x:fst R --> ap s x:set evs)
    97 & (ALL n. n:newn R --> Nonce (nonce s n) ~:used evs))"
    98 
    99 inductive_set
   100   tr :: "proto => event list set"
   101   for p :: proto
   102 where
   103 
   104   Nil [intro]: "[]:tr p"
   105 
   106 | Fake [intro]: "[| evsf:tr p; X:synth (analz (spies evsf)) |]
   107   ==> Says Spy B X # evsf:tr p"
   108 
   109 | Proto [intro]: "[| evs:tr p; R:p; ok evs R s |] ==> ap' s R # evs:tr p"
   110 
   111 subsection{*general properties*}
   112 
   113 lemma one_step_tr [iff]: "one_step (tr p)"
   114 apply (unfold one_step_def, clarify)
   115 by (ind_cases "ev # evs:tr p" for ev evs, auto)
   116 
   117 definition has_only_Says' :: "proto => bool" where
   118 "has_only_Says' p == ALL R. R:p --> is_Says (snd R)"
   119 
   120 lemma has_only_Says'D: "[| R:p; has_only_Says' p |]
   121 ==> (EX A B X. snd R = Says A B X)"
   122 by (unfold has_only_Says'_def is_Says_def, blast)
   123 
   124 lemma has_only_Says_tr [simp]: "has_only_Says' p ==> has_only_Says (tr p)"
   125 apply (unfold has_only_Says_def)
   126 apply (rule allI, rule allI, rule impI)
   127 apply (erule tr.induct)
   128 apply (auto simp: has_only_Says'_def ok_def)
   129 by (drule_tac x=a in spec, auto simp: is_Says_def)
   130 
   131 lemma has_only_Says'_in_trD: "[| has_only_Says' p; list @ ev # evs1 \<in> tr p |]
   132 ==> (EX A B X. ev = Says A B X)"
   133 by (drule has_only_Says_tr, auto)
   134 
   135 lemma ok_not_used: "[| Nonce n ~:used evs; ok evs R s;
   136 ALL x. x:fst R --> is_Says x |] ==> Nonce n ~:parts (apm s `(msg `(fst R)))"
   137 apply (unfold ok_def, clarsimp simp: image_eq_UN)
   138 apply (drule_tac x=x in spec, drule_tac x=x in spec)
   139 by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts)
   140 
   141 lemma ok_is_Says: "[| evs' @ ev # evs:tr p; ok evs R s; has_only_Says' p;
   142 R:p; x:fst R |] ==> is_Says x"
   143 apply (unfold ok_def is_Says_def, clarify)
   144 apply (drule_tac x=x in spec, simp)
   145 apply (subgoal_tac "one_step (tr p)")
   146 apply (drule trunc, simp, drule one_step_Cons, simp)
   147 apply (drule has_only_SaysD, simp+)
   148 by (clarify, case_tac x, auto)
   149 
   150 subsection{*types*}
   151 
   152 type_synonym keyfun = "rule => subs => nat => event list => key set"
   153 
   154 type_synonym secfun = "rule => nat => subs => key set => msg"
   155 
   156 subsection{*introduction of a fresh guarded nonce*}
   157 
   158 definition fresh :: "proto => rule => subs => nat => key set => event list
   159 => bool" where
   160 "fresh p R s n Ks evs == (EX evs1 evs2. evs = evs2 @ ap' s R # evs1
   161 & Nonce n ~:used evs1 & R:p & ok evs1 R s & Nonce n:parts {apm' s R}
   162 & apm' s R:guard n Ks)"
   163 
   164 lemma freshD: "fresh p R s n Ks evs ==> (EX evs1 evs2.
   165 evs = evs2 @ ap' s R # evs1 & Nonce n ~:used evs1 & R:p & ok evs1 R s
   166 & Nonce n:parts {apm' s R} & apm' s R:guard n Ks)"
   167 by (unfold fresh_def, blast)
   168 
   169 lemma freshI [intro]: "[| Nonce n ~:used evs1; R:p; Nonce n:parts {apm' s R};
   170 ok evs1 R s; apm' s R:guard n Ks |]
   171 ==> fresh p R s n Ks (list @ ap' s R # evs1)"
   172 by (unfold fresh_def, blast)
   173 
   174 lemma freshI': "[| Nonce n ~:used evs1; (l,r):p;
   175 Nonce n:parts {apm s (msg r)}; ok evs1 (l,r) s; apm s (msg r):guard n Ks |]
   176 ==> fresh p (l,r) s n Ks (evs2 @ ap s r # evs1)"
   177 by (drule freshI, simp+)
   178 
   179 lemma fresh_used: "[| fresh p R' s' n Ks evs; has_only_Says' p |]
   180 ==> Nonce n:used evs"
   181 apply (unfold fresh_def, clarify)
   182 apply (drule has_only_Says'D)
   183 by (auto intro: parts_used_app)
   184 
   185 lemma fresh_newn: "[| evs' @ ap' s R # evs:tr p; wdef p; has_only_Says' p;
   186 Nonce n ~:used evs; R:p; ok evs R s; Nonce n:parts {apm' s R} |]
   187 ==> EX k. k:newn R & nonce s k = n"
   188 apply (drule wdef_Nonce, simp+)
   189 apply (frule ok_not_used, simp+)
   190 apply (clarify, erule ok_is_Says, simp+)
   191 apply (clarify, rule_tac x=k in exI, simp add: newn_def image_eq_UN)
   192 apply (clarify, drule_tac Y="msg x" and s=s in apm_parts)
   193 apply (drule ok_not_used, simp+)
   194 by (clarify, erule ok_is_Says, simp_all add: image_eq_UN)
   195 
   196 lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs;
   197 Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev"
   198 apply (drule trunc, simp, ind_cases "ev # evs:tr p", simp)
   199 by (drule_tac x=X in in_sub, drule parts_sub, simp, simp, blast+)
   200 
   201 lemma fresh_ruleD: "[| fresh p R' s' n Ks evs; keys R' s' n evs <= Ks; wdef p;
   202 has_only_Says' p; evs:tr p; ALL R k s. nonce s k = n --> Nonce n:used evs -->
   203 R:p --> k:newn R --> Nonce n:parts {apm' s R} --> apm' s R:guard n Ks -->
   204 apm' s R:parts (spies evs) --> keys R s n evs <= Ks --> P |] ==> P"
   205 apply (frule fresh_used, simp)
   206 apply (unfold fresh_def, clarify)
   207 apply (drule_tac x=R' in spec)
   208 apply (drule fresh_newn, simp+, clarify)
   209 apply (drule_tac x=k in spec)
   210 apply (drule_tac x=s' in spec)
   211 apply (subgoal_tac "apm' s' R':parts (spies (evs2 @ ap' s' R' # evs1))")
   212 apply (case_tac R', drule has_only_Says'D, simp, clarsimp)
   213 apply (case_tac R', drule has_only_Says'D, simp, clarsimp)
   214 apply (rule_tac Y="apm s' X" in parts_parts, blast)
   215 by (rule parts.Inj, rule Says_imp_spies, simp, blast)
   216 
   217 subsection{*safe keys*}
   218 
   219 definition safe :: "key set => msg set => bool" where
   220 "safe Ks G == ALL K. K:Ks --> Key K ~:analz G"
   221 
   222 lemma safeD [dest]: "[| safe Ks G; K:Ks |] ==> Key K ~:analz G"
   223 by (unfold safe_def, blast)
   224 
   225 lemma safe_insert: "safe Ks (insert X G) ==> safe Ks G"
   226 by (unfold safe_def, blast)
   227 
   228 lemma Guard_safe: "[| Guard n Ks G; safe Ks G |] ==> Nonce n ~:analz G"
   229 by (blast dest: Guard_invKey)
   230 
   231 subsection{*guardedness preservation*}
   232 
   233 definition preserv :: "proto => keyfun => nat => key set => bool" where
   234 "preserv p keys n Ks == (ALL evs R' s' R s. evs:tr p -->
   235 Guard n Ks (spies evs) --> safe Ks (spies evs) --> fresh p R' s' n Ks evs -->
   236 keys R' s' n evs <= Ks --> R:p --> ok evs R s --> apm' s R:guard n Ks)"
   237 
   238 lemma preservD: "[| preserv p keys n Ks; evs:tr p; Guard n Ks (spies evs);
   239 safe Ks (spies evs); fresh p R' s' n Ks evs; R:p; ok evs R s;
   240 keys R' s' n evs <= Ks |] ==> apm' s R:guard n Ks"
   241 by (unfold preserv_def, blast)
   242 
   243 lemma preservD': "[| preserv p keys n Ks; evs:tr p; Guard n Ks (spies evs);
   244 safe Ks (spies evs); fresh p R' s' n Ks evs; (l,Says A B X):p;
   245 ok evs (l,Says A B X) s; keys R' s' n evs <= Ks |] ==> apm s X:guard n Ks"
   246 by (drule preservD, simp+)
   247 
   248 subsection{*monotonic keyfun*}
   249 
   250 definition monoton :: "proto => keyfun => bool" where
   251 "monoton p keys == ALL R' s' n ev evs. ev # evs:tr p -->
   252 keys R' s' n evs <= keys R' s' n (ev # evs)"
   253 
   254 lemma monotonD [dest]: "[| keys R' s' n (ev # evs) <= Ks; monoton p keys;
   255 ev # evs:tr p |] ==> keys R' s' n evs <= Ks"
   256 by (unfold monoton_def, blast)
   257 
   258 subsection{*guardedness theorem*}
   259 
   260 lemma Guard_tr [rule_format]: "[| evs:tr p; has_only_Says' p;
   261 preserv p keys n Ks; monoton p keys; Guard n Ks (initState Spy) |] ==>
   262 safe Ks (spies evs) --> fresh p R' s' n Ks evs --> keys R' s' n evs <= Ks -->
   263 Guard n Ks (spies evs)"
   264 apply (erule tr.induct)
   265 (* Nil *)
   266 apply simp
   267 (* Fake *)
   268 apply (clarify, drule freshD, clarsimp)
   269 apply (case_tac evs2)
   270 (* evs2 = [] *)
   271 apply (frule has_only_Says'D, simp)
   272 apply (clarsimp, blast)
   273 (* evs2 = aa # list *)
   274 apply (clarsimp, rule conjI)
   275 apply (blast dest: safe_insert)
   276 (* X:guard n Ks *)
   277 apply (rule in_synth_Guard, simp, rule Guard_analz)
   278 apply (blast dest: safe_insert)
   279 apply (drule safe_insert, simp add: safe_def)
   280 (* Proto *)
   281 apply (clarify, drule freshD, clarify)
   282 apply (case_tac evs2)
   283 (* evs2 = [] *)
   284 apply (frule has_only_Says'D, simp)
   285 apply (frule_tac R=R' in has_only_Says'D, simp)
   286 apply (case_tac R', clarsimp, blast)
   287 (* evs2 = ab # list *)
   288 apply (frule has_only_Says'D, simp)
   289 apply (clarsimp, rule conjI)
   290 apply (drule Proto, simp+, blast dest: safe_insert)
   291 (* apm s X:guard n Ks *)
   292 apply (frule Proto, simp+)
   293 apply (erule preservD', simp+)
   294 apply (blast dest: safe_insert)
   295 apply (blast dest: safe_insert)
   296 by (blast, simp, simp, blast)
   297 
   298 subsection{*useful properties for guardedness*}
   299 
   300 lemma newn_neq_used: "[| Nonce n:used evs; ok evs R s; k:newn R |]
   301 ==> n ~= nonce s k"
   302 by (auto simp: ok_def)
   303 
   304 lemma ok_Guard: "[| ok evs R s; Guard n Ks (spies evs); x:fst R; is_Says x |]
   305 ==> apm s (msg x):parts (spies evs) & apm s (msg x):guard n Ks"
   306 apply (unfold ok_def is_Says_def, clarify)
   307 apply (drule_tac x="Says A B X" in spec, simp)
   308 by (drule Says_imp_spies, auto intro: parts_parts)
   309 
   310 lemma ok_parts_not_new: "[| Y:parts (spies evs); Nonce (nonce s n):parts {Y};
   311 ok evs R s |] ==> n ~:newn R"
   312 by (auto simp: ok_def dest: not_used_not_spied parts_parts)
   313 
   314 subsection{*unicity*}
   315 
   316 definition uniq :: "proto => secfun => bool" where
   317 "uniq p secret == ALL evs R R' n n' Ks s s'. R:p --> R':p -->
   318 n:newn R --> n':newn R' --> nonce s n = nonce s' n' -->
   319 Nonce (nonce s n):parts {apm' s R} --> Nonce (nonce s n):parts {apm' s' R'} -->
   320 apm' s R:guard (nonce s n) Ks --> apm' s' R':guard (nonce s n) Ks -->
   321 evs:tr p --> Nonce (nonce s n) ~:analz (spies evs) -->
   322 secret R n s Ks:parts (spies evs) --> secret R' n' s' Ks:parts (spies evs) -->
   323 secret R n s Ks = secret R' n' s' Ks"
   324 
   325 lemma uniqD: "[| uniq p secret; evs: tr p; R:p; R':p; n:newn R; n':newn R';
   326 nonce s n = nonce s' n'; Nonce (nonce s n) ~:analz (spies evs);
   327 Nonce (nonce s n):parts {apm' s R}; Nonce (nonce s n):parts {apm' s' R'};
   328 secret R n s Ks:parts (spies evs); secret R' n' s' Ks:parts (spies evs);
   329 apm' s R:guard (nonce s n) Ks; apm' s' R':guard (nonce s n) Ks |] ==>
   330 secret R n s Ks = secret R' n' s' Ks"
   331 by (unfold uniq_def, blast)
   332 
   333 definition ord :: "proto => (rule => rule => bool) => bool" where
   334 "ord p inff == ALL R R'. R:p --> R':p --> ~ inff R R' --> inff R' R"
   335 
   336 lemma ordD: "[| ord p inff; ~ inff R R'; R:p; R':p |] ==> inff R' R"
   337 by (unfold ord_def, blast)
   338 
   339 definition uniq' :: "proto => (rule => rule => bool) => secfun => bool" where
   340 "uniq' p inff secret == ALL evs R R' n n' Ks s s'. R:p --> R':p -->
   341 inff R R' --> n:newn R --> n':newn R' --> nonce s n = nonce s' n' -->
   342 Nonce (nonce s n):parts {apm' s R} --> Nonce (nonce s n):parts {apm' s' R'} -->
   343 apm' s R:guard (nonce s n) Ks --> apm' s' R':guard (nonce s n) Ks -->
   344 evs:tr p --> Nonce (nonce s n) ~:analz (spies evs) -->
   345 secret R n s Ks:parts (spies evs) --> secret R' n' s' Ks:parts (spies evs) -->
   346 secret R n s Ks = secret R' n' s' Ks"
   347 
   348 lemma uniq'D: "[| uniq' p inff secret; evs: tr p; inff R R'; R:p; R':p; n:newn R;
   349 n':newn R'; nonce s n = nonce s' n'; Nonce (nonce s n) ~:analz (spies evs);
   350 Nonce (nonce s n):parts {apm' s R}; Nonce (nonce s n):parts {apm' s' R'};
   351 secret R n s Ks:parts (spies evs); secret R' n' s' Ks:parts (spies evs);
   352 apm' s R:guard (nonce s n) Ks; apm' s' R':guard (nonce s n) Ks |] ==>
   353 secret R n s Ks = secret R' n' s' Ks"
   354 by (unfold uniq'_def, blast)
   355 
   356 lemma uniq'_imp_uniq: "[| uniq' p inff secret; ord p inff |] ==> uniq p secret"
   357 apply (unfold uniq_def)
   358 apply (rule allI)+
   359 apply (case_tac "inff R R'")
   360 apply (blast dest: uniq'D)
   361 by (auto dest: ordD uniq'D intro: sym)
   362 
   363 subsection{*Needham-Schroeder-Lowe*}
   364 
   365 definition a :: agent where "a == Friend 0"
   366 definition b :: agent where "b == Friend 1"
   367 definition a' :: agent where "a' == Friend 2"
   368 definition b' :: agent where "b' == Friend 3"
   369 definition Na :: nat where "Na == 0"
   370 definition Nb :: nat where "Nb == 1"
   371 
   372 abbreviation
   373   ns1 :: rule where
   374   "ns1 == ({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
   375 
   376 abbreviation
   377   ns2 :: rule where
   378   "ns2 == ({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})},
   379     Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))"
   380 
   381 abbreviation
   382   ns3 :: rule where
   383   "ns3 == ({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}),
   384     Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})},
   385     Says a b (Crypt (pubK b) (Nonce Nb)))"
   386 
   387 inductive_set ns :: proto where
   388   [iff]: "ns1:ns"
   389 | [iff]: "ns2:ns"
   390 | [iff]: "ns3:ns"
   391 
   392 abbreviation (input)
   393   ns3a :: event where
   394   "ns3a == Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
   395 
   396 abbreviation (input)
   397   ns3b :: event where
   398   "ns3b == Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})"
   399 
   400 definition keys :: "keyfun" where
   401 "keys R' s' n evs == {priK' s' a, priK' s' b}"
   402 
   403 lemma "monoton ns keys"
   404 by (simp add: keys_def monoton_def)
   405 
   406 definition secret :: "secfun" where
   407 "secret R n s Ks ==
   408 (if R=ns1 then apm s (Crypt (pubK b) {|Nonce Na, Agent a|})
   409 else if R=ns2 then apm s (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})
   410 else Number 0)"
   411 
   412 definition inf :: "rule => rule => bool" where
   413 "inf R R' == (R=ns1 | (R=ns2 & R'~=ns1) | (R=ns3 & R'=ns3))"
   414 
   415 lemma inf_is_ord [iff]: "ord ns inf"
   416 apply (unfold ord_def inf_def)
   417 apply (rule allI)+
   418 apply (rule impI)
   419 apply (simp add: split_paired_all)
   420 by (rule impI, erule ns.cases, simp_all)+
   421 
   422 subsection{*general properties*}
   423 
   424 lemma ns_has_only_Says' [iff]: "has_only_Says' ns"
   425 apply (unfold has_only_Says'_def)
   426 apply (rule allI, rule impI)
   427 apply (simp add: split_paired_all)
   428 by (erule ns.cases, auto)
   429 
   430 lemma newn_ns1 [iff]: "newn ns1 = {Na}"
   431 by (simp add: newn_def)
   432 
   433 lemma newn_ns2 [iff]: "newn ns2 = {Nb}"
   434 by (auto simp: newn_def Na_def Nb_def)
   435 
   436 lemma newn_ns3 [iff]: "newn ns3 = {}"
   437 by (auto simp: newn_def)
   438 
   439 lemma ns_wdef [iff]: "wdef ns"
   440 by (auto simp: wdef_def elim: ns.cases)
   441 
   442 subsection{*guardedness for NSL*}
   443 
   444 lemma "uniq ns secret ==> preserv ns keys n Ks"
   445 apply (unfold preserv_def)
   446 apply (rule allI)+
   447 apply (rule impI, rule impI, rule impI, rule impI, rule impI)
   448 apply (erule fresh_ruleD, simp, simp, simp, simp)
   449 apply (rule allI)+
   450 apply (rule impI, rule impI, rule impI)
   451 apply (simp add: split_paired_all)
   452 apply (erule ns.cases)
   453 (* fresh with NS1 *)
   454 apply (rule impI, rule impI, rule impI, rule impI, rule impI, rule impI)
   455 apply (erule ns.cases)
   456 (* NS1 *)
   457 apply clarsimp
   458 apply (frule newn_neq_used, simp, simp)
   459 apply (rule No_Nonce, simp)
   460 (* NS2 *)
   461 apply clarsimp
   462 apply (frule newn_neq_used, simp, simp)
   463 apply (case_tac "nonce sa Na = nonce s Na")
   464 apply (frule Guard_safe, simp)
   465 apply (frule Crypt_guard_invKey, simp)
   466 apply (frule ok_Guard, simp, simp, simp, clarsimp)
   467 apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp)
   468 apply (frule_tac R=ns1 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
   469 apply (simp add: secret_def, simp add: secret_def, force, force)
   470 apply (simp add: secret_def keys_def, blast)
   471 apply (rule No_Nonce, simp)
   472 (* NS3 *)
   473 apply clarsimp
   474 apply (case_tac "nonce sa Na = nonce s Nb")
   475 apply (frule Guard_safe, simp)
   476 apply (frule Crypt_guard_invKey, simp)
   477 apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
   478 apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp)
   479 apply (frule_tac R=ns1 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
   480 apply (simp add: secret_def, simp add: secret_def, force, force)
   481 apply (simp add: secret_def, rule No_Nonce, simp)
   482 (* fresh with NS2 *)
   483 apply (rule impI, rule impI, rule impI, rule impI, rule impI, rule impI)
   484 apply (erule ns.cases)
   485 (* NS1 *)
   486 apply clarsimp
   487 apply (frule newn_neq_used, simp, simp)
   488 apply (rule No_Nonce, simp)
   489 (* NS2 *)
   490 apply clarsimp
   491 apply (frule newn_neq_used, simp, simp)
   492 apply (case_tac "nonce sa Nb = nonce s Na")
   493 apply (frule Guard_safe, simp)
   494 apply (frule Crypt_guard_invKey, simp)
   495 apply (frule ok_Guard, simp, simp, simp, clarsimp)
   496 apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp)
   497 apply (frule_tac R=ns2 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
   498 apply (simp add: secret_def, simp add: secret_def, force, force)
   499 apply (simp add: secret_def, rule No_Nonce, simp)
   500 (* NS3 *)
   501 apply clarsimp
   502 apply (case_tac "nonce sa Nb = nonce s Nb")
   503 apply (frule Guard_safe, simp)
   504 apply (frule Crypt_guard_invKey, simp)
   505 apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
   506 apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp)
   507 apply (frule_tac R=ns2 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
   508 apply (simp add: secret_def, simp add: secret_def, force, force)
   509 apply (simp add: secret_def keys_def, blast)
   510 apply (rule No_Nonce, simp)
   511 (* fresh with NS3 *)
   512 by simp
   513 
   514 subsection{*unicity for NSL*}
   515 
   516 lemma "uniq' ns inf secret"
   517 apply (unfold uniq'_def)
   518 apply (rule allI)+
   519 apply (simp add: split_paired_all)
   520 apply (rule impI, erule ns.cases)
   521 (* R = ns1 *)
   522 apply (rule impI, erule ns.cases)
   523 (* R' = ns1 *)
   524 apply (rule impI, rule impI, rule impI, rule impI)
   525 apply (rule impI, rule impI, rule impI, rule impI)
   526 apply (rule impI, erule tr.induct)
   527 (* Nil *)
   528 apply (simp add: secret_def)
   529 (* Fake *)
   530 apply (clarify, simp add: secret_def)
   531 apply (drule notin_analz_insert)
   532 apply (drule Crypt_insert_synth, simp, simp, simp)
   533 apply (drule Crypt_insert_synth, simp, simp, simp, simp)
   534 (* Proto *)
   535 apply (erule_tac P="ok evsa R sa" in rev_mp)
   536 apply (simp add: split_paired_all)
   537 apply (erule ns.cases)
   538 (* ns1 *)
   539 apply (clarify, simp add: secret_def)
   540 apply (erule disjE, erule disjE, clarsimp)
   541 apply (drule ok_parts_not_new, simp, simp, simp)
   542 apply (clarify, drule ok_parts_not_new, simp, simp, simp)
   543 (* ns2 *)
   544 apply (simp add: secret_def)
   545 (* ns3 *)
   546 apply (simp add: secret_def)
   547 (* R' = ns2 *)
   548 apply (rule impI, rule impI, rule impI, rule impI)
   549 apply (rule impI, rule impI, rule impI, rule impI)
   550 apply (rule impI, erule tr.induct)
   551 (* Nil *)
   552 apply (simp add: secret_def)
   553 (* Fake *)
   554 apply (clarify, simp add: secret_def)
   555 apply (drule notin_analz_insert)
   556 apply (drule Crypt_insert_synth, simp, simp, simp)
   557 apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp, simp)
   558 (* Proto *)
   559 apply (erule_tac P="ok evsa R sa" in rev_mp)
   560 apply (simp add: split_paired_all)
   561 apply (erule ns.cases)
   562 (* ns1 *)
   563 apply (clarify, simp add: secret_def)
   564 apply (drule_tac s=sa and n=Na in ok_parts_not_new, simp, simp, simp)
   565 (* ns2 *)
   566 apply (clarify, simp add: secret_def)
   567 apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp)
   568 (* ns3 *)
   569 apply (simp add: secret_def)
   570 (* R' = ns3 *)
   571 apply simp
   572 (* R = ns2 *)
   573 apply (rule impI, erule ns.cases)
   574 (* R' = ns1 *)
   575 apply (simp only: inf_def, blast)
   576 (* R' = ns2 *)
   577 apply (rule impI, rule impI, rule impI, rule impI)
   578 apply (rule impI, rule impI, rule impI, rule impI)
   579 apply (rule impI, erule tr.induct)
   580 (* Nil *)
   581 apply (simp add: secret_def)
   582 (* Fake *)
   583 apply (clarify, simp add: secret_def)
   584 apply (drule notin_analz_insert)
   585 apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp)
   586 apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp, simp)
   587 (* Proto *)
   588 apply (erule_tac P="ok evsa R sa" in rev_mp)
   589 apply (simp add: split_paired_all)
   590 apply (erule ns.cases)
   591 (* ns1 *)
   592 apply (simp add: secret_def)
   593 (* ns2 *)
   594 apply (clarify, simp add: secret_def)
   595 apply (erule disjE, erule disjE, clarsimp, clarsimp)
   596 apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp)
   597 apply (erule disjE, clarsimp)
   598 apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp)
   599 by (simp_all add: secret_def)
   600 
   601 end