Quelle  Trace.thy

(*<*)
theory Trace
imports Basis
begin

declare Let_def[simp] if_split_asm[split]
(*>*)

section‹A trace based model›

text‹The only clumsy aspect of the state based model is ‹safe›: we use a state component to record if the sequence of events
  lead to a state satisfies some property. That is, we simulate a
  on traces via the state. Unsurprisingly, it is not trivial
  convince oneself that ‹safe› really has the informal meaning
  out at the beginning of subsection~\ref{sec:formalizing-safety}.
  we now describe an alternative, purely trace based model,
  to Paulson's inductive protocol model~cite‹"Paulson-JCS98"›.
  events are:
 ›

datatype event =
  Check_in guest room card | Enter guest room card | Exit guest room

text‹Instead of a state, we have a trace, i.e.\ list of events, and
  the state from the trace:›

consts
  initk :: "room ==> key"
   
primrec owns :: "event list ==> room ==> guest option" where
"owns [] r = None" |
"owns (e#s) r = (case e of
 Check_in g r' c ==> if r' = r then Some g else owns s r |
 Enter g r' c ==> owns s r |
 Exit g r' ==> owns s r)"

primrec currk :: "event list ==> room ==> key" where
"currk [] r = initk r" |
"currk (e#s) r = (let k = currk s r in
    case e of Check_in g r' c ==> if r' = r then snd c else k
            | Enter g r' c ==> k
            | Exit g r ==> k)"

primrec issued :: "event list ==> key set" where
"issued [] = range initk" |
"issued (e#s) = issued s ∪
  (case e of Check_in g r c ==> {snd c} | Enter g r c ==> {} | Exit g r ==> {})"

primrec cards :: "event list ==> guest ==> card set" where
"cards [] g = {}" |
"cards (e#s) g = (let C = cards s g in
                    case e of Check_in g' r c ==> if g' = g then insert c C
                                                else C
                            | Enter g r c ==> C
                            | Exit g r ==> C)"

primrec roomk :: "event list ==> room ==> key" where
"roomk [] r = initk r" |
"roomk (e#s) r = (let k = roomk s r in
    case e of Check_in g r' c ==> k
            | Enter g r' (x,y) ==> if r' = r 🍋‹∧ x = k› then y else k
            | Exit g r ==> k)"

primrec isin :: "event list ==> room ==> guest set" where
"isin [] r = {}" |
"isin (e#s) r = (let G = isin s r in
                 case e of Check_in g r c ==> G
                 | Enter g r' c ==> if r' = r then {g} ∪ G else G
                 | Exit g r' ==> if r'=r then G - {g} else G)"

primrec hotel :: "event list ==> bool" where
"hotel [] = True" |
"hotel (e # s) = (hotel s & (case e of
  Check_in g r (k,k') ==> k = currk s r ∧ k' ∉ issued s |
  Enter g r (k,k') ==> (k,k') : cards s g & (roomk s r : {k, k'}) |
  Exit g r ==> g : isin s r))"

text‹Except for @{const initk}, which is completely unspecified,
  these functions are defined by primitive recursion over traces:
 {thm[display]owns.simps}
 {thm[display]currk.simps}
 {thm[display]issued.simps}
 {thm[display]cards.simps}
 {thm[display]roomk.simps}
 {thm[display]isin.simps}

 , not every trace is possible. Function @{const hotel} tells us
  traces correspond to real hotels:
 {thm[display]hotel.simps}
  we could have followed Paulson~cite‹"Paulson-JCS98"›
  defining @{const hotel} as an inductive set of traces.
  difference is only slight.

 subsection{Formalizing safety}
 label{sec:FormalSafetyTrace}

  principal advantage of the trace model is the intuitive
  of safety. Using the auxiliary predicate ‹no_Check_in›
 ›

(*<*)abbreviation no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
"no_Check_in s r ≡ ¬(∃g c. Check_in g r c ∈ set s)"

text‹\medskip\noindent we define a trace to be ‹safe₀› for a
  if the card obtained at the last @{const Check_in} was later
  used to @{const Enter} the room:›

(*<*)definition safe\<^sub>0 :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
"safe₀ s r = (∃s₁ s₂ s₃ g c.
 s = s₃ @ [Enter g r c] @ s₂ @ [Check_in g r c] @ s₁ ∧ no_Check_in (s₃ @ s₂) r)"

text‹\medskip\noindent A trace is ‹safe› if additionally the room was
  when it was entered:›

(*<*)definition safe :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
"safe s r = (∃s₁ s₂ s₃ g c.
 s = s₃ @ [Enter g r c] @ s₂ @ [Check_in g r c] @ s₁ ∧
 no_Check_in (s₃ @ s₂) r ∧ isin (s₂ @ [Check_in g r c] @ s₁) r = {})"

text‹\medskip\noindent The two notions of safety are distinguished because,
  for the main theorem, @{const safe₀} suffices.

  alert reader may already have wondered why, in contrast to the
  based model, we do not require @{const initk} to be
 . If @{const initk} is not injective, e.g.\ @{prop"initk
 ₁ = initk r₂"} and @{prop"r₁ ≠ r₂"},
  @{term"[Enter g r₂ (initk r₁,k), Check_in g
 ₁ (initk r₁,k)]"} is a legal trace and guest ‹g› ends up in a room he is not the owner of. However, this is not a
  trace for room ‹r₂› according to our
 . This reflects that hotel rooms are not safe until
  first time their owner has entered them. We no longer protect the
  from its guests.›

(* state thm w/o "isin"
hotel s ==> s = Enter g # s' \<Longrightarrow> owns s' r = Some g \<or> s' = s1 @ Checkin g @ s2 \<and> 
no checkin, no enter in s1

*)

(*<*)
lemma safe_safe: "safe s r ==> safe₀ s r"
by (simp add: safe₀_def safe_def) blast

lemma initk_issued[simp]: "hotel s ==> initk r ∈ issued s"
by (induct s) (auto split:event.split)

lemma currk_issued[simp]: "hotel s ==> currk s r ∈ issued s"
by (induct s) (auto split:event.split)

lemma key1_issued[simp]: "hotel s ==> (k,k') : cards s g ==> k ∈ issued s"
by (induct s) (auto split:event.split)

lemma key2_issued[simp]: "hotel s ==> (k,k') : cards s g ==> k' ∈ issued s"
by (induct s) (auto split:event.split)

lemma roomk_issued[simp]: "hotel s ==> roomk s r ∈ issued s"
by (induct s) (auto split:event.split)

lemma issued_app: "issued (s @ s') = issued s ∪ issued s'"
apply (induct s) apply (auto split:event.split)
apply (induct s') apply (auto split:event.split)
done

lemma owns_app[simp]: "no_Check_in s₂ r ==> owns (s₂ @ s₁) r = owns s₁ r"
by (induct s₂) (auto split:event.split)

lemma currk_app[simp]: "no_Check_in s₂ r ==> currk (s₂ @ s₁) r = currk s₁ r"
by (induct s₂) (auto split:event.split)

lemma currk_Check_in:
 "[ hotel (s₂ @ Check_in g r (k, k')# s₁);
    k' = currk (s₂ @ Check_in g r (k, k') # s₁) r' ] ==> r' = r"
by (induct s₂) (auto simp: issued_app split:event.splits)

lemma no_checkin_no_newkey:
"[ hotel(s₂ @ [Check_in g r (k,k')] @ s₁); no_Check_in s₂ r ]
 ==> (k',k'') ∉ cards (s₂ @ Check_in g r (k,k') # s₁) g'"
apply(induct s₂)
 apply fastforce
apply(fastforce split:event.splits dest: currk_Check_in)
done

lemma guest_key2_disj2[simp]: 
"[ hotel s; (k₁,k) ∈ cards s g₁; (k₂,k) ∈ cards s g₂ ] ==> g₁=g₂"
apply (induct s)
apply(auto split:event.splits)
done

lemma safe_roomk_currk[simp]:
 "hotel s ==> safe₀ s r ==> roomk s r = currk s r"
apply(clarsimp simp:safe₀_def)
apply(hypsubst_thin)
apply(erule rev_mp)+
apply(induct_tac s₃)
apply(auto split:event.split)
apply(rename_tac guest ba)
apply(subgoal_tac "(b, ba)
        ∉ cards ((list @ Enter g r (a, b) # s₂) @ Check_in g r (a, b) # s₁)
           guest")
apply simp
apply(rule no_checkin_no_newkey) apply simp_all
done

lemma only_owner_enter_normal:
 "[ hotel s; safe₀ s r; (k,roomk s r) ∈ cards s g ] ==> owns s r = Some g"
apply(clarsimp simp:safe₀_def)
apply(hypsubst_thin)
apply(erule rev_mp)+
apply(induct_tac s₃)
 apply (fastforce)
apply (auto simp add:issued_app split:event.split)
done

(* A short proof *)
lemma "[ hotel s; safe s r; g ∈ isin s r ] ==> owns s r = Some g"
apply(clarsimp simp add:safe_def)
apply(hypsubst_thin)
apply(rename_tac g' k k')
apply(erule rev_mp)+
apply(induct_tac s₃)
 apply simp
apply (auto split:event.split)
 apply(subgoal_tac
 "safe₀ (list @ Enter g' r (k,k') # s₂ @ Check_in g' r (k, k') # s₁) r")
  prefer 2
  apply(simp add:safe₀_def)apply blast
 apply(simp)
 apply(cut_tac s₂ = "list @ Enter g' r (k, k') # s₂" in no_checkin_no_newkey)
   apply simp
  apply simp
 apply simp
 apply fast
apply(subgoal_tac
 "safe₀ (list @ Enter g' r (k,k') # s₂ @ Check_in g' r (k, k') # s₁) r")
 apply(drule (1) only_owner_enter_normal)
  apply blast
 apply simp
apply(simp add:safe₀_def)
apply blast
done

lemma in_set_conv_decomp_firstD:
assumes "P x"
shows "x ∈ set xs ==>
  ∃ys x zs. xs = ys @ x # zs ∧ P x ∧ (∀y ∈ set ys. ¬ P y)"
  (is "_ ==> ∃ys x zs. ?P xs ys x zs")
proof (induct xs)
  case Nil thus ?case by simp
next
  case (Cons a xs)
  show ?case
  proof cases
    assume "x = a ∨ P a" hence "?P (a#xs) [] a xs" using ‹P x› by auto
    thus ?case by blast
  next
    assume "¬(x = a ∨ P a)"
    with assms Cons show ?case by clarsimp (fastforce intro!: Cons_eq_appendI)
  qed
qed

lemma ownsD: "owns s r = Some g ==>
 ∃s₁ s₂ g c. s = s₂ @ [Check_in g r c] @ s₁ ∧ no_Check_in s₂ r"
apply(induct s)
 apply simp
apply (auto split:event.splits)
apply(rule_tac x = s in exI)
apply(rule_tac x = "[]" in exI)
apply simp
apply(rule_tac x = s₁ in exI)
apply simp
apply(rule_tac x = s₁ in exI)
apply simp
apply(rule_tac x = s₁ in exI)
apply simp
done

lemma no_Check_in_owns[simp]: "no_Check_in s r ==> owns s r = None"
by (induct s) (auto split:event.split)

theorem Enter_safe:
 "[ hotel(Enter g r c # s); safe₀ s r ] ==> owns s r = Some g"
apply(subgoal_tac "∃s₁ s₂ g c. s = s₂ @ [Check_in g r c] @ s₁ ∧ no_Check_in s₂ r")
 prefer 2
 apply(simp add:safe₀_def)
 apply(elim exE conjE)
 apply(rule_tac x = s₁ in exI)
 apply (simp)
apply(elim exE conjE)
apply(cases c)
apply(clarsimp)
apply(erule disjE)
apply (simp add:no_checkin_no_newkey)
apply simp
apply(frule only_owner_enter_normal)
apply assumption
apply simp
apply simp
done

lemma safe_future: "safe₀ s r ==> no_Check_in s' r ==> safe₀ (s' @ s) r"
apply(clarsimp simp:safe₀_def)
apply(rule_tac x = s₁ in exI)
apply(rule_tac x = s₂ in exI)
apply simp
done

corollary Enter_safe_future:
 "[ hotel(Enter g r c # s' @ s); safe₀ s r; no_Check_in s' r ]
 ==> owns s r = Some g"
apply(drule (1) safe_future)
apply(drule (1) Enter_safe)
apply simp
done
(*>*)

text_raw‹
 \begin{figure}
 \begin{center}\begin{minipage}{\textwidth}
 \isastyle\isamarkuptrue
 ›
theorem safe: assumes "hotel s" and "safe s r" and "g ∈ isin s r"
                    shows "owns s r = ⌊g⌋"
proof -
  { fix s₁ s₂ s₃ g' k k'
    let ?b = "[Enter g' r (k,k')] @ s₂ @ [Check_in g' r (k,k')] @ s₁"
    let ?s = "s₃ @ ?b"
    assume 0: "isin (s₂ @ [Check_in g' r (k,k')] @ s₁) r = {}"
    have "[ hotel ?s; no_Check_in (s₃ @ s₂) r; g ∈ isin ?s r ] ==> g' = g"
    proof(induct s₃)
      case Nil thus ?case using 0 by simp
    next
      case (Cons e s₃)
      let ?s = "s₃ @ ?b" and ?t = "(e ⋅ s₃) @ ?b"
      show ?case
      proof(cases e)
        case [simp]: (Enter g'' r' c)
        show "g' = g"
        proof cases
          assume [simp]: "r' = r"
          show "g' = g"
          proof cases
            assume [simp]: "g'' = g"
            have 1: "hotel ?s" and 2: "c ∈ cards ?s g" using ‹hotel ?t› by auto
            have 3: "safe ?s r" using ‹no_Check_in ((e ⋅ s₃) @ s₂) r› 0
              by(simp add:safe_def) blast
            obtain k₁ k₂ where [simp]: "c = (k₁,k₂)" by force
            have "roomk ?s r = k'"
              using safe_roomk_currk[OF 1 safe_safe[OF 3]]
                ‹no_Check_in ((e ⋅ s₃) @ s₂) r› by auto
            hence "k₁ ≠ roomk ?s r"
              using no_checkin_no_newkey[where s₂ = "s₃ @ [Enter g' r (k,k')] @ s₂"]
                1 2 ‹no_Check_in ((e ⋅ s₃) @ s₂) r› by auto
            hence "k₂ = roomk ?s r" using ‹hotel ?t› by auto
            with only_owner_enter_normal[OF 1 safe_safe[OF 3]] 2
            have "owns ?t r = ⌊g⌋" by auto
            moreover have "owns ?t r = ⌊g'⌋"
              using ‹hotel ?t› ‹no_Check_in ((e ⋅ s₃) @ s₂) r› by simp
            ultimately show "g' = g" by simp
          next
            assume "g'' ≠ g" thus "g' = g" using Cons by auto
          qed
        next
          assume "r' ≠ r" thus "g' = g" using Cons by auto
        qed
      qed (insert Cons, auto)
    qed
  } with assms show "owns s r = ⌊g⌋" by(auto simp:safe_def)
qed
text_raw‹
 \end{minipage}
 \end{center}
 \caption{Isar proof of Theorem~\ref{safe}}\label{fig:proof}
 \end{figure}
 ›
text‹
 subsection{Verifying safety}

 ~\ref{state-lemmas} largely carries over after replacing
 mbox{@{prop"s : reach"}} by @{prop"hotel s"} and @{const safe} by
 {const safe₀}. Only properties \ref{currk_inj} and
 ref{key1_not_currk} no longer hold because we no longer assume that
 {const roomk} is initially injective.
  are replaced by two somewhat similar properties:
 begin{lemma}\label{trace-lemmas}\mbox{}
 begin{enumerate}
 item @{thm[display,margin=80]currk_Check_in}
 item \label{no_checkin_no_newkey}
 @{thm[display,margin=100] no_checkin_no_newkey}
 end{enumerate}
 end{lemma}
  are proved by induction on ‹s₂›.
  addition we need some easy structural properties:
 begin{lemma}\label{app-lemmas}
 begin{enumerate}
 item @{thm issued_app}
 item @{thm owns_app}
 item \label{currk_app} @{thm currk_app}
 end{enumerate}
 end{lemma}

  main theorem again correspond closely to its state based
 :
 begin{theorem}\label{safe}
 {thm[mode=IfThen] safe}
 end{theorem}
  us examine the proof of this theorem to show how it differs from
  state based version. For the core of the proof let
 {prop"s = s₃ @ [Enter g' r (k,k')] @ s₂ @ [Check_in g' r (k,k')] @ s₁"}
  assume
 {prop"isin (s₂ @ [Check_in g' r (k,k')] @ s₁) r = {}"} (0). By induction on
 ‹s₃› we prove
 {prop[display]"[hotel s; no_Check_in (s₃ @ s₂) r; g ∈ isin s r ] ==> g' = g"}
  actual theorem follows by definition of @{const safe}.
  base case of the induction follows from (0). For the induction step let
 {prop"t = (e#s₃) @ [Enter g' r (k,k')] @ s₂ @ [Check_in g' r (k,k')] @ s₁"}.
  assume @{prop"hotel t"}, @{prop"no_Check_in ((e#s₃) @ s₂) r"},
  @{prop"g ∈ isin s r"}, and show @{prop"g' = g"}.
  proof is by case distinction on the event ‹e›.
  cases @{const Check_in} and @{const Exit} follow directly from the
  hypothesis because the set of occupants of ‹r›
  only decrease. Now we focus on the case @{prop"e = Enter g'' r' c"}.
  @{prop"r' ≠ r"} the set of occupants of ‹r› remains unchanged
  the claim follow directly from the induction hypothesis.
  @{prop"g'' ≠ g"} then ‹g› must already have been in ‹r›
  the ‹Enter› event and the claim again follows directly
  the induction hypothesis. Now assume @{prop"r' = r"}
  @{prop"g'' = g"}.
  @{prop"hotel t"} we obtain @{prop"hotel s"} (1) and
 {prop"c ∈ cards s g"} (2), and
  @{prop"no_Check_in (s₃ @ s₂) r"} and (0)
  obtain @{prop"safe s r"} (3). Let @{prop"c = (k₁,k₂)"}.
  Lemma~\ref{state-lemmas}.\ref{safe_roomk_currk} and
 ~\ref{app-lemmas}.\ref{currk_app} we obtain
 ‹roomk s r = currk s r = k'›.
  @{prop"k₁ ≠ roomk s r"} by
 ~\ref{trace-lemmas}.\ref{no_checkin_no_newkey}
  (1), (2) and @{prop"no_Check_in (s₃ @ s₂) r"}.
  @{prop"k₂ = roomk s r"} by @{prop"hotel t"}.
  Lemma~\ref{state-lemmas}.\ref{safe_only_owner_enter_normal}
  (1--3) we obtain
 {prop"owns t r = ⌊g⌋"}. At the same time we have @{prop"owns t r = ⌊g'⌋"}
  @{prop"hotel t"} and @{prop"no_Check_in ((e # s₃) @ s₂) r"}: nobody
  checked in to room ‹r› after ‹g'›. Thus the claim
 {prop"g' = g"} follows.

  details of this proof differ from those of Theorem~\ref{safe-state}
  the structure is very similar.

 subsection{Eliminating \isa{isin}}

  the state based approach we needed @{const isin} to express our
  guarantees. In the presence of traces, we can do away with it
  talk about @{const Enter} events instead. We show that if somebody
  a safe room, he is the owner:
 begin{theorem}\label{Enter_safe}
 {thm[mode=IfThen] Enter_safe}
 end{theorem}
  @{prop"safe₀ s r"} it follows that ‹s› must be of the form
 {term"s₂ @ [Check_in g₀ r c'] @ s₁"} such that @{prop"no_Check_in s₂ r"}.
  @{prop"c = (x,y)"} and @{prop"c' = (k,k')"}.
  Lemma~\ref{state-lemmas}.\ref{safe_roomk_currk} we have
 ‹roomk s r = currk s r = k'›.
  @{prop"hotel(Enter g r c # s)"} it follows that
 {prop"(x,y) ∈ cards s g"} and @{prop"k' ∈ {x,y}"}.
  Lemma~\ref{trace-lemmas}.\ref{no_checkin_no_newkey}
 {prop"x = k'"} would contradict @{prop"(x,y) ∈ cards s g"}.
  @{prop"y = k'"}.
  Lemma~\ref{state-lemmas}.\ref{safe_only_owner_enter_normal}
  obtain @{prop"owns s r = ⌊g⌋"}.

  dispensed with @{const isin} we could also eliminate @{const
 } to arrive at a model closer to the ones in~cite‹"Jackson06"›.

  one may quibble that all the safety theorems proved so far
  safety of the room at that point in time when somebody enters
 . That is, the owner of the room must be sure that once a room is
 , it stays safe, in order to profit from those safety theorems.
  course, this is the case as long as nobody else checks in to that room:
 begin{lemma}
 {thm[mode=IfThen]safe_future}
 end{lemma}
  follows easily that Theorem~\ref{Enter_safe} also extends until check-in:
 begin{corollary}
 {thm[mode=IfThen]Enter_safe_future}
 end{corollary}

 subsection{Completeness of @{const safe}}

  proved correctness of @{const safe}, i.e.\ that safe behaviour
  against intruders, one may wonder if @{const safe} is
 , i.e.\ if it covers all safe behaviour, or if it is too
 . It turns out that @{const safe} is incomplete for two
  reasons. The trivial one is that in case @{const initk} is
 , every room is protected against intruders right from the
 . That is, @{term"[Check_in g r c]"} will only allow @{term g} to
  ‹r› until somebody else checks in to ‹r›. The
 , more subtle incompleteness is that even if there are previous
  of a room, it may be safe to enter a room with an old card
 ‹c›: one merely needs to make sure that no other guest checked
  after the check-in where one obtained ‹c›. However,
  this is not only messy, it is also somewhat pointless:
  liberalization is not something a guest can take advantage of
  there is no (direct) way he can find out which of his cards
  this criterion. But without this knowledge, the only safe thing
  do is to make sure he has used his latest card. This incompleteness
  to the state based model as well.
 ›

(*<*)
end
(*>*)