Quelle  State.thy

(*  Title:      A state based hotel key card system

    Author:     Tobias Nipkow, TU Muenchen
*)

(*<*)
theory State
imports Basis
begin

declare if_split_asm[split]
(*>*)

section‹A state based model›

text‹The model is based on three opaque types @{typ guest},
 {typ key} and @{typ room}. Type @{typ card} is just an abbreviation
  @{typ"key × key"}.

  state of the system is modelled as a record which combines the
  about the front desk, the rooms and the guests.
 ›

record state =
 owns :: "room ==> guest option"
 currk :: "room ==> key"
 issued :: "key set"
 cards :: "guest ==> card set"
 roomk :: "room ==> key"
 isin :: "room ==> guest set"
 safe :: "room ==> bool"

text‹\noindent Reception records who @{const owns} a room (if anybody, hence
 {typ"guest option"}), the current key @{const currk} that has been
  for a room, and which keys have been @{const issued} so
 . Each guest has a set of @{const cards}. Each room has a key
 {const roomk} recorded in the lock and a set @{const isin} of
 . The auxiliary variable @{const safe} is explained further
 ; we ignore it for now.

  specification languages like Z, VDM and B we would now define a
  of operations on this state space. Since they are the only
  operations on the state, this defines a set of
 emph{reachable} states. In a purely logical environment like
 /HOL this set can be defined directly by an inductive
 . Each clause of the definition corresponds to a
 /operation/event. This is the standard approach to modelling
  machines in theorem provers.

  set of reachable states of the system (called ‹reach›) is
  by four transitions: initialization, checking in, entering a room,
  leaving a room:›

(*<*)
inductive_set reach :: "state set"
where
(*>*)
init:
"inj initk ==>
\<lparr> owns = (λr. None), currk = initk, issued = range initk,
  cards = (λg. {}), roomk = initk, isin = (λr. {}),
  safe = (λr. True) ) ∈ reach"

| check_in:
"[ s ∈ reach; k ∉ issued s ] ==>
s( currk := (currk s)(r := k), issued := issued s ∪ {k},
   cards := (cards s)(g := cards s g ∪ {(currk s r, k)}),
   owns := (owns s)(r := Some g),
   safe := (safe s)(r := False) ) ∈ reach"

| enter_room:
"[ s ∈ reach; (k,k') ∈ cards s g; roomk s r ∈ {k,k'} ] ==>
s( isin := (isin s)(r := isin s r ∪ {g}),
   roomk := (roomk s)(r := k'),
   safe := (safe s)(r := owns s r = ⌊g⌋ ∧ isin s r = {} ∧ k' = currk s r
                              ∨ safe s r)
  ) ∈ reach"

| exit_room:
"[ s ∈ reach; g ∈ isin s r ] ==>
s( isin := (isin s)(r := isin s r - {g}) ) ∈ reach"

text‹\bigskip There is no check-out event because it is implicit in the next
 -in for that room: this covers the cases where a guest leaves without checking out (in which case the room should not be blocked forever) or where
  hotel decides to rent out a room prematurely, probably by accident.
  do guests have to return their cards at any point because they may
  cards or may pretended to have lost them.
  will now explain the events.
 begin{description}
 item[‹init›]
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
  @{const currk} is injective. Nobody
  a room, the keys of all rooms are recorded as issued, nobody has
  card, and all rooms are empty.
 item[@{thm[source] enter_room}]
  guest may enter if either of the two keys on his card equal the room key.
  ‹g› is added to the occupants of ‹r› and
  room key is set to the second key on the card.
  this has no effect because the second key is already the room key.
  when entering for the first time, the first key on the card equals
  room key and then the lock is actually recoded.
 item[‹exit_room›]
  an occupant from the occupants of a room.
 item[‹check_in›] for room ‹r› and guest ‹g›
  the card @{term"(currk s r, k)"}
  ‹g›, where ‹k› is new, makes ‹g› the owner of the room,
  sets @{term"currk s r"} to the new key ‹k›.
 end{description}

  reader can easily check that our specification allows the intended
  implementation: entering only reads and writes the key in
  lock, and check-in only reads and writes the information at
 .

  contrast to Jackson we require that initially distinct rooms have
  keys. This protects the hotel from its guests: otherwise a
  may be able to enter rooms he does not own, potentially stealing
  from those rooms. Of course he can also steal objects from his
  room, but in that case it is easier to hold him responsible. In
 , the hotel may just want to minimize the opportunity for
 .

  main difference to Jackson's model is that his can talk about
  between states rather than merely about reachable
 . This means that he can specify that unauthorized entry into a
  should not occur. Because our specification does not formalize
  transition relation itself, we need to include the ‹isin›
  in order to
  the same requirement. In the end, we would like to establish
  the system is \emph{safe}: only the owner of a room can be in a
 :
 begin{center}
 {prop"s ∈ reach ==> g ∈ isin s r ==> owns s r = Some g"}
 end{center}
 , this is just not true. It does not take a PhD in
  science to come up with the following scenario: because
  can retain their cards, there is nothing to stop a guest from
  his old room after he has checked out (in our model: after
  next guest has checked in), but before the next guest has entered
  room. Hence the best we can do is to prove a conditional safety
 : under certain conditions, the above safety property
 . The question is: which conditions? It is clear that the room
  be empty when its owner enters it, or all bets
  off. But is that sufficient? Unfortunately not. Jackson's Alloy tool
  2 seconds~cite‹‹p.~303› in "Jackson06"›
  find the following ``guest-in-the-middle'' attack:

 begin{enumerate}

 item Guest 1 checks in and obtains a card $(k_1,k_2)$ for room 1 (whose key
  the lock is $k_1$). Guest 1 does not enter room 1.

 item Guest 2 checks in, obtains a card $(k_2,k_3)$ for room 1, but
  not enter room 1 either.

 item Guest 1 checks in again, obtains a card $(k_3,k_4)$, goes to
  1, opens it with his old card $(k_1,k_2)$, finds the room empty,
  feels safe \ldots

 end{enumerate}
  Guest~1 has left his room, Guest~2 enters and makes off with the
 .

  now assumes that guests return their cards upon
 -out, which can be modelled as follows: upon check-in, the new card
  not added to the guest's set of cards but it replaces his previous
  of cards, i.e.\ guests return old cards the next time they check
 . Under this assumption, Alloy finds no more counterexamples to
  --- at least not up to 6 cards and keys and 3 guests and
 . This is not a proof but a strong indication that the given
  suffice for safety. We prove that this is indeed the case.

  should be noted that the system also suffers from a liveness
 : if a guest never enters the room he checked in to, that room
  forever blocked. In practice this is dealt with by a master key. We
  liveness.

 subsection{Formalizing safety}
 label{sec:formalizing-safety}

  should be clear that one cannot force guests to always return their
  (or, equivalently, never to use an old card). We can only prove that if
  do, their room is safe. However, we do not follow Jackson's
  of globally assuming everybody returns their old cards upon
 -in. Instead we would like to take a local approach where it is up
  each guest whether he follows this safety policy. We allow
  to keep their cards but make safety dependent on how they use
 . This generality requires a finer grained model: we need to
  if a guest has entered his room in a safe manner,
 .e.\ if it was empty and if he used the latest key for the room, the
  stored at reception.
  auxiliary variable @{const safe} records for each room if this
  the case at some point between his last check-in and now.
  main theorem will be that if a room is safe in this
 , then only the owner can be in the room.
  we explain how @{const safe} is modified with each event:

 begin{description}
 item[‹init›] sets @{const safe} to @{const True} for every room.
 item[‹check_in›] for room ‹r› resets @{prop"safe s r"}
  it is not safe for the new owner yet.
 item[@{thm[source] enter_room}] for room ‹r› sets @{prop"safe s r"} if
  owner entered an empty room using the latest card issued for that room
  reception, or if the room was already safe.
 item[‹exit_room›] does not modify @{const safe}.
 end{description}

  reader should convince his or herself that @{const safe}
  to the informal safety policy set out above. Note that a
  may find his room non-empty the first time he enters, and
 {const safe} will not be set, but he may come back later, find the
  empty, and then @{const safe} will be set. Furthermore, it is
  that @{thm[source] enter_room} cannot reset @{const safe}
  to the disjunct ‹∨ safe s r›. Hence ‹check_in› is
  only event that can reset @{const safe}. That is, a room stays
  until the next ‹check_in›. Additionally @{const safe} is
  @{const True}, which is fine because initially injectivity
  ‹initk› prohibits illegal entries by non-owners.

  that because none of the other state components depend on @{const
 }, it is truly auxiliary: it can be deleted from the system and
  same set of reachable states is obtained, modulo the absence of
 {const safe}.

  have formalized a very general safety policy of always using the
  card. A special case of this policy is the one called
 emph{NoIntervening} by Jackson~cite‹‹p.~200› in "Jackson06"›: every ‹check_in› must immediately be followed by the corresponding @{thm[source]
 }.
 ›

(*<*)
lemma currk_issued[simp]: "s : reach ==> currk s r : issued s"
by (induct set: reach) auto

lemma key1_issued[simp]: "s : reach ==> (k,k') : cards s g ==> k : issued s"
by (induct set: reach) auto

lemma key2_issued[simp]: "s : reach ==> (k,k') : cards s g ==> k' : issued s"
by (induct set: reach) auto

lemma roomk_issued[simp]: "s : reach ==> roomk s k : issued s"
by (induct set: reach) auto

lemma currk_inj[simp]:
 "s : reach ==> ∀r r'. (currk s r = currk s r') = (r = r')"
by (induct set: reach) (auto simp:inj_on_def)

lemma key1_not_currk[simp]:
 "s : reach ==> (currk s r,k') ∉ cards s g"
by (induct set: reach) auto

lemma guest_key2_disj[simp]: 
 "[ s : reach; (k₁,k) ∈ cards s g₁; (k₂,k) ∈ cards s g₂ ] ==> g₁=g₂"
by (induct set: reach) auto

lemma safe_roomk_currk[simp]:
 "s : reach ==> safe s r ==> roomk s r = currk s r"
by (induct set: reach) auto


lemma safe_only_owner_enter_normal_aux[simp]:
 "[ s : reach; safe s r; (k',roomk s r) ∈ cards s g ] ==> owns s r = Some g"
by (induct set: reach) (auto)

lemma safe_only_owner_enter_normal:
assumes "s : reach"
shows "[ safe s r; (k',roomk s r) ∈ cards s g ] ==> owns s r = Some g"
using assms
proof induct
  case (enter_room s k k1 g1 r1)
  let ?s' = "s(isin := (isin s)(r1 := isin s r1 ∪ {g1}),
               roomk := (roomk s)(r1 := k1),
               safe := (safe s)
                 (r1 :=
                    owns s r1 = Some g1 ∧ isin s r1 = {} ∧ k1 = currk s r1 ∨
                    safe s r1))"
  note s = ‹s ∈ reach›
  and IH = ‹[ safe s r; (k', roomk s r) ∈ cards s g ] ==> owns s r = Some g›
  and card_g1 = ‹(k,k1) ∈ cards s g1› and safe = ‹safe ?s' r›
  and card_g = ‹(k',roomk ?s' r) ∈ cards ?s' g›
  have "roomk s r1 = k ∨ roomk s r1 = k1" using ‹roomk s r1 ∈ {k,k1}› by simp
  thus ?case
  proof
    assume [symmetric,simp]: "roomk s r1 = k"
    show ?thesis
    proof (cases "r1 = r")
      assume "r1 ≠ r" with IH safe card_g show ?thesis by simp
    next
      assume [simp]: "r1 = r"
      hence safe': "owns s r = Some g1 ∨ safe s r"
        using safe by auto
      thus ?thesis
      proof
        assume "safe s r"
        with s card_g1 have False by simp
        thus ?thesis ..
      next
        assume [simp]: "owns s r = Some g1"
        thus "owns ?s' r = Some g"
          using s card_g card_g1 by simp
      qed
    qed
  next
    assume "roomk s r1 = k1"
    with enter_room show ?case by auto
  qed
qed auto

theorem "s : reach ==> safe s r ==> g : isin s r ==> owns s r = Some g"
by (induct set: reach) auto

theorem safe: assumes "s : reach"
shows "safe s r ==> g : isin s r ==> owns s r = Some g"
using assms
proof induct
  case (enter_room s k1 k2 g1 r1)
  let ?s' = "s(isin := (isin s)(r1 := isin s r1 ∪ {g1}),
               roomk := (roomk s)(r1 := k2),
               safe := (safe s)
                 (r1 :=
                    owns s r1 = Some g1 ∧ isin s r1 = {} ∧ k2 = currk s r1 ∨
                    safe s r1))"
  note s = ‹s ∈ reach›
  and IH = ‹[ safe s r; g ∈ isin s r ] ==> owns s r = Some g›
  and card_g1 = ‹(k1,k2) ∈ cards s g1› and safe = ‹safe ?s' r›
  and isin = ‹g ∈ isin ?s' r›
  show ?case
    proof (cases "r1 = r")
      assume "r1 ≠ r" with IH isin safe show ?thesis by simp
    next
      assume [simp]: "r1 = r"
      have "g ∈ isin s r ∨ g = g1" using isin by auto
      thus ?thesis
      proof
        assume g: "g ∈ isin s r"
        then have "safe s r" using safe by auto
        with g show ?thesis using IH by simp
      next
        assume [simp]: "g = g1"
        have "k2 = roomk s r1 ∨ k1 = roomk s r1"
          using ‹roomk s r1 ∈ {k1,k2}› by auto
        thus ?thesis
        proof
          assume "k2 = roomk s r1"
          with card_g1 s safe show ?thesis
            by auto
      next
        assume [simp]: "k1 = roomk s r1"
        have "owns s r = Some g1 ∨ safe s r" using safe by auto
        thus ?thesis
        proof
          assume "owns s r = Some g1" thus ?thesis by simp
        next
          assume "safe s r"
          hence False using s card_g1 by auto
          thus ?thesis ..
        qed
      qed
    qed
  qed
qed auto
(*>*)

text‹

 subsection{Verifying safety}
 label{sec:verisafe}

  of our lemmas are invariants of @{const reach}.
  complete list, culminating in the main theorem, is this:
 begin{lemma}\label{state-lemmas}
 begin{enumerate}
 item @{thm currk_issued}
 item @{thm key1_issued}
 item @{thm key2_issued}
 item @{thm roomk_issued}
 item \label{currk_inj} @{thm currk_inj}
 item \label{key1_not_currk} @{thm key1_not_currk}
 item @{thm guest_key2_disj}
 item \label{safe_roomk_currk} @{thm[display] safe_roomk_currk}
 item \label{safe_only_owner_enter_normal} @{thm safe_only_owner_enter_normal}
 end{enumerate}
 end{lemma}
 begin{theorem}\label{safe-state}
 {thm[mode=IfThen] safe}
 end{theorem}
  lemmas and the theorem are proved in this order, each one is marked as a
  rule, and each proof is a one-liner: induction on
 {prop"s ∈ reach"} followed by ‹auto›.

 , or maybe even because these proofs work so smoothly one may
  to understand why. Hence we examine the proof of
 ~\ref{safe-state} in more detail. The only interesting case is
 {thm[source] enter_room}. We assume that guest ‹g₁› enters room
 ‹r₁› with card @{term"(k₁,k₂)"} and call the new state ‹t›.
  assume @{prop"safe t r"} and @{prop"g ∈ isin t r"} and prove
 {prop"owns t r = ⌊g⌋"} by case distinction.
  @{prop"r₁ ≠ r"}, the claim follows directly from the induction hypothesis
  \mbox{@{prop"safe s r"}} and @{prop"g ∈ isin t r"}
  @{prop"owns t r = owns s r"} and @{prop"safe t r = safe s r"}.
  @{prop"r₁ = r"} then @{prop"g ∈ isin t r"} is equivalent with
 {prop"g ∈ isin s r ∨ g = g₁"}. If @{prop"g ∈ isin s r"} then
 mbox{@{prop"safe s r"}} follows from @{prop"safe t r"} by
  of @{thm[source]enter_room} because @{prop"g ∈ isin s r"}
  @{prop"isin s r ≠ {}"}. Hence the induction hypothesis implies the
 . If @{prop"g = g₁"} we make another case distinction.
  @{prop"k₂ = roomk s r"}, the claim follows immediately from
 ~\ref{state-lemmas}.\ref{safe_only_owner_enter_normal} above:
  the owner of a room can possess a card where the second
  is the room key.
  @{prop"k₁ = roomk s r"} then, by definition of @{thm[source]enter_room},
 {prop"safe t r"} implies @{prop"owns s r = ⌊g⌋ ∨ safe s r"}.
  the first case the claim is immediate. If @{prop"safe s r"}
  @{prop"roomk s r = currk s r"}
 by Lemma~\ref{state-lemmas}.\ref{safe_roomk_currk})
  thus @{prop"(currk s r, k₂) ∈ cards s g"} by assumption
 {prop"(k₁,k₂) ∈ cards s g₁"}, thus contradicting
 ~\ref{state-lemmas}.\ref{key1_not_currk}.

  detailed proof shows that a number of case distinctions are
 . Luckily, they all suggest themselves to Isabelle via the
  of function update (‹:=›) or via disjunctions that
  automatically.
 ›

(*<*)
end
(*>*)