Quelle Proto.thy Sprache: Isabelle

(*  Title:      HOL/Auth/Guard/Proto.thy
    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
    Copyright   2002  University of Cambridge
*)

section\<open>Other Protocol-Independent Results\<close>

theory Proto imports Guard_Public begin

subsection\<open>protocols\<close>

type_synonym rule = "event set * event"

abbreviation
  msg' :: "rule => msg" where
  "msg' R == msg (snd R)"

type_synonym proto = "rule set"

definition wdef :: "proto => bool" where
"wdef p \ \R k. R \ p \ Number k \ parts {msg' R}
\<longrightarrow> Number k \<in> parts (msg`(fst R))"

subsection\<open>substitutions\<close>

record subs =
  agent   :: "agent => agent"
  nonce :: "nat => nat"
  nb    :: "nat => msg"
  key   :: "key => key"

primrec apm :: "subs => msg => msg" where
  "apm s (Agent A) = Agent (agent s A)"
| "apm s (Nonce n) = Nonce (nonce s n)"
| "apm s (Number n) = nb s n"
| "apm s (Key K) = Key (key s K)"
| "apm s (Hash X) = Hash (apm s X)"
| "apm s (Crypt K X) = (
if (\<exists>A. K = pubK A) then Crypt (pubK (agent s (agt K))) (apm s X)
else if (\<exists>A. K = priK A) then Crypt (priK (agent s (agt K))) (apm s X)
else Crypt (key s K) (apm s X))"
| "apm s \X,Y\ = \apm s X, apm s Y\"

lemma apm_parts: "X \ parts {Y} \ apm s X \ parts {apm s Y}"
apply (erule parts.induct, simp_all, blast)
apply (erule parts.Fst)
apply (erule parts.Snd)
by (erule parts.Body)+

lemma Nonce_apm [rule_format]: "Nonce n \ parts {apm s X} \
(\<forall>k. Number k \<in> parts {X} \<longrightarrow> Nonce n \<notin> parts {nb s k}) \<longrightarrow>
(\<exists>k. Nonce k \<in> parts {X} \<and> nonce s k = n)"
by (induct X, simp_all, blast)

lemma wdef_Nonce: "\Nonce n \ parts {apm s X}; R \ p; msg' R = X; wdef p;
Nonce n \<notin> parts (apm s `(msg `(fst R)))\<rbrakk> \<Longrightarrow>
(\<exists>k. Nonce k \<in> parts {X} \<and> nonce s k = n)"
apply (erule Nonce_apm, unfold wdef_def)
apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp)
apply (drule_tac x=x in bspec, simp)
apply (drule_tac Y="msg x" and s=s in apm_parts, simp)
by (blast dest: parts_parts)

primrec ap :: "subs \ event \ event" where
  "ap s (Says A B X) = Says (agent s A) (agent s B) (apm s X)"
| "ap s (Gets A X) = Gets (agent s A) (apm s X)"
| "ap s (Notes A X) = Notes (agent s A) (apm s X)"

abbreviation
  ap' :: "subs \ rule \ event" where
  "ap' s R \ ap s (snd R)"

abbreviation
  apm' :: "subs \ rule \ msg" where
  "apm' s R \ apm s (msg' R)"

abbreviation
  priK' :: "subs \ agent \ key" where
  "priK' s A \ priK (agent s A)"

abbreviation
  pubK' :: "subs \ agent \ key" where
  "pubK' s A \ pubK (agent s A)"

subsection\<open>nonces generated by a rule\<close>

definition newn :: "rule \ nat set" where
"newn R \ {n. Nonce n \ parts {msg (snd R)} \ Nonce n \ parts (msg`(fst R))}"

lemma newn_parts: "n \ newn R \ Nonce (nonce s n) \ parts {apm' s R}"
by (auto simp: newn_def dest: apm_parts)

subsection\<open>traces generated by a protocol\<close>

definition ok :: "event list \ rule \ subs \ bool" where
"ok evs R s \ ((\x. x \ fst R \ ap s x \ set evs)
\<and> (\<forall>n. n \<in> newn R \<longrightarrow> Nonce (nonce s n) \<notin> used evs))"

inductive_set
  tr :: "proto => event list set"
  for p :: proto
where

  Nil [intro]: "[] \ tr p"

| Fake [intro]: "\evsf \ tr p; X \ synth (analz (spies evsf))\
  \<Longrightarrow> Says Spy B X # evsf \<in> tr p"

| Proto [intro]: "\evs \ tr p; R \ p; ok evs R s\ \ ap' s R # evs \ tr p"

subsection\<open>general properties\<close>

lemma one_step_tr [iff]: "one_step (tr p)"
apply (unfold one_step_def, clarify)
by (ind_cases "ev # evs \ tr p" for ev evs, auto)

definition has_only_Says' :: "proto => bool" where
"has_only_Says' p \ \R. R \ p \ is_Says (snd R)"

lemma has_only_Says'D: "\R \ p; has_only_Says' p\
\<Longrightarrow> (\<exists>A B X. snd R = Says A B X)"
by (unfold has_only_Says'_def is_Says_def, blast)

lemma has_only_Says_tr [simp]: "has_only_Says' p \ has_only_Says (tr p)"
unfolding has_only_Says_def
apply (rule allI, rule allI, rule impI)
apply (erule tr.induct)
apply (auto simp: has_only_Says'_def ok_def)
by (drule_tac x=a in spec, auto simp: is_Says_def)

lemma has_only_Says'_in_trD: "\has_only_Says' p; list @ ev # evs1 \ tr p\
\<Longrightarrow> (\<exists>A B X. ev = Says A B X)"
by (drule has_only_Says_tr, auto)

lemma ok_not_used: "\Nonce n \ used evs; ok evs R s;
\<forall>x. x \<in> fst R \<longrightarrow> is_Says x\<rbrakk> \<Longrightarrow> Nonce n \<notin> parts (apm s `(msg `(fst R)))"
apply (unfold ok_def, clarsimp)
apply (drule_tac x=x in spec, drule_tac x=x in spec)
by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts)

lemma ok_is_Says: "\evs' @ ev # evs \ tr p; ok evs R s; has_only_Says' p;
R \<in> p; x \<in> fst R\<rbrakk> \<Longrightarrow> is_Says x"
apply (unfold ok_def is_Says_def, clarify)
apply (drule_tac x=x in spec, simp)
apply (subgoal_tac "one_step (tr p)")
apply (drule trunc, simp, drule one_step_Cons, simp)
apply (drule has_only_SaysD, simp+)
by (clarify, case_tac x, auto)

subsection\<open>types\<close>

type_synonym keyfun = "rule \ subs \ nat \ event list \ key set"

type_synonym secfun = "rule \ nat \ subs \ key set \ msg"

subsection\<open>introduction of a fresh guarded nonce\<close>

definition fresh :: "proto \ rule \ subs \ nat \ key set \ event list
\<Rightarrow> bool" where
"fresh p R s n Ks evs \ (\evs1 evs2. evs = evs2 @ ap' s R # evs1
\<and> Nonce n \<notin> used evs1 \<and> R \<in> p \<and> ok evs1 R s \<and> Nonce n \<in> parts {apm' s R}
\<and> apm' s R \<in> guard n Ks)"

lemma freshD: "fresh p R s n Ks evs \ (\evs1 evs2.
evs = evs2 @ ap' s R # evs1 \ Nonce n \ used evs1 \ R \ p \ ok evs1 R s
\<and> Nonce n \<in> parts {apm' s R} \<and> apm' s R \<in> guard n Ks)"
  unfolding fresh_def by blast

lemma freshI [intro]: "\Nonce n \ used evs1; R \ p; Nonce n \ parts {apm' s R};
ok evs1 R s; apm' s R \ guard n Ks\
\<Longrightarrow> fresh p R s n Ks (list @ ap' s R # evs1)"
  unfolding fresh_def by blast

lemma freshI': "\Nonce n \ used evs1; (l,r) \ p;
Nonce n \<in> parts {apm s (msg r)}; ok evs1 (l,r) s; apm s (msg r) \<in> guard n Ks\<rbrakk>
\<Longrightarrow> fresh p (l,r) s n Ks (evs2 @ ap s r # evs1)"
by (drule freshI, simp+)

lemma fresh_used: "\fresh p R' s' n Ks evs; has_only_Says' p\
\<Longrightarrow> Nonce n \<in> used evs"
apply (unfold fresh_def, clarify)
apply (drule has_only_Says'D)
by (auto intro: parts_used_app)

lemma fresh_newn: "\evs' @ ap' s R # evs \ tr p; wdef p; has_only_Says' p;
Nonce n \<notin> used evs; R \<in> p; ok evs R s; Nonce n \<in> parts {apm' s R}\<rbrakk>
\<Longrightarrow> \<exists>k. k \<in> newn R \<and> nonce s k = n"
apply (drule wdef_Nonce, simp+)
apply (frule ok_not_used, simp+)
apply (clarify, erule ok_is_Says, simp+)
apply (clarify, rule_tac x=k in exI, simp add: newn_def)
apply (clarify, drule_tac Y="msg x" and s=s in apm_parts)
apply (drule ok_not_used, simp+)
by (clarify, erule ok_is_Says, simp_all)

lemma fresh_rule: "\evs' @ ev # evs \ tr p; wdef p; Nonce n \ used evs;
Nonce n \<in> parts {msg ev}\<rbrakk> \<Longrightarrow> \<exists>R s. R \<in> p \<and> ap' s R = ev"
apply (drule trunc, simp, ind_cases "ev # evs \ tr p", simp)
by (drule_tac x=X in in_sub, drule parts_sub, simp, simp, blast+)

lemma fresh_ruleD: "\fresh p R' s' n Ks evs; keys R' s' n evs \ Ks; wdef p;
has_only_Says' p; evs \ tr p; \R k s. nonce s k = n \ Nonce n \ used evs \
R \<in> p \<longrightarrow> k \<in> newn R \<longrightarrow> Nonce n \<in> parts {apm' s R} \<longrightarrow> apm' s R \<in> guard n Ks \<longrightarrow>
apm' s R \ parts (spies evs) \ keys R s n evs \ Ks \ P\ \ P"
apply (frule fresh_used, simp)
apply (unfold fresh_def, clarify)
apply (drule_tac x=R' in spec)
apply (drule fresh_newn, simp+, clarify)
apply (drule_tac x=k in spec)
apply (drule_tac x=s' in spec)
apply (subgoal_tac "apm' s' R' \ parts (spies (evs2 @ ap' s' R' # evs1))")
apply (case_tac R', drule has_only_Says'D, simp, clarsimp)
apply (case_tac R', drule has_only_Says'D, simp, clarsimp)
apply (rule_tac Y="apm s' X" in parts_parts, blast)
by (rule parts.Inj, rule Says_imp_spies, simp, blast)

subsection\<open>safe keys\<close>

definition safe :: "key set \ msg set \ bool" where
"safe Ks G \ \K. K \ Ks \ Key K \ analz G"

lemma safeD [dest]: "\safe Ks G; K \ Ks\ \ Key K \ analz G"
  unfolding safe_def by blast

lemma safe_insert: "safe Ks (insert X G) \ safe Ks G"
  unfolding safe_def by blast

lemma Guard_safe: "\Guard n Ks G; safe Ks G\ \ Nonce n \ analz G"
by (blast dest: Guard_invKey)

subsection\<open>guardedness preservation\<close>

definition preserv :: "proto \ keyfun \ nat \ key set \ bool" where
"preserv p keys n Ks \ (\evs R' s' R s. evs \ tr p \
Guard n Ks (spies evs) \<longrightarrow> safe Ks (spies evs) \<longrightarrow> fresh p R' s' n Ks evs \<longrightarrow>
keys R' s' n evs \<subseteq> Ks \<longrightarrow> R \<in> p \<longrightarrow> ok evs R s \<longrightarrow> apm' s R \<in> guard n Ks)"

lemma preservD: "\preserv p keys n Ks; evs \ tr p; Guard n Ks (spies evs);
safe Ks (spies evs); fresh p R' s' n Ks evs; R \<in> p; ok evs R s;
keys R' s' n evs \<subseteq> Ks\<rbrakk> \<Longrightarrow> apm' s R \<in> guard n Ks"
  unfolding preserv_def by blast

lemma preservD': "\preserv p keys n Ks; evs \ tr p; Guard n Ks (spies evs);
safe Ks (spies evs); fresh p R' s' n Ks evs; (l,Says A B X) \<in> p;
ok evs (l,Says A B X) s; keys R' s' n evs \<subseteq> Ks\<rbrakk> \<Longrightarrow> apm s X \<in> guard n Ks"
by (drule preservD, simp+)

subsection\<open>monotonic keyfun\<close>

definition monoton :: "proto => keyfun => bool" where
"monoton p keys \ \R' s' n ev evs. ev # evs \ tr p \
keys R' s' n evs \<subseteq> keys R' s' n (ev # evs)"

lemma monotonD [dest]: "\keys R' s' n (ev # evs) \ Ks; monoton p keys;
ev # evs \<in> tr p\<rbrakk> \<Longrightarrow> keys R' s' n evs \<subseteq> Ks"
  unfolding monoton_def by blast

subsection\<open>guardedness theorem\<close>

lemma Guard_tr [rule_format]: "\evs \ tr p; has_only_Says' p;
preserv p keys n Ks; monoton p keys; Guard n Ks (initState Spy)\<rbrakk> \<Longrightarrow>
safe Ks (spies evs) \<longrightarrow> fresh p R' s' n Ks evs \<longrightarrow> keys R' s' n evs \<subseteq> Ks \<longrightarrow>
Guard n Ks (spies evs)"
apply (erule tr.induct)
(* Nil *)
apply simp
(* Fake *)
apply (clarify, drule freshD, clarsimp)
apply (case_tac evs2)
(* evs2 = [] *)
apply (frule has_only_Says'D, simp)
apply (clarsimp, blast)
(* evs2 = aa # list *)
apply (clarsimp, rule conjI)
apply (blast dest: safe_insert)
(* X:guard n Ks *)
apply (rule in_synth_Guard, simp, rule Guard_analz)
apply (blast dest: safe_insert)
apply (drule safe_insert, simp add: safe_def)
(* Proto *)
apply (clarify, drule freshD, clarify)
apply (case_tac evs2)
(* evs2 = [] *)
apply (frule has_only_Says'D, simp)
apply (frule_tac R=R' in has_only_Says'D, simp)
apply (case_tac R', clarsimp, blast)
(* evs2 = ab # list *)
apply (frule has_only_Says'D, simp)
apply (clarsimp, rule conjI)
apply (drule Proto, simp+, blast dest: safe_insert)
(* apm s X:guard n Ks *)
apply (frule Proto, simp+)
apply (erule preservD', simp+)
apply (blast dest: safe_insert)
apply (blast dest: safe_insert)
by (blast, simp, simp, blast)

subsection\<open>useful properties for guardedness\<close>

lemma newn_neq_used: "\Nonce n \ used evs; ok evs R s; k \ newn R\
\<Longrightarrow> n \<noteq> nonce s k"
by (auto simp: ok_def)

lemma ok_Guard: "\ok evs R s; Guard n Ks (spies evs); x \ fst R; is_Says x\
\<Longrightarrow> apm s (msg x) \<in> parts (spies evs) \<and> apm s (msg x) \<in> guard n Ks"
apply (unfold ok_def is_Says_def, clarify)
apply (drule_tac x="Says A B X" in spec, simp)
by (drule Says_imp_spies, auto intro: parts_parts)

lemma ok_parts_not_new: "\Y \ parts (spies evs); Nonce (nonce s n) \ parts {Y};
ok evs R s\<rbrakk> \<Longrightarrow> n \<notin> newn R"
by (auto simp: ok_def dest: not_used_not_spied parts_parts)

subsection\<open>unicity\<close>

definition uniq :: "proto \ secfun \ bool" where
"uniq p secret \ \evs R R' n n' Ks s s'. R \ p \ R' \ p \
n \<in> newn R \<longrightarrow> n' \<in> newn R' \<longrightarrow> nonce s n = nonce s' n' \<longrightarrow>
Nonce (nonce s n) \<in> parts {apm' s R} \<longrightarrow> Nonce (nonce s n) \<in> parts {apm' s' R'} \<longrightarrow>
apm' s R \ guard (nonce s n) Ks \ apm' s' R' \ guard (nonce s n) Ks \
evs \<in> tr p \<longrightarrow> Nonce (nonce s n) \<notin> analz (spies evs) \<longrightarrow>
secret R n s Ks \<in> parts (spies evs) \<longrightarrow> secret R' n' s' Ks \<in> parts (spies evs) \<longrightarrow>
secret R n s Ks = secret R' n' s' Ks"

lemma uniqD: "\uniq p secret; evs \ tr p; R \ p; R' \ p; n \ newn R; n' \ newn R';
nonce s n = nonce s' n'; Nonce (nonce s n) \<notin> analz (spies evs);
Nonce (nonce s n) \<in> parts {apm' s R}; Nonce (nonce s n) \<in> parts {apm' s' R'};
secret R n s Ks \<in> parts (spies evs); secret R' n' s' Ks \<in> parts (spies evs);
apm' s R \ guard (nonce s n) Ks; apm' s' R' \ guard (nonce s n) Ks\ \
secret R n s Ks = secret R' n' s' Ks"
  unfolding uniq_def by blast

definition ord :: "proto \ (rule \ rule \ bool) \ bool" where
"ord p inff \ \R R'. R \ p \ R' \ p \ \ inff R R' \ inff R' R"

lemma ordD: "\ord p inff; \ inff R R'; R \ p; R' \ p\ \ inff R' R"
  unfolding ord_def by blast

definition uniq' :: "proto \ (rule \ rule \ bool) \ secfun \ bool" where
"uniq' p inff secret \ \evs R R' n n' Ks s s'. R \ p \ R' \ p \
inff R R' \ n \ newn R \ n' \ newn R' \ nonce s n = nonce s' n' \
Nonce (nonce s n) \<in> parts {apm' s R} \<longrightarrow> Nonce (nonce s n) \<in> parts {apm' s' R'} \<longrightarrow>
apm' s R \ guard (nonce s n) Ks \ apm' s' R' \ guard (nonce s n) Ks \
evs \<in> tr p \<longrightarrow> Nonce (nonce s n) \<notin> analz (spies evs) \<longrightarrow>
secret R n s Ks \<in> parts (spies evs) \<longrightarrow> secret R' n' s' Ks \<in> parts (spies evs) \<longrightarrow>
secret R n s Ks = secret R' n' s' Ks"

lemma uniq'D: "\uniq' p inff secret; evs \ tr p; inff R R'; R \ p; R' \ p; n \ newn R;
n' \ newn R'; nonce s n = nonce s' n'; Nonce (nonce s n) \ analz (spies evs);
Nonce (nonce s n) \<in> parts {apm' s R}; Nonce (nonce s n) \<in> parts {apm' s' R'};
secret R n s Ks \<in> parts (spies evs); secret R' n' s' Ks \<in> parts (spies evs);
apm' s R \ guard (nonce s n) Ks; apm' s' R' \ guard (nonce s n) Ks\ \
secret R n s Ks = secret R' n' s' Ks"
by (unfold uniq'_def, blast)

lemma uniq'_imp_uniq: "\uniq' p inff secret; ord p inff\ \ uniq p secret"
unfolding uniq_def
apply (rule allI)+
apply (case_tac "inff R R'")
apply (blast dest: uniq'D)
by (auto dest: ordD uniq'D intro: sym)

subsection\<open>Needham-Schroeder-Lowe\<close>

definition a :: agent where "a == Friend 0"
definition b :: agent where "b == Friend 1"
definition a' :: agent where "a' == Friend 2"
definition b' :: agent where "b' == Friend 3"
definition Na :: nat where "Na == 0"
definition Nb :: nat where "Nb == 1"

abbreviation
  ns1 :: rule where
  "ns1 == ({}, Says a b (Crypt (pubK b) \Nonce Na, Agent a\))"

abbreviation
  ns2 :: rule where
  "ns2 == ({Says a' b (Crypt (pubK b) \Nonce Na, Agent a\)},
    Says b a (Crypt (pubK a) \<lbrace>Nonce Na, Nonce Nb, Agent b\<rbrace>))"

abbreviation
  ns3 :: rule where
  "ns3 == ({Says a b (Crypt (pubK b) \Nonce Na, Agent a\),
    Says b' a (Crypt (pubK a) \Nonce Na, Nonce Nb, Agent b\)},
    Says a b (Crypt (pubK b) (Nonce Nb)))"

inductive_set ns :: proto where
  [iff]: "ns1 \ ns"
| [iff]: "ns2 \ ns"
| [iff]: "ns3 \ ns"

abbreviation (input)
  ns3a :: event where
  "ns3a == Says a b (Crypt (pubK b) \Nonce Na, Agent a\)"

abbreviation (input)
  ns3b :: event where
  "ns3b == Says b' a (Crypt (pubK a) \Nonce Na, Nonce Nb, Agent b\)"

definition keys :: "keyfun" where
"keys R' s' n evs == {priK' s' a, priK' s' b}"

lemma "monoton ns keys"
by (simp add: keys_def monoton_def)

definition secret :: "secfun" where
"secret R n s Ks ==
(if R=ns1 then apm s (Crypt (pubK b) \<lbrace>Nonce Na, Agent a\<rbrace>)
else if R=ns2 then apm s (Crypt (pubK a) \<lbrace>Nonce Na, Nonce Nb, Agent b\<rbrace>)
else Number 0)"

definition inf :: "rule => rule => bool" where
"inf R R' == (R=ns1 | (R=ns2 & R'~=ns1) | (R=ns3 & R'=ns3))"

lemma inf_is_ord [iff]: "ord ns inf"
apply (unfold ord_def inf_def)
apply (rule allI)+
apply (rule impI)
apply (simp add: split_paired_all)
by (rule impI, erule ns.cases, simp_all)+

subsection\<open>general properties\<close>

lemma ns_has_only_Says' [iff]: "has_only_Says' ns"
apply (unfold has_only_Says'_def)
apply (rule allI, rule impI)
apply (simp add: split_paired_all)
by (erule ns.cases, auto)

lemma newn_ns1 [iff]: "newn ns1 = {Na}"
by (simp add: newn_def)

lemma newn_ns2 [iff]: "newn ns2 = {Nb}"
by (auto simp: newn_def Na_def Nb_def)

lemma newn_ns3 [iff]: "newn ns3 = {}"
by (auto simp: newn_def)

lemma ns_wdef [iff]: "wdef ns"
by (auto simp: wdef_def elim: ns.cases)

subsection\<open>guardedness for NSL\<close>

lemma "uniq ns secret \ preserv ns keys n Ks"
unfolding preserv_def
apply (rule allI)+
apply (rule impI, rule impI, rule impI, rule impI, rule impI)
apply (erule fresh_ruleD, simp, simp, simp, simp)
apply (rule allI)+
apply (rule impI, rule impI, rule impI)
apply (simp add: split_paired_all)
apply (erule ns.cases)
(* fresh with NS1 *)
apply (rule impI, rule impI, rule impI, rule impI, rule impI, rule impI)
apply (erule ns.cases)
(* NS1 *)
apply clarsimp
apply (frule newn_neq_used, simp, simp)
apply (rule No_Nonce, simp)
(* NS2 *)
apply clarsimp
apply (frule newn_neq_used, simp, simp)
apply (case_tac "nonce sa Na = nonce s Na")
apply (frule Guard_safe, simp)
apply (frule Crypt_guard_invKey, simp)
apply (frule ok_Guard, simp, simp, simp, clarsimp)
apply (frule_tac K="pubK' s Proto.b" in Crypt_guard_invKey, simp)
apply (frule_tac R=ns1 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
apply (simp add: secret_def, simp add: secret_def, force, force)
apply (simp add: secret_def keys_def, blast)
apply (rule No_Nonce, simp)
(* NS3 *)
apply clarsimp
apply (case_tac "nonce sa Na = nonce s Nb")
apply (frule Guard_safe, simp)
apply (frule Crypt_guard_invKey, simp)
apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
apply (frule_tac K="pubK' s Proto.a" in Crypt_guard_invKey, simp)
apply (frule_tac R=ns1 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
apply (simp add: secret_def, simp add: secret_def, force, force)
apply (simp add: secret_def, rule No_Nonce, simp)
(* fresh with NS2 *)
apply (rule impI, rule impI, rule impI, rule impI, rule impI, rule impI)
apply (erule ns.cases)
(* NS1 *)
apply clarsimp
apply (frule newn_neq_used, simp, simp)
apply (rule No_Nonce, simp)
(* NS2 *)
apply clarsimp
apply (frule newn_neq_used, simp, simp)
apply (case_tac "nonce sa Nb = nonce s Na")
apply (frule Guard_safe, simp)
apply (frule Crypt_guard_invKey, simp)
apply (frule ok_Guard, simp, simp, simp, clarsimp)
apply (frule_tac K="pubK' s Proto.b" in Crypt_guard_invKey, simp)
apply (frule_tac R=ns2 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
apply (simp add: secret_def, simp add: secret_def, force, force)
apply (simp add: secret_def, rule No_Nonce, simp)
(* NS3 *)
apply clarsimp
apply (case_tac "nonce sa Nb = nonce s Nb")
apply (frule Guard_safe, simp)
apply (frule Crypt_guard_invKey, simp)
apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
apply (frule_tac K="pubK' s Proto.a" in Crypt_guard_invKey, simp)
apply (frule_tac R=ns2 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
apply (simp add: secret_def, simp add: secret_def, force, force)
apply (simp add: secret_def keys_def, blast)
apply (rule No_Nonce, simp)
(* fresh with NS3 *)
by simp

subsection\<open>unicity for NSL\<close>

lemma "uniq' ns inf secret"
apply (unfold uniq'_def)
apply (rule allI)+
apply (simp add: split_paired_all)
apply (rule impI, erule ns.cases)
(* R = ns1 *)
apply (rule impI, erule ns.cases)
(* R' = ns1 *)
apply (rule impI, rule impI, rule impI, rule impI)
apply (rule impI, rule impI, rule impI, rule impI)
apply (rule impI, erule tr.induct)
(* Nil *)
apply (simp add: secret_def)
(* Fake *)
apply (clarify, simp add: secret_def)
apply (drule notin_analz_insert)
apply (drule Crypt_insert_synth, simp, simp, simp)
apply (drule Crypt_insert_synth, simp, simp, simp, simp)
(* Proto *)
apply (erule_tac P="ok evsa R sa" in rev_mp)
apply (simp add: split_paired_all)
apply (erule ns.cases)
(* ns1 *)
apply (clarify, simp add: secret_def)
apply (erule disjE, erule disjE, clarsimp)
apply (drule ok_parts_not_new, simp, simp, simp)
apply (clarify, drule ok_parts_not_new, simp, simp, simp)
(* ns2 *)
apply (simp add: secret_def)
(* ns3 *)
apply (simp add: secret_def)
(* R' = ns2 *)
apply (rule impI, rule impI, rule impI, rule impI)
apply (rule impI, rule impI, rule impI, rule impI)
apply (rule impI, erule tr.induct)
(* Nil *)
apply (simp add: secret_def)
(* Fake *)
apply (clarify, simp add: secret_def)
apply (drule notin_analz_insert)
apply (drule Crypt_insert_synth, simp, simp, simp)
apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp, simp)
(* Proto *)
apply (erule_tac P="ok evsa R sa" in rev_mp)
apply (simp add: split_paired_all)
apply (erule ns.cases)
(* ns1 *)
apply (clarify, simp add: secret_def)
apply (drule_tac s=sa and n=Na in ok_parts_not_new, simp, simp, simp)
(* ns2 *)
apply (clarify, simp add: secret_def)
apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp)
(* ns3 *)
apply (simp add: secret_def)
(* R' = ns3 *)
apply simp
(* R = ns2 *)
apply (rule impI, erule ns.cases)
(* R' = ns1 *)
apply (simp only: inf_def, blast)
(* R' = ns2 *)
apply (rule impI, rule impI, rule impI, rule impI)
apply (rule impI, rule impI, rule impI, rule impI)
apply (rule impI, erule tr.induct)
(* Nil *)
apply (simp add: secret_def)
(* Fake *)
apply (clarify, simp add: secret_def)
apply (drule notin_analz_insert)
apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp)
apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp, simp)
(* Proto *)
apply (erule_tac P="ok evsa R sa" in rev_mp)
apply (simp add: split_paired_all)
apply (erule ns.cases)
(* ns1 *)
apply (simp add: secret_def)
(* ns2 *)
apply (clarify, simp add: secret_def)
apply (erule disjE, erule disjE, clarsimp, clarsimp)
apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp)
apply (erule disjE, clarsimp)
apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp)
by (simp_all add: secret_def)

end

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.