scyther-proof-0.3.1: data/isabelle/src/ESPLogic/WeakTyping.thy
(*****************************************************************************
* ESPL --- an embedded security protocol logic
* http://people.inf.ethz.ch/meiersi/espl/
*
* Copyright (c) 2009-2011, Simon Meier, ETH Zurich, Switzerland
*
* Extension to compromising adversaries:
*
* Copyright (c) 2010-2011, Martin Schaub, ETH Zurich, Switzerland
*
* All rights reserved. See file LICENCE for more information.
******************************************************************************)
theory WeakTyping
imports
InferenceRules
Syntax
begin
section{* A Shallow Embedding of a Message Type System *}
subsection{* Introduction *}
text{*
The goal of this theory is to develop a simple way for specifying
type invariants for the message variables of a protocol. A message
type is a set of messages that depends on the thread and the
system state that this message type is interpreted relative to.
A typing is then a function assigning to each combination of a
role and an identifier of a message variable in this role a
message type.
Each typing approximates the set of states where all instantiated
message variables are instantiated with a message corresponding
to their type.
*}
types msgtype = "tid \<Rightarrow> state \<Rightarrow> execmsg set"
types typing = "(role \<times> id) \<Rightarrow> msgtype"
definition approx :: "typing \<Rightarrow> state set"
where "approx typing q \<equiv> case q of (t,r,s) \<Rightarrow>
\<forall> (i,step) \<in> steps t.
\<forall> R. roleMap r i = Some R \<longrightarrow>
(\<forall> n. MVar n \<in> FV (stepPat step) \<longrightarrow>
s (MVar n, i) \<in> typing (R, n) i (t,r,s)
)"
locale typed_state = reachable_state+
fixes typing :: "typing"
assumes approximates: "(t,r,s) \<in> approx typing"
locale typed_thread = reachable_thread+
fixes typing :: "typing"
assumes approximates: "(t,r,s) \<in> approx typing"
sublocale typed_thread \<subseteq> typed_state
using approximates by unfold_locales
lemma approx_unfold:
"((t,r,s) \<in> approx typing) =
(\<forall> (i,step) \<in> steps t.
\<forall> R. roleMap r i = Some R \<longrightarrow>
(\<forall> n. MVar n \<in> FV (stepPat step) \<longrightarrow>
s (MVar n, i) \<in> typing (R, n) i (t,r,s)))"
by (auto simp: approx_def mem_def)
lemma in_approxI:
assumes all_vars:
"\<And> i step R n.
\<lbrakk> (i,step) \<in> steps t;
roleMap r i = Some R;
MVar n \<in> FV (stepPat step)
\<rbrakk>
\<Longrightarrow> s (MV n i) \<in> typing (R, n) i (t,r,s)"
shows "(t,r,s) \<in> approx typing"
by (auto simp: approx_unfold dest!: all_vars)
lemma in_approxD:
assumes approx: "(t,r,s) \<in> approx typing"
and asms: "(i,step) \<in> steps t"
"roleMap r i = Some R"
"MVar n \<in> FV (stepPat step)"
shows "s (MV n i) \<in> typing (R, n) i (t,r,s)"
using approx asms
by (auto simp: approx_unfold)
subsection{* A Combinator Language for Message Types *}
subsubsection{* Structural Types *}
text{*
Structural message types specify the structure of a message.
Their interpretation is independent of the thread that they
are interpreted in. All of them except the type for nonces of
a specific role are also independent of the state that they
are interpreted in.
*}
definition ConstT :: "id \<Rightarrow> msgtype"
where "ConstT c i q \<equiv> { LC c }"
definition AgentT :: msgtype
where "AgentT i q \<equiv> Agent"
declare AgentT_def [simp]
definition NonceT :: "role \<Rightarrow> id \<Rightarrow> msgtype"
where "NonceT R n i q \<equiv> case q of
(t,r,s) \<Rightarrow> { LN n i' | i'. roleMap r i' = Some R }"
definition HashT :: "msgtype \<Rightarrow> msgtype"
where "HashT ty i q \<equiv> { Hash m | m. m \<in> ty i q }"
definition TupT :: "msgtype \<Rightarrow> msgtype \<Rightarrow> msgtype"
where "TupT ty1 ty2 i q \<equiv>
{ \<lbrace>x, y\<rbrace> | x y. x \<in> ty1 i q \<and> y \<in> ty2 i q }"
definition EncT :: "msgtype \<Rightarrow> msgtype \<Rightarrow> msgtype"
where "EncT tym tyk i q \<equiv>
{ Enc m k | m k. m \<in> tym i q \<and> k \<in> tyk i q }"
definition PKT :: "msgtype \<Rightarrow> msgtype"
where "PKT ty i q \<equiv> { PK m | m. m \<in> ty i q }"
definition SKT :: "msgtype \<Rightarrow> msgtype"
where "SKT ty i q \<equiv> { SK m | m. m \<in> ty i q }"
definition KT :: "msgtype \<Rightarrow> msgtype \<Rightarrow> msgtype"
where "KT ty1 ty2 i q \<equiv>
{ K m1 m2 | m1 m2. m1 \<in> ty1 i q \<and> m2 \<in> ty2 i q }"
definition KShrT :: "msgtype"
where "KShrT i q \<equiv> { KShr A | A. True }"
text{* TODO: Make this syntax abbreviation work. *}
syntax
"@TTuple" :: "['a, args] => 'a * 'b" ("(2{$_,/ _$})")
syntax (xsymbols)
"@TTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>$_,/ _$\<rbrace>)")
translations
"{$x, y, z$}" == "{$x, {$y, z$}$}"
"{$x, y$}" == "WeakTyping.TupT x y"
subsubsection{* Special Types *}
text{*
The empty type denotes that a variable is never instantiated.
The sum type denotes the union of two message types, while
the intersection type denotes the intersection of the two
message types.
*}
definition EmptyT :: "msgtype"
where "EmptyT i q \<equiv> {}"
declare EmptyT_def [simp]
definition SumT :: "msgtype \<Rightarrow> msgtype \<Rightarrow> msgtype"
where "SumT ty1 ty2 i q \<equiv> ty1 i q \<union> ty2 i q"
definition InterT :: "msgtype \<Rightarrow> msgtype \<Rightarrow> msgtype"
where "InterT ty1 ty2 i q \<equiv> ty1 i q \<inter> ty2 i q"
text{*
The known before a specific role step type captures the
interaction of the intruder with the execution of a protocol.
If the intruder fakes a message being received, then the
variables are instantiated with messages known to the intruder
\emph{before} the receive step was executed.
*}
definition KnownT :: "rolestep \<Rightarrow> msgtype"
where "KnownT step i q \<equiv> case q of (t,r,s) \<Rightarrow>
{ m | m. predOrd t (Ln m) (St (i,step)) }"
subsubsection{* Constructing Type Invariants *}
text{*
The following function converts a list of type assignments to a
typing. It will be used to specify the type invariants of specific
protocols.
*}
definition mk_typing :: "((role \<times> id) \<times> msgtype) list \<Rightarrow> typing"
where "mk_typing tyeqs \<equiv>
foldr (\<lambda>(x, ty) typing. typing(x:=ty)) tyeqs (\<lambda>x. EmptyT)"
subsection{* Proving Well-Typedness *}
text{*
A protocol is well-typed with respect to a typing iff
all its reachable state are approximated by the typing.
We specialize the induction scheme that we get from the definition
of the set of reachable states to a ``type checking'' induction
scheme. It works for message typings that are monotoneous with
respect to state updates.
*}
definition monoTyp :: "typing \<Rightarrow> bool"
where "monoTyp typ \<equiv>
(\<forall> x i t r s t' r'.
roleMap r \<subseteq>\<^sub>m roleMap r' \<longrightarrow>
typ x i (t,r,s) \<subseteq> typ x i (t@t',r',s)
)"
lemma monoTypI:
"\<lbrakk> \<And> x i t r s t' r' s' m.
\<lbrakk> roleMap r \<subseteq>\<^sub>m roleMap r'; m \<in> typ x i (t,r,s) \<rbrakk>
\<Longrightarrow> m \<in> typ x i (t@t',r',s)
\<rbrakk> \<Longrightarrow> monoTyp typ"
by(auto simp: monoTyp_def)
lemma monoTypD:
"\<lbrakk> monoTyp typ;
m \<in> typ x i (t,r,s);
roleMap r \<subseteq>\<^sub>m roleMap r'
\<rbrakk> \<Longrightarrow>
m \<in> typ x i (t@t',r',s)"
unfolding monoTyp_def by blast
lemma monoTyp_freeD:
"\<lbrakk> monoTyp typ;
m \<in> typ x i (t,r,s);
roleMap r \<subseteq>\<^sub>m roleMap r';
t' = t@t''
\<rbrakk> \<Longrightarrow>
m \<in> typ x i (t',r',s)"
unfolding monoTyp_def by blast
lemma monoTyp_appendD:
"\<lbrakk> monoTyp typ;
m \<in> typ x i (t,r,s)
\<rbrakk> \<Longrightarrow>
m \<in> typ x i (t@t',r,s)"
by (rule monoTyp_freeD) auto
lemma (in reachable_state) reachable_in_approxI:
assumes monoTyp: "monoTyp typing"
and recv_case:
"\<And> t r s i done todo skipped m R step n.
\<lbrakk> R \<in> P;
roleMap r i = Some R;
(done, step # todo) \<in> set (splits R);
recvStep step;
MVar n \<in> FV (stepPat step);
\<forall> step' \<in> set done. MVar n \<notin> FV (stepPat step');
hint ''completenessCase'' (step, n);
(t,r,s) \<in> reachable P;
(t,r,s) \<in> approx typing;
r i = Some (done, step # todo, skipped);
Some m = inst s i (stepPat step);
m \<in> knows t
\<rbrakk> \<Longrightarrow>
s (MV n i) \<in> typing (R, n) i (t @ [Step (i, step)], r(i \<mapsto> (done @ [step], todo, skipped)), s)"
shows "(t,r,s) \<in> approx typing"
proof -
{ fix i step "done" todo skipped n
have
"\<lbrakk> r i = Some (done, todo, skipped);
(i,step) \<in> steps t;
MVar n \<in> FV (stepPat step)
\<rbrakk> \<Longrightarrow> s (MV n i) \<in> typing (done@todo, n) i (t,r,s)"
proof(induct arbitrary: i "done" todo step n skipped rule: reachable_induct)
case (send t r s i "done" l pt todo skipped m i' done' todo' step n skipped')
then interpret th1:
reachable_thread P t r s i "done" "Send l pt # todo" skipped
by unfold_locales auto
from send
have "(i', step) \<in> steps t \<or> (i' = i) \<and> step = Send l pt"
(is "?old \<or> ?new") by auto
moreover
{ assume ?old
hence "s(MV n i') \<in> typing (done'@todo', n) i' (t,r,s)"
using send by (auto split: if_splits)
hence ?case
proof(rule monoTyp_freeD[OF monoTyp])
qed (auto simp: th1.thread_exists)
}
moreover
{ let ?role = "done @ Send l pt # todo"
note IH = send(2)
assume "?new"
hence "MVar n \<in> FV pt"
using send by auto
then obtain l' msg'
where "(i, Recv l' msg') \<in> steps t"
"MVar n \<in> FV msg'"
by (fastsimp dest!: th1.send_step_FV[OF th1.thread_exists])
hence typed: "s (MV n i) \<in> typing (?role, n) i (t, r, s)"
by (auto dest: IH[OF th1.thread_exists])
have "done'@todo' = ?role"
using send `?new` by auto
hence ?case using `?new`
apply -
apply(rule monoTyp_freeD[OF monoTyp])
by (auto intro!: typed simp: th1.thread_exists)
}
ultimately show ?case by fast
next
case (recv t r s i "done" l pt todo skipped m i' done' todo' step n skipped') then
interpret th1:
reachable_thread P t r s i "done" "Recv l pt # todo" skipped
by unfold_locales auto
from recv
have "(i', step) \<in> steps t \<or> (i' = i) \<and> step = Recv l pt"
(is "?old \<or> ?new") by auto
moreover
{ assume ?old
hence "s(MV n i') \<in> typing (done'@todo', n) i' (t,r,s)"
using recv by (auto split: if_splits)
hence ?case using `?old`
apply -
apply(rule monoTyp_freeD[OF monoTyp])
apply(auto simp: th1.thread_exists)
done
}
moreover
{ let ?role = "done @ Recv l pt # todo"
note IH = recv(2)
assume "?new"
hence cur_thread: "?role = done' @ todo'" "i = i'"
using recv by auto
have ?case
proof(cases "\<exists> step' \<in> set done. MVar n \<in> FV (stepPat step')")
case True
with recv
obtain step''
where FV: "MVar n \<in> FV (stepPat step'')"
and step'': "step'' \<in> set done"
by auto
thus ?thesis
proof(cases "step'' \<in> skipped")
case False
then obtain step'
where FV: "MVar n \<in> FV (stepPat step')"
and notinSkipped: "step' \<notin> skipped"
and step': "(i,step') \<in> steps t"
using FV step''
by(auto simp add: th1.in_steps_conv_done_skipped)
hence "s (MV n i) \<in> typing (?role, n) i (t, r, s)"
by (auto intro!: IH th1.thread_exists)
hence "s (MV n i') \<in> typing (done'@todo', n) i' (t, r, s)"
using cur_thread by simp
thus ?thesis
apply -
apply(rule monoTyp_freeD[OF monoTyp])
apply(auto simp: th1.thread_exists)
done
next
case True
then obtain step'
where FV: "MVar n \<in> FV (stepPat step')"
and inSkipped: "step' \<in> skipped"
and inDone: "step' \<in> set done"
using FV step''
by auto
then obtain l' ty' pt'
where noteEq: "(Note l' ty' pt') = step'"
by(auto dest!: th1.note_in_skipped)
hence "\<exists> l'' pt''. listOrd ?role (Recv l'' pt'') (Note l' ty' pt') \<and> MVar n \<in> FV (stepPat (Recv l'' pt''))"
using FV inSkipped inDone
apply -
apply(drule FV_FMV_conv[THEN iffD2])
apply(subgoal_tac "Note l' ty' pt' \<in> set ?role")
apply(drule th1.Note_FV)
by (auto dest: FV_FMV_conv[THEN iffD1])
then obtain l'' pt''
where roleBefore: "listOrd ?role (Recv l'' pt'') (Note l' ty' pt')"
and varOfRecv: "MVar n \<in> FV (stepPat (Recv l'' pt''))"
by auto
hence "Recv l'' pt'' \<in> set done"
using inDone noteEq
apply -
apply(drule listOrd_append[THEN iffD1])
apply(case_tac "listOrd done (Recv l'' pt'') (Note l' ty' pt')")
apply(fastsimp dest: in_set_listOrd1)
apply(case_tac "listOrd (Recv l pt # todo) (Recv l'' pt'') (Note l' ty' pt')")
apply(fastsimp dest: in_set_listOrd2 th1.done_notin_todoD)
apply(case_tac "Recv l'' pt'' \<in> set done \<and> Note l' ty' pt' \<in> set (Recv l pt # todo)")
by(auto dest: th1.done_notin_todoD)
hence "(i, Recv l'' pt'') \<in> steps t" by auto
hence "s (MV n i) \<in> typing (?role, n) i (t, r, s)"
using varOfRecv by (auto intro!: IH th1.thread_exists)
hence "s (MV n i') \<in> typing (done'@todo', n) i' (t, r, s)"
using cur_thread by simp
thus ?thesis
apply -
apply(rule monoTyp_freeD[OF monoTyp])
apply(auto simp: th1.thread_exists)
done
qed
next
case False
moreover have "(t, r, s) \<in> approx typing"
by (auto simp: approx_unfold dest!: IH roleMap_SomeD)
moreover have "MVar n \<in> FV pt"
using `MVar n \<in> FV (stepPat step)` `?new` by auto
moreover note `Some m = inst s i pt`
moreover note `m \<in> knows t`
moreover note cur_thread[symmetric]
ultimately show ?thesis
apply -
apply(clarsimp simp del: fun_upd_apply)
apply(rule recv_case)
apply(simp_all add: th1.role_in_P th1.roleMap th1.thread_exists
in_set_splits_conv remove_hints)
done
qed
}
ultimately show ?case by fastsimp
next
case (compr t r s i "done" l ty pt todo skipped m i' done' todo' step n skipped')
then interpret th1:
reachable_thread P t r s i "done" "Note l ty pt # todo" skipped
by unfold_locales auto
from compr
have "(i', step) \<in> steps t \<or> (i' = i) \<and> step = Note l ty pt"
(is "?old \<or> ?new") by auto
moreover
{ assume ?old
hence "s(MV n i') \<in> typing (done'@todo', n) i' (t,r,s)"
using compr by (auto split: if_splits)
hence ?case
proof(rule monoTyp_freeD[OF monoTyp])
qed (auto simp: th1.thread_exists)
}
moreover
{ let ?role = "done @ Note l ty pt # todo"
note IH = compr(2)
assume "?new"
hence "MVar n \<in> FV pt"
using compr by auto
then obtain l' msg'
where "(i, Recv l' msg') \<in> steps t"
"MVar n \<in> FV msg'"
by (fastsimp dest!: th1.note_step_FV[OF th1.thread_exists])
hence typed: "s (MV n i) \<in> typing (?role, n) i (t, r, s)"
by (auto dest: IH[OF th1.thread_exists])
have "done'@todo' = ?role"
using compr `?new` by auto
hence ?case using `?new`
apply -
apply(rule monoTyp_freeD[OF monoTyp])
by (auto intro!: typed simp: th1.thread_exists)
}
ultimately show ?case by fast
next
case (skip t r s i "done" l ty pt todo skipped i' done' todo' step n skipped')
then interpret th1:
reachable_thread P t r s i "done" "Note l ty pt # todo" skipped
by unfold_locales auto
from skip
have "(i', step) \<in> steps t" (is "?old") by auto
hence "s(MV n i') \<in> typing (done'@todo', n) i' (t,r,s)"
using skip by (auto split: if_splits)
thus ?case
proof(rule monoTyp_freeD[OF monoTyp])
qed (auto simp: th1.thread_exists)
qed (auto intro: monoTyp_appendD[OF monoTyp])
}
thus ?thesis unfolding approx_unfold by(auto elim!: roleMap_SomeE)
qed
text{*
We prove a variant of the above lemma, which is suitable for
automation. The difference is the description of the variables
that need to be checked. Here, it is done such that Isabelle's
simplifier gets a finite set that it can rewrite into normal
form.
*}
lemma (in reachable_state) reachable_in_approxI_ext:
assumes monoTyp: "monoTyp typing"
and recv_case:
"\<And> t r s i done todo skipped m R step n.
\<lbrakk> R \<in> P;
roleMap r i = Some R;
(done, step # todo) \<in> set (splits R);
recvStep step;
MVar n \<in> foldl (\<lambda> fv step'. fv - FV (stepPat step')) (FV (stepPat step)) done;
hint ''completenessCase'' (step, n);
(t,r,s) \<in> reachable P;
(t,r,s) \<in> approx typing;
r i = Some (done, step # todo ,skipped);
Some m = inst s i (stepPat step);
m \<in> knows t
\<rbrakk> \<Longrightarrow>
s (MV n i) \<in> typing (R, n) i ( t @ [Step (i, step)], r(i \<mapsto> (done @ [step], todo, skipped)), s)"
shows "(t,r,s) \<in> approx typing"
proof(induct rule: reachable_in_approxI[OF monoTyp])
case (1 t r s i "done" todo skipped m R step n)
{ fix v V
assume "v \<in> V"
and "\<forall>step'\<in>set done. v \<notin> FV (stepPat step')"
hence "v \<in> foldl (\<lambda> fv step'. fv - FV (stepPat step')) V done"
by (induct "done" arbitrary: V) auto
}
hence "MVar n \<in> foldl (\<lambda> fv step'. fv - FV (stepPat step')) (FV (stepPat step)) done"
using 1 by auto
thus ?case using 1
apply(subgoal_tac "True")
apply(clarsimp)
apply(rule recv_case)
by(assumption | simp add: remove_hints)+
qed
text{* Proving typing monotonicity *}
subsubsection{* Monotonicity Proofs *}
definition monoMsgTyp :: "msgtype \<Rightarrow> bool"
where "monoMsgTyp ty \<equiv>
(\<forall>i t r s t' r'.
roleMap r \<subseteq>\<^sub>m roleMap r' \<longrightarrow>
ty i (t, r, s) \<subseteq> ty i (t @ t', r', s))"
lemma monoMsgTypD:
"\<lbrakk> monoMsgTyp ty;
m \<in> ty i (t,r,s);
roleMap r \<subseteq>\<^sub>m roleMap r'
\<rbrakk> \<Longrightarrow>
m \<in> ty i (t@t',r',s)"
unfolding monoMsgTyp_def by blast
lemma monoMsgTyp_SumTI[intro!]:
assumes ty1: "monoMsgTyp ty1"
and ty2: "monoMsgTyp ty2"
shows "monoMsgTyp (SumT ty1 ty2)"
by(auto simp: monoMsgTyp_def SumT_def
dest: monoMsgTypD[OF ty1] monoMsgTypD[OF ty2])
lemma monoMsgTyp_InterTI[intro!]:
assumes ty1: "monoMsgTyp ty1"
and ty2: "monoMsgTyp ty2"
shows "monoMsgTyp (InterT ty1 ty2)"
by(auto simp: monoMsgTyp_def InterT_def
dest: monoMsgTypD[OF ty1] monoMsgTypD[OF ty2])
lemma monoMsgTyp_KnownTI[iff]:
shows "monoMsgTyp (KnownT step)"
by(auto simp: monoMsgTyp_def KnownT_def )
lemma monoMsgTyp_NonceTI[iff]:
shows "monoMsgTyp (NonceT R n)"
by(auto simp: monoMsgTyp_def NonceT_def dest: map_leD)
lemma monoMsgTyp_ConstTI[iff]:
shows "monoMsgTyp (ConstT c)"
by(auto simp: monoMsgTyp_def ConstT_def dest: map_leD)
lemma monoMsgTyp_AgentTI[iff]:
shows "monoMsgTyp AgentT"
by(auto simp: monoMsgTyp_def AgentT_def dest: map_leD)
lemma monoMsgTyp_EncTI[intro!]:
assumes ty1: "monoMsgTyp ty1"
and ty2: "monoMsgTyp ty2"
shows "monoMsgTyp (EncT ty1 ty2)"
by(auto simp: monoMsgTyp_def EncT_def
dest: monoMsgTypD[OF ty1] monoMsgTypD[OF ty2])
lemma monoMsgTyp_KTI[intro!]:
assumes ty1: "monoMsgTyp ty1"
and ty2: "monoMsgTyp ty2"
shows "monoMsgTyp (KT ty1 ty2)"
by(auto simp: monoMsgTyp_def KT_def
dest: monoMsgTypD[OF ty1] monoMsgTypD[OF ty2])
lemma monoMsgTyp_KShrTI[intro!]:
shows "monoMsgTyp KShrT"
by(auto simp: monoMsgTyp_def KShrT_def)
lemma monoMsgTyp_TupTI[intro!]:
assumes ty1: "monoMsgTyp ty1"
and ty2: "monoMsgTyp ty2"
shows "monoMsgTyp (TupT ty1 ty2)"
by(auto simp: monoMsgTyp_def TupT_def
dest: monoMsgTypD[OF ty1] monoMsgTypD[OF ty2])
lemma monoMsgTyp_HashTI[intro!]:
assumes ty: "monoMsgTyp ty"
shows "monoMsgTyp (HashT ty)"
by(auto simp: monoMsgTyp_def HashT_def
dest: monoMsgTypD[OF ty])
lemma monoMsgTyp_PKTI[intro!]:
assumes ty: "monoMsgTyp ty"
shows "monoMsgTyp (PKT ty)"
by(auto simp: monoMsgTyp_def PKT_def
dest: monoMsgTypD[OF ty])
lemma monoMsgTyp_SKTI[intro!]:
assumes ty: "monoMsgTyp ty"
shows "monoMsgTyp (SKT ty)"
by(auto simp: monoMsgTyp_def SKT_def
dest: monoMsgTypD[OF ty])
lemma monoTyp_mk_typing[intro!]:
assumes monoMsgTyp:
"\<And> pos ty. (pos, ty) \<in> set tyeqs \<Longrightarrow> monoMsgTyp ty"
shows "monoTyp (mk_typing tyeqs)"
using monoMsgTyp
proof(induct tyeqs)
case Nil thus ?case
by(auto intro!: monoTypI simp: mk_typing_def EmptyT_def)
next
case (Cons tyeq tyeqs)
thus ?case
proof(cases tyeq)
case (Pair pos' ty')
have mk_typing_Cons [simp]:
"mk_typing ((pos',ty')#tyeqs) = (mk_typing tyeqs)(pos' := ty')"
by (simp add: mk_typing_def)
with Pair show ?thesis
apply(auto intro!: monoTypI)
apply(auto intro: monoTypD[OF Cons(1), OF Cons(2)]
monoMsgTypD[OF Cons(2)]
simp: Pair)
done
qed
qed
subsection{* Automation *}
text{*
The automation of the welltypedness proofs is rather fragile.
As a general rule of operation we try to unfold type information
as late as possible. This allows to guide the automation tools
by matching on the structure of the types. However, it also
implies that more rules are necessary. Moreover the current set
of rules is not guaranteed to be complete.
*}
subsubsection{* ACI of Sum and Intersection Types *}
lemma SumT_absorb [simp]: "SumT ty ty = ty"
by (rule ext, rule ext) (auto simp: SumT_def)
lemma SumT_left_absorb: "SumT ty1 (SumT ty1 ty2) = SumT ty1 ty2"
by (rule ext, rule ext) (auto simp: SumT_def)
lemma SumT_commute: "SumT ty1 ty2 = SumT ty1 ty2"
by (rule ext, rule ext) (auto simp: SumT_def)
lemma SumT_left_commute: "SumT ty1 (SumT ty2 ty3) = SumT ty2 (SumT ty1 ty3)"
by (rule ext, rule ext) (auto simp: SumT_def)
lemma SumT_assoc: "SumT (SumT ty1 ty2) ty3 = SumT ty1 (SumT ty2 ty3)"
by (rule ext, rule ext) (auto simp: SumT_def)
lemmas SumT_ac = SumT_assoc SumT_left_absorb SumT_commute SumT_left_commute
-- {* Type sum is an AC-operator *}
lemma InterT_absorb [simp]: "InterT ty ty = ty"
by (rule ext, rule ext) (auto simp: InterT_def)
lemma InterT_left_absorb: "InterT ty1 (InterT ty1 ty2) = InterT ty1 ty2"
by (rule ext, rule ext) (auto simp: InterT_def)
lemma InterT_commute: "InterT ty1 ty2 = InterT ty1 ty2"
by (rule ext, rule ext) (auto simp: InterT_def)
lemma InterT_left_commute: "InterT ty1 (InterT ty2 ty3) = InterT ty2 (InterT ty1 ty3)"
by (rule ext, rule ext) (auto simp: InterT_def)
lemma InterT_assoc: "InterT (InterT ty1 ty2) ty3 = InterT ty1 (InterT ty2 ty3)"
by (rule ext, rule ext) (auto simp: InterT_def)
lemmas InterT_ac = InterT_assoc InterT_left_absorb InterT_commute InterT_left_commute
-- {* Type intersection is an AC-operator *}
subsubsection{* Type Membership *}
text{* Special types *}
text{* The rules for SumT are special, as their usage currently
depends on the combination of SumT and KnownT.
*}
lemma in_SumTE:
"\<lbrakk> m \<in> SumT ty1 ty2 i q; m \<in> ty1 i q \<Longrightarrow> R; m \<in> ty2 i q \<Longrightarrow> R
\<rbrakk> \<Longrightarrow> R"
by(auto simp: SumT_def)
lemma notin_SumTE [elim!]:
"\<lbrakk> m \<notin> SumT ty1 ty2 i q;
\<lbrakk> m \<notin> ty1 i q; m \<notin> ty2 i q \<rbrakk> \<Longrightarrow> R
\<rbrakk> \<Longrightarrow> R"
by(auto simp: SumT_def)
lemma notin_KnownT_append_StepE [dest!]:
"m \<notin> KnownT step i (t@ [Step (i, step)], r, s) \<Longrightarrow>
m \<notin> knows t"
by(auto simp: KnownT_def)
text{* Direct unfoldings *}
lemma in_ConstT_simp [iff]:
"(m \<in> ConstT c i q) = (m = LC c)"
by(auto simp: ConstT_def)
lemma in_KnownTD [dest!]:
"(x \<in> KnownT step i (t,r,s)) \<Longrightarrow> (predOrd t (Ln x) (St (i, step)))"
by(simp add: KnownT_def)
text{* To be used together with if\_splits in a well-typedness
proof *}
lemma in_NonceT [simp]:
"(LN n i \<in> NonceT R n i' (t,r,s)) = (roleMap r i = Some R)"
by(simp add: NonceT_def)
lemma in_NonceTE [elim!]:
"\<lbrakk> m \<in> NonceT R n i (t,r,s);
\<And> nTid. \<lbrakk> m = LN n nTid; roleMap r nTid = Some R \<rbrakk> \<Longrightarrow> Q
\<rbrakk> \<Longrightarrow> Q"
by(auto simp: NonceT_def)
lemma notin_NonceT_thenonceE [elim!]:
"\<lbrakk> LN n nTid \<notin> NonceT nR n i (t, r(i \<mapsto> (done,todo,skipped)), s);
nTid = i \<Longrightarrow> Q;
\<lbrakk> nTid \<noteq> i; roleMap r nTid \<noteq> Some nR \<rbrakk> \<Longrightarrow> Q
\<rbrakk> \<Longrightarrow> Q"
by(auto simp: NonceT_def split: if_splits)
text{* These rules ensure that type information is exploited
when a match impossible without intruder activity happening.
*}
lemma Tup_in_SumT_KnownT_NonceTD [dest!]:
"Tup x y \<in> SumT (KnownT step) (NonceT R n) i (t, r, s)
\<Longrightarrow> predOrd t (Ln (Tup x y)) (St (i, step))"
by(auto simp: KnownT_def SumT_def)
lemma Hash_in_SumT_KnownT_NonceTD [dest!]:
"Hash x \<in> SumT (KnownT step) (NonceT R n) i (t, r, s)
\<Longrightarrow> predOrd t (Ln (Hash x)) (St (i, step))"
by(auto simp: KnownT_def SumT_def)
lemma Enc_in_SumT_KnownT_NonceTD [dest!]:
"Enc x y \<in> SumT (KnownT step) (NonceT R n) i (t, r, s)
\<Longrightarrow> predOrd t (Ln (Enc x y)) (St (i, step))"
by(auto simp: KnownT_def SumT_def)
text{* TODO: Extend these lemmas for further combinations. This requires
some more thinking. However, for a well-designed protocols the message
structure is not required for disambiguation because the encryptions
contain tags that identify them.
*}
text{* Structural types *}
text{* The following rules are used in well-typedness proofs *}
lemma Hash_in_HashT [simp]:
"(Hash x \<in> HashT ty i q) = (x \<in> ty i q)"
by (simp add: HashT_def)
lemma Tup_in_TupT [simp]:
"(Tup x y \<in> TupT ty1 ty2 i q) = (x \<in> ty1 i q \<and> y \<in> ty2 i q)"
by (simp add: TupT_def)
lemma Enc_in_EncT [simp]:
"(Enc x y \<in> EncT ty1 ty2 i q) = (x \<in> ty1 i q \<and> y \<in> ty2 i q)"
by (simp add: EncT_def)
lemma PK_in_PKT [simp]: "(PK x \<in> PKT ty i q) = (x \<in> ty i q)"
by (simp add: PKT_def)
lemma SK_in_SKT [simp]: "(SK x \<in> SKT ty i q) = (x \<in> ty i q)"
by (simp add: SKT_def)
lemma K_in_KT [simp]:
"(K x y \<in> KT ty1 ty2 i q) = (x \<in> ty1 i q \<and> y \<in> ty2 i q)"
by (simp add: KT_def)
text{* The following rules ensure that messages are expanded
automatically in when applying the sources rule.
*}
lemma in_HashTE [elim!]:
"\<lbrakk> m \<in> HashT ty i q;
\<And> x. \<lbrakk> m = Hash x; x \<in> ty i q \<rbrakk> \<Longrightarrow> Q
\<rbrakk> \<Longrightarrow> Q"
by(auto simp: HashT_def)
lemma in_EncTE [elim!]:
"\<lbrakk> m \<in> EncT ty1 ty2 i q;
\<And> x k. \<lbrakk> m = Enc x k; x \<in> ty1 i q; k \<in> ty2 i q \<rbrakk> \<Longrightarrow> Q
\<rbrakk> \<Longrightarrow> Q"
by(auto simp: EncT_def)
lemma in_TupTE [elim!]:
"\<lbrakk> m \<in> TupT ty1 ty2 i q;
\<And> x y. \<lbrakk> m = \<lbrace> x, y \<rbrace>; x \<in> ty1 i q; y \<in> ty2 i q \<rbrakk> \<Longrightarrow> Q
\<rbrakk> \<Longrightarrow> Q"
by(auto simp: TupT_def)
lemma in_KTE [elim!]:
"\<lbrakk> m \<in> KT ty1 ty2 i q;
\<And> x y. \<lbrakk> m = K x y; x \<in> ty1 i q; y \<in> ty2 i q \<rbrakk> \<Longrightarrow> Q
\<rbrakk> \<Longrightarrow> Q"
by(auto simp: KT_def)
lemma in_PKTE [elim!]:
"\<lbrakk> m \<in> PKT ty i q;
\<And> x. \<lbrakk> m = PK x; x \<in> ty i q \<rbrakk> \<Longrightarrow> Q
\<rbrakk> \<Longrightarrow> Q"
by(auto simp: PKT_def)
lemma in_SKTE [elim!]:
"\<lbrakk> m \<in> SKT ty i q;
\<And> x. \<lbrakk> m = SK x; x \<in> ty i q \<rbrakk> \<Longrightarrow> Q
\<rbrakk> \<Longrightarrow> Q"
by(auto simp: SKT_def)
subsection{* Specialization of the Chain Rule *}
text{* We prove the case distinction on messages known to the
intruder with respect to an typed state, because we need
a sufficiently precise invariant when reasoning about the
contents of a variable.
*}
lemma (in typed_state) knows_cases:
assumes known: "m' \<in> knows t"
shows "
(m' \<in> IK0 \<and>
hint ''case_name'' ''ik0''
) \<or>
(\<exists> m. m' = Hash m \<and> Ln m \<prec> Ln (Hash m) \<and>
hint ''case_name'' ''fake''
) \<or>
(\<exists> m k. m' = Enc m k \<and>
Ln m \<prec> Ln (Enc m k) \<and> Ln k \<prec> Ln (Enc m k) \<and>
hint ''case_name'' ''fake''
) \<or>
(\<exists> x y. m' = Tup x y \<and>
Ln x \<prec> Ln (Tup x y) \<and> Ln y \<prec> Ln (Tup x y) \<and>
hint ''case_name'' ''fake''
) \<or>
(\<exists> R \<in> P. \<exists> i. roleMap r i = Some R \<and>
(\<exists> step \<in> set R.
(sendStep step \<or> noteStep step) \<and>
(\<exists> m. Some m = inst s i (stepPat step) \<and> decrChain [] t {St (i, step)} m m') \<and>
prefixClose s t R step i \<and>
(\<forall> v \<in> FV (stepPat step). \<forall> n. v = MVar n \<longrightarrow>
s (MVar n, i) \<in> typing (R, n) i (t,r,s)) \<and>
hint ''decrChainFrom'' (i, R, step) \<and>
hint ''case_name'' ''decrypt''
)
) \<or>
(\<exists> a. m' = SK a \<and> LKR a \<prec> Ln m' \<and> hint ''case_name'' ''asym_lkr'') \<or>
(\<exists> a b. m' = K a b \<and> LKR a \<prec> Ln m' \<and> hint ''case_name'' ''sym_lkr1'') \<or>
(\<exists> a b. m' = K a b \<and> LKR b \<prec> Ln m' \<and> hint ''case_name'' ''sym_lkr2'') \<or>
(\<exists> A. \<exists> a \<in> A. m' = KShr A \<and> LKR (LAg a) \<prec> Ln m' \<and> hint ''case_name'' ''shr_lkr'')
"
(is "?ik0 \<or> ?hash \<or> ?encr \<or> ?tup \<or> ?decr \<or> ?keys")
proof -
from known have
"(m' \<in> IK0) \<or>
(\<exists> m. m' = Hash m \<and> Ln m \<prec> Ln (Hash m)) \<or>
(\<exists> m k. m' = Enc m k \<and> Ln m \<prec> Ln (Enc m k) \<and> Ln k \<prec> Ln (Enc m k)) \<or>
(\<exists> x y. m' = Tup x y \<and> Ln x \<prec> Ln (Tup x y) \<and> Ln y \<prec> Ln (Tup x y)) \<or>
(\<exists> i done todo skipped. r i = Some (done, todo, skipped) \<and>
(\<exists> l pt m.
Send l pt \<in> set done \<and> Some m = inst s i pt \<and>
decrChain [] t {St (i, Send l pt)} m m'
)
) \<or>
(\<exists> i done todo skipped. r i = Some (done, todo, skipped) \<and>
(\<exists> l ty pt m.
Note l ty pt \<in> set done \<and> Note l ty pt \<notin> skipped \<and>
Some m = inst s i pt \<and>
decrChain [] t {St (i, Note l ty pt)} m m'
)
) \<or>
(\<exists> a. m' = SK a \<and> LKR a \<prec> Ln m') \<or>
(\<exists> a b. m' = K a b \<and> LKR a \<prec> Ln m') \<or>
(\<exists> a b. m' = K a b \<and> LKR b \<prec> Ln m') \<or>
(\<exists> A. \<exists> a \<in> A. m' = KShr A \<and> LKR (LAg a) \<prec> Ln m')
"
(is "?ik0_raw \<or> ?hash_raw \<or> ?encr_raw \<or> ?tup_raw \<or> ?decr_raw \<or> ?note_raw \<or> ?keys_raw")
by (rule knows_cases_raw)
moreover
{
assume "?ik0_raw"
hence ?thesis by( simp add: remove_hints)
}
moreover
{
assume "?hash_raw"
hence ?thesis by( simp add: remove_hints)
}
moreover
{
assume "?encr_raw"
hence ?thesis by( simp add: remove_hints)
}
moreover
{
assume "?tup_raw"
hence ?thesis by( simp add: remove_hints)
}
moreover
{
assume "?keys_raw"
hence ?thesis by( simp add: remove_hints)
}
moreover
{ assume ?decr_raw then
obtain i "done" todo l msg skipped m
where thread_exists: "r i = Some (done, todo,skipped)"
and send_done: "Send l msg \<in> set done"
and msg: "Some m = inst s i msg"
and decrChain: "decrChain [] t {St (i, Send l msg)} m m'"
by fast
then interpret th1: typed_thread P t r s i "done" todo skipped "typing"
using approximates by unfold_locales
from send_done have send_step: "(i, Send l msg) \<in> steps t"
by (rule th1.in_steps_send[THEN iffD1])
moreover
have "prefixClose s t (done@todo) (Send l msg) i" using send_step
by(auto intro!: prefixCloseI th1.roleMap)
moreover
have send_in_role: "Send l msg \<in> set (done @ todo)"
using send_done by simp
moreover
note in_approxD[OF th1.approximates send_step th1.roleMap, simplified]
ultimately
have ?decr using decrChain msg
apply -
apply(rule bexI[OF _ th1.role_in_P])
apply(rule exI)
apply(rule conjI[OF th1.roleMap])
apply(rule bexI[OF _ send_in_role])
by(auto simp: remove_hints)
hence ?thesis by blast
}
moreover
{
assume ?note_raw
then obtain i "done" todo skipped l ty pt m
where thread_exists: "r i = Some (done, todo,skipped)"
and inDone: "Note l ty pt \<in> set done"
and notinSkipped: "Note l ty pt \<notin> skipped"
and msg: "Some m = inst s i pt"
and decrChain: "decrChain [] t {St (i, Note l ty pt)} m m'"
by fast
then interpret th1: typed_thread P t r s i "done" todo skipped "typing"
using approximates by unfold_locales
from inDone and notinSkipped have note_step: "(i, Note l ty pt) \<in> steps t"
by (fastsimp dest!: th1.in_steps_eq_in_done)
moreover
have "prefixClose s t (done@todo) (Note l ty pt) i" using note_step
by(auto intro!: prefixCloseI th1.roleMap)
moreover
have note_in_role: "Note l ty pt \<in> set (done @ todo)"
using inDone by simp
moreover
note in_approxD[OF th1.approximates note_step th1.roleMap, simplified]
ultimately
have ?decr using decrChain msg
apply -
apply(rule bexI[OF _ th1.role_in_P])
apply(rule exI)+
apply(rule conjI[OF th1.roleMap])
apply(rule bexI[OF _ note_in_role])
by(auto simp: remove_hints)
hence ?thesis by blast
}
ultimately
show ?thesis by fastsimp
qed
lemma (in reachable_state) decrChain_AgentE:
assumes decrChain: "decrChain path t from m m'"
and Agent: "m \<in> Agent"
and nonempty: "from = {} \<Longrightarrow> Q"
shows "Q"
using decrChain Agent nonempty
by (auto simp: Agent_def)
(*
lemma (in reachable_state) decrChain_AgentTE:
assumes decrChain: "decrChain path t from m m'"
and AgentT: "m \<in> AgentT i (t,r,s)"
and elim: "m = m' \<Longrightarrow> Q"
shows "Q"
using decrChain AgentT elim
by (auto simp: AgentT_def)
*)
lemma (in reachable_state) decrChain_imp_predOrd:
"\<lbrakk> decrChain path t from m m' \<rbrakk> \<Longrightarrow>
\<exists> im \<in> pairParts m. (\<forall> f \<in> from. f \<prec> Ln im) \<and> Ln im \<preceq> Ln m'"
proof(induct m arbitrary: path "from")
case (Tup x y) thus ?case
apply(simp)
apply(erule disjE)
apply(clarsimp)
apply(rule disjI2)
apply(fastsimp intro: less_le_trans)
done
qed fastsimp+
lemma (in reachable_state) decrChain_KnownT:
assumes decrChain: "decrChain path t from m m'"
and KnownT: "predOrd t (Ln m) (St (i, step))"
shows "\<exists> im \<in> pairParts m.
(\<forall> f \<in> from. f \<prec> Ln im) \<and> Ln im \<prec> St (i, step)"
proof -
obtain im
where "im \<in> pairParts m" and "\<forall>f \<in> from. f \<prec> Ln im"
using decrChain by (fast dest!: decrChain_imp_predOrd)
with KnownT show ?thesis
by (fastsimp intro: pairParts_before)
qed
lemma (in reachable_state) decrChain_KnownTE:
assumes decrChain: "decrChain path t from m m'"
and KnownT: "predOrd t (Ln m) (St (i, step))"
and elim: "\<And> im. \<lbrakk> im \<in> pairParts m;
\<forall> f \<in> from. f \<prec> Ln im;
Ln im \<prec> St (i, step)
\<rbrakk> \<Longrightarrow> Q"
shows "Q"
using decrChain KnownT
by(auto dest!: decrChain_KnownT elim)
lemma (in reachable_state) decrChain_SumT_KnownTE:
assumes KnownT: "m \<in> SumT (KnownT step) ty i (t,r,s)"
and decrChain: "decrChain path t from m m'"
and elimK: "\<And> im. \<lbrakk> im \<in> pairParts m;
\<forall> f \<in> from. f \<prec> Ln im;
Ln im \<prec> St (i, step)
\<rbrakk> \<Longrightarrow> Q"
and elimTy: "m \<in> ty i (t,r,s) \<Longrightarrow> Q"
shows "Q"
using decrChain KnownT elimK elimTy
by(auto elim!: in_SumTE decrChain_KnownTE)
lemma (in reachable_state) AV_in_Agent [iff]:
"s (AV a aTid) \<in> Agent"
using inst_AVar_cases
by (auto simp: Agent_def)
end
(* TODO:
- Remove agent variables from protocol model by
replacing them with type annotations.
[General version will require us to reintroduce create event.
But composition becomes nicer, as we can now model protocols, which
use parameters that are secret values and so on.
]
- Put decryption chain case into recursion of chain
predicate to make more information available locally.
*)