--- a/Paper.thy	Thu Jun 13 22:15:32 2013 +0800
+++ b/Paper.thy	Thu Jun 13 22:51:03 2013 +0800
@@ -117,8 +117,8 @@
  "\<lbrakk>p \<in> current_procs \<tau>; u \<in> init_users\<rbrakk> \<Longrightarrow> os_grant \<tau> (ChangeOwner p u)"
 by simp
 
-lemma osgrant10:
-  "\<lbrakk>p \<in> current_procs \<tau>; p' = new_proc \<tau>\<rbrakk> \<Longrightarrow> os_grant \<tau> (Clone p p')"
+lemma osgrant10: (* modified by chunhan *)
+  "\<lbrakk>p \<in> current_procs \<tau>; p' \<notin> current_procs \<tau>\<rbrakk> \<Longrightarrow> os_grant \<tau> (Clone p p')"
 by simp 
 
 
@@ -436,7 +436,7 @@
   file @{text "/usr/bin/make"} is represented by the list @{text
   "[make, bin, usr]"} and the @{text root}-directory is the @{text
   Nil}-list. Following the presentation in \cite{ottrc}, our model of
-  IPCs is rather simple-minded: we only have events for creation and deletion Of IPCs,
+  IPCs is rather simple-minded: we only have events for creation and deletion of IPCs,
   as well as sending and receiving messages.
 
   Events essentially transform one state of the system into
@@ -499,7 +499,7 @@
   processes is unchanged. We have similar functions for alive files and 
   IPCs, called @{term "current_files"} and @{term "current_ipcs"}. 
 
-  We can use these function in order to formally model which events are
+  We can use these functions in order to formally model which events are
   \emph{admissible} by the operating system in each state. We show just three 
   rules that give the gist of this definition. First the rule for changing 
   an owner of a process:
@@ -537,6 +537,8 @@
   ID generated by the function @{term new_proc}. This process ID should
   not already exist. Therefore we define @{term new_proc} as
 
+  (* HERE ????? chunhan *)
+
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
   @{term "new_proc s"} & @{text "\<equiv>"} & @{term "Max (current_procs s) + 1"}
@@ -570,7 +572,7 @@
   set of @{text r}. 
 
   The complication in the RC-Model arises from the
-  way how the current role of a process in a state @{text s} is
+  way the current role of a process in a state @{text s} is
   calculated---represented by the predicate @{term is_current_role} in our formalisation.  
   For defining this predicate we need to trace the role of a process from
   the initial state to the current state. In the
@@ -622,7 +624,7 @@
 
   \noindent
   We check whether @{term pf} is the parent file (directory) of @{text f} and check
-  whether the type of @{term pf} is @{term t}. We also need to fetch the 
+  whether the type of @{term pf} is @{term t}. We also need to fetch 
   the role @{text r} of the process that seeks to get permission for creating 
   the file. If the default type of this role @{text r} states that the 
   type of the newly created file will be inherited from the parent file
@@ -781,7 +783,7 @@
   hope for a meaningful check by just trying out all possible
   valid states in our dynamic model. The reason is that there are
   potentially infinitely many of them and therefore the search space would be
-  infinite.  For example staring from an
+  infinite.  For example starting from an
   initial state containing a process @{text p} and a file @{text pf}, 
   we can create files @{text "f\<^isub>1"}, @{text "f\<^isub>2"}, @{text "..."} 
   via @{text "CreateFile"}-events. This can be pictured roughly as follows:
@@ -944,7 +946,7 @@
   with this setup of recording the precise information for the initial
   state is where two processes have the same role and type
   information, but only one is tainted in the initial state, but the
-  other is not. The recorded unique process IDs allows us to
+  other is not. The recorded unique process ID allows us to
   distinguish between both processes.  For all newly created objects,
   on the other hand, we do not care.  This is crucial, because
   otherwise exploring all possible ``reachable'' objects can lead to
@@ -1122,7 +1124,7 @@
   \noindent
   The function @{text "\<lbrakk>_\<rbrakk>"} extracts the static information from an object.
   For example for a process it extracts the role, default role, type and
-  user; for a file the type and the anchor. If a process in tainted and creates
+  user; for a file the type and the anchor. If a process is tainted and creates
   a file with a normal type @{text "t'"} then also the created file
   is tainted. The corresponding rule is
 
@@ -1249,7 +1251,7 @@
   want to know whether a virus-infected file introduced by a user can
   affect the core system files. Our test allows the system
   administrator to find this out provided the RC-policy makes the core
-  system files undeletable. We assume that this provisio is already part 
+  system files undeletable. We assume that this proviso is already part 
   of best practice rule for running a system.
 
   We envisage our test to be useful in two kind of situations: First, if
@@ -1359,6 +1361,7 @@
 end
 (*>*)
 
+
 (*
 
   Central to RC-Model is the roles and types. We start with do formalisation on
@@ -1417,7 +1420,9 @@
   processes and IPCs, all types that calculated by @{term "type_of_process"} and 
   @{term "type_of_ipc"} are alrealdy efficient types. 
 
-*}
+*)
+
+(*
 
 text {*
   \begin{isabelle}\ \ \ \ \ %%%
@@ -1486,4 +1491,6 @@
   determinated by the efficient forced role of the executable file
   @{term "forcedrole"}.  When new process is created, this process'
   role is assigned to its creator's role.
+
+*}
 *)
\ No newline at end of file