theory ExampleSystemPolicyFlows

lemma Sys3UT3Reads_correct_bw : "x \<in> Sys3Reads \<Longrightarrow> x \<in> subjectReads Sys3AuthGraph (OrdinaryLabel (UT3))" apply (simp add: Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3Reads_def) apply (erule disjE) 
   (* UT3 reads UT3 *)
    apply simp 
  (* UT3 reads EP3 *)
   apply (erule disjE) apply (rule_tac auth = SyncSend in reads_ep) apply (simp) apply (simp add:insertI1) 
  (* UT3 reads T3 *)
   apply (rule_tac ep = "OrdinaryLabel (EP3)" in read_sync_ep_read_receivers) apply (rule_tac auth = SyncSend in reads_ep) apply (simp) apply (rule insertI1) apply (simp add: insertI1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> Sys3Reads \<Longrightarrow> x \<in> subjectReads Sys3AuthGraph (OrdinaryLabel UT3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel UT3 \<or> x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel UT3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3)
 2. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel UT3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3)
 2. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel EP3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3)
 2. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3) proof (prove)
goal (3 subgoals):
 1. x = OrdinaryLabel EP3 \<Longrightarrow> (OrdinaryLabel UT3, SyncSend, x) \<in> insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))
 2. x = OrdinaryLabel EP3 \<Longrightarrow> SyncSend \<in> {SyncSend, Receive}
 3. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel EP3 \<Longrightarrow> SyncSend \<in> {SyncSend, Receive}
 2. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel T3 \<Longrightarrow> OrdinaryLabel EP3 \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel UT3)
 2. x = OrdinaryLabel T3 \<Longrightarrow> (x, Receive, OrdinaryLabel EP3) \<in> insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3}))) proof (prove)
goal (3 subgoals):
 1. x = OrdinaryLabel T3 \<Longrightarrow> (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) \<in> insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))
 2. x = OrdinaryLabel T3 \<Longrightarrow> SyncSend \<in> {SyncSend, Receive}
 3. x = OrdinaryLabel T3 \<Longrightarrow> (x, Receive, OrdinaryLabel EP3) \<in> insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3}))) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel T3 \<Longrightarrow> SyncSend \<in> {SyncSend, Receive}
 2. x = OrdinaryLabel T3 \<Longrightarrow> (x, Receive, OrdinaryLabel EP3) \<in> insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3}))) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel T3 \<Longrightarrow> (x, Receive, OrdinaryLabel EP3) \<in> insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3}))) proof (prove)
goal:
No subgoals!