--- a/Paper.thy	Fri Sep 20 12:14:39 2013 +0100
+++ b/Paper.thy	Fri Sep 20 12:22:04 2013 +0100
@@ -309,29 +309,29 @@
   We improve upon their results by using our sound and complete 
   static policy check to make this feasible. 
 
-  Our work is also closely related to the work on \emph{grsecurity}, an 
+  The  work we report is also closely related to the work on \emph{grsecurity}, an 
   access control system developed as a patch on top of Linux kernel \cite{gran12}. 
   It installs a reference monitor to restrict access to system resources.
   They model a dynamic semantics of the operating system with four rules dealing with
   executing a file, setting a role and setting an UID as well as GID.
-  These rules depend on an arbitrary but fixed access policy.
+  These rules are parametrerised by an arbitrary but fixed access policy.
   Although, there are only four rules, their state-space is in general
-  infinite, like in our work. They then give an abstracted semantics,
+  infinite, like in our work. They therfore give an abstracted semantics,
   which gives them a finite state-space. For example the abstracted 
   semantics dispenses with users and roles by introducing
   abstract users and abstract roles. They obtain a soundness result
   for their abstract semantics and under some weak assumptions
-  also a completeness result. Comparing it to our work, we will have a much
+  also a completeness result. Comparing this to our work, we will have a much
   more fine-grained model of the underlying operating system. We will
   also obtain a soundness result, but more importantly obtain 
   also a completeness result. But since we have a much more fine-grained
-  model it will depend on some stronger assumptions.  The abstract semantics
+  model, it will depend on some stronger assumptions.  The abstract semantics
   in \cite{gran12} is used for model-checking policies according to
   whether, for example, information flow properties are ensured. 
-  Since there formalism consists of only a few rules, they can get away with
-  `pencil-and-paper proofs', whereas reasoning about our more detailed 
-  model containing substantially more rules needs the support of
-  a theorem prover.
+  Since their formalism consists of only a few rules, they can get away with
+  ``pencil-and-paper proofs'', whereas reasoning about our more detailed 
+  model containing substantially more rules really necessitates the support of
+  a theorem prover and completely formalised models.
 
   Our formal models and correctness proofs are mechanised in the
   interactive theorem prover Isabelle/HOL. The mechanisation of the models is a
@@ -1392,16 +1392,18 @@
   reasoning about sequences of events \cite{Paulson98}.
   We have approximately 1000 lines of code for definitions and 6000 lines of
   code for proofs. Our formalisation is available from the
-  Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/rc/}.\\[-12mm]
+  Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/rc/}.\\[-12mm]\mbox{}
 
-
+%%\\[-12mm]
+%
+%
 %In a word, what the manager need is that given the
 %initial state of the system, a policy checker that make sure the under the policy
 %he made, this important file cannot: 1. be deleted; 2. be tainted. 
 %Formally speaking, this policy-checker @{text "PC"} (a function that given the 
 %initial state of system, a policy and an object, it tells whether this object 
 %will be fully protected or not) should satisfy this criteria: 
-
+%
 %  @{text "(PC init policy obj) \<and> (exists init obj) \<longrightarrow> \<not> taintable obj"}
 %If the @{text obj} exists in the initial-state, and @{text "PC"} justify the safety
 %of this object under @{text "policy"}, this object should not be @{text taintable}.
@@ -1409,26 +1411,19 @@
 %And there is the \emph{soundness} criteria of @{text "PC"} too, otherwise a "NO-to-ALL"
 %answer always satisfy the \emph{completeness}. \emph{soundness} formally is:
 %  @{text "PC init policy obj \<longrightarrow> taintable obj"}
-
+%
 %This policy-checker should satisfy other properties:
 % 1. fully statical, that means this policy-checker should not rely on the system 
 %running information, like new created files/process, and most importantly the 
 %trace of system running. 
 % 2. decidable, that means this policy-checker should always terminate.
-
+%
 *}
-
-
-
-
-
 (*<*)
 end
 
 end
 (*>*)
-
-
 (*
 
   Central to RC-Model is the roles and types. We start with do formalisation on
@@ -1488,7 +1483,6 @@
   @{term "type_of_ipc"} are alrealdy efficient types. 
 
 *)
-
 (*
 
 text {*