final_theorems.thy
author chunhan
Thu, 13 Jun 2013 22:53:49 +0800
changeset 9 91fb17bb6229
parent 1 dcde836219bc
permissions -rw-r--r--
add paper pdf
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1
dcde836219bc add thy files
chunhan
parents:
diff changeset
     1
theory final_theorems
dcde836219bc add thy files
chunhan
parents:
diff changeset
     2
imports Main rc_theory del_vs_del_s tainted_vs_tainted_s
dcde836219bc add thy files
chunhan
parents:
diff changeset
     3
begin
dcde836219bc add thy files
chunhan
parents:
diff changeset
     4
dcde836219bc add thy files
chunhan
parents:
diff changeset
     5
context tainting_s_complete begin
dcde836219bc add thy files
chunhan
parents:
diff changeset
     6
dcde836219bc add thy files
chunhan
parents:
diff changeset
     7
theorem static_complete: 
dcde836219bc add thy files
chunhan
parents:
diff changeset
     8
  assumes undel: "undeletable obj" and tbl: "taintable obj"
dcde836219bc add thy files
chunhan
parents:
diff changeset
     9
  shows "taintable_s obj"
dcde836219bc add thy files
chunhan
parents:
diff changeset
    10
proof-
dcde836219bc add thy files
chunhan
parents:
diff changeset
    11
  from tbl obtain s where tainted: "obj \<in> tainted s"
dcde836219bc add thy files
chunhan
parents:
diff changeset
    12
    by (auto simp:taintable_def)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    13
  hence vs: "valid s" by (simp add:tainted_is_valid)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    14
  from undel vs have "\<not> deleted obj s" and "exists [] obj" 
dcde836219bc add thy files
chunhan
parents:
diff changeset
    15
    by (auto simp:undeletable_def)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    16
  moreover from tainted have "valid s" by (rule tainted_is_valid)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    17
  ultimately have "source_of_sobj (obj2sobj s obj) = Some obj" 
dcde836219bc add thy files
chunhan
parents:
diff changeset
    18
    using init_obj_keeps_source by auto
dcde836219bc add thy files
chunhan
parents:
diff changeset
    19
  with tainted t2ts 
dcde836219bc add thy files
chunhan
parents:
diff changeset
    20
  show ?thesis unfolding taintable_s_def
dcde836219bc add thy files
chunhan
parents:
diff changeset
    21
    by (rule_tac x = "obj2sobj s obj" in exI, simp)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    22
qed
dcde836219bc add thy files
chunhan
parents:
diff changeset
    23
dcde836219bc add thy files
chunhan
parents:
diff changeset
    24
theorem undeletable_s_complete:
dcde836219bc add thy files
chunhan
parents:
diff changeset
    25
  "undeletable_s obj \<Longrightarrow> undeletable obj"
dcde836219bc add thy files
chunhan
parents:
diff changeset
    26
apply (clarsimp simp:undeletable_s_def undeletable_def)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    27
apply (drule deleted_imp_deletable_s, simp+)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    28
done
dcde836219bc add thy files
chunhan
parents:
diff changeset
    29
dcde836219bc add thy files
chunhan
parents:
diff changeset
    30
theorem final_offer:
dcde836219bc add thy files
chunhan
parents:
diff changeset
    31
  "\<lbrakk>undeletable_s obj; \<not> taintable_s obj; exists [] obj\<rbrakk> \<Longrightarrow> \<not> taintable obj"
dcde836219bc add thy files
chunhan
parents:
diff changeset
    32
apply (erule swap)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    33
by (simp add:static_complete undeletable_s_complete)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    34
dcde836219bc add thy files
chunhan
parents:
diff changeset
    35
end
dcde836219bc add thy files
chunhan
parents:
diff changeset
    36
dcde836219bc add thy files
chunhan
parents:
diff changeset
    37
context tainting_s_sound begin
dcde836219bc add thy files
chunhan
parents:
diff changeset
    38
dcde836219bc add thy files
chunhan
parents:
diff changeset
    39
theorem static_sound:
dcde836219bc add thy files
chunhan
parents:
diff changeset
    40
  assumes tbl_s: "taintable_s obj"
dcde836219bc add thy files
chunhan
parents:
diff changeset
    41
  shows "taintable obj"
dcde836219bc add thy files
chunhan
parents:
diff changeset
    42
proof-
dcde836219bc add thy files
chunhan
parents:
diff changeset
    43
  from tbl_s obtain sobj where ts: "sobj \<in> tainted_s"
dcde836219bc add thy files
chunhan
parents:
diff changeset
    44
    and sreq: "source_of_sobj sobj = Some obj" 
dcde836219bc add thy files
chunhan
parents:
diff changeset
    45
    by (auto simp:taintable_s_def)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    46
  from ts obtain obj' \<tau> where t: "obj' \<in> tainted \<tau>" 
dcde836219bc add thy files
chunhan
parents:
diff changeset
    47
    and vs: "valid \<tau>" and sreq': "sobj_source_eq_obj sobj obj'"
dcde836219bc add thy files
chunhan
parents:
diff changeset
    48
    by (auto dest!:tainted_s2tainted dest:tainted_is_valid)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    49
  from sreq' sreq have "obj = obj'" by (simp add:source_eq)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    50
  with vs t 
dcde836219bc add thy files
chunhan
parents:
diff changeset
    51
  show ?thesis by (auto simp:taintable_def)
dcde836219bc add thy files
chunhan
parents:
diff changeset
    52
qed
dcde836219bc add thy files
chunhan
parents:
diff changeset
    53
dcde836219bc add thy files
chunhan
parents:
diff changeset
    54
end
dcde836219bc add thy files
chunhan
parents:
diff changeset
    55
dcde836219bc add thy files
chunhan
parents:
diff changeset
    56
end