--- a/Paper.thy	Fri Apr 12 10:46:43 2013 +0100
+++ b/Paper.thy	Fri Apr 12 18:07:03 2013 +0100
@@ -1326,20 +1326,6 @@
   Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/rc/}.\\[-12mm]
 
 
-%  0. Not Policy-Analysis: cause even policy is analysed correct, there is still a gap between it and policy application to the real Access Control system. Hence here Our dynamic model is bridging this gap.  Policy-Analysis "basic" based on "Information flow", but it is not enough: the static "write" right to a certain typed file do not mean a process having this right definitely can write the file, it has to pass a "particular" "Control Flow" to achieve the state of "There are this typed file and this righted process"! 
-%  1. Both Dynamic and Statical analysis, and proved link between two \\
-%  2. Tainting Relation Formalisation  \\
-%  3. Formalisation and Verification than Model Checking  \\
-%  4. Universal Checker of Policy  \\
-%  5. source of RC rules made more precise \\
-%  6. RC example of Webserver with CGIs (key notion: Program Based Roles)  \\
-%  7. RBAC is more Policy-lever(with HUGE companies, many stablised num of roles but frequently varifying num of users); RC is more Program Base Roles, set for system with a lot of program based default value, once pre-setted, it will remains after running. which is key to policy checker.
-
-%The distinct feature of RC is to deal with program based roles, such as server behaviour. 
-%This is in contrast to usual RSBAC models where roles are modeled around a hierachy, for
-%example in a company. 
-
-
 %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. 
@@ -1361,24 +1347,10 @@
 %trace of system running. 
 % 2. decidable, that means this policy-checker should always terminate.
 
-
-%   The purpose of an operating system is to provide a common
-%  interface for accessing resources. This interface is typically 
-%  realised as a collection of system calls, for example for reading 
-%  and writing files, forking of processes, or sending and receiving 
-%  messages. Role based access control is one approach for 
-%  restricting access to such system calls: if a user has
-%  suffient rights, then a system call can be performed. 
+*}
 
-%  a user might have
-%  one or more roles and acces is granted if the role has sufficent
-%  rights
 
-%  static world...make predictions about accessing
-%  files, do they translate into actual systems behaviour.
 
-  
-*}
 
 
 (*<*)