Commit 3a5a755f authored by Christian Müller's avatar Christian Müller

examples

parent 301bbee4
......@@ -5,19 +5,19 @@ forallmay x:A,p:P
forallmay x:A,p:P
!Conf(x,p) → Assign += (x,p)
forall x:A,p:P,r:R
(Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
(Assign(x,p) ∧ Oracle(x,p,r)) → Review += (x,p,r)
loop {
forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,xb,p,r)
forallmay x:A,p:P,r:R (Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
}
Declassify
O(x:A,p:P,r:R): ¬ Conf(xa:A,p:P)
Oracle(x:A,p:P,r:R): ¬ Conf(xat:A,p:P)
Target
Read(xa:A, xb:A, p:P, r:R)
Read(xat:A, xbt:A, pt:P, rt:R)
Causality
......
Workflow
forallmay x:A,p:P
True → Conf += (x,p)
forallmay x:A,p:P
!Conf(x,p) → Assign += (x,p)
forall x:A,p:P,r:R
(Assign(x,p) ∧ Oracle(x,p,r)) → Review += (x,p,r)
loop {
forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,xb,p,r)
forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
}
Target
Read(xat:A, xbt:A, pt:P, rt:R)
Causality
a:A
Workflow
forall x,s
O(x,s) -> R += (x)
Declassify
O(x,s): True
Target
R(xt)
Workflow
forallmay x,s
O(s) -> R += (x)
forall x,s
O(x,s) -> R += (x)
Target
......
Workflow
forall x,s
O(x,s) -> R += (x,s)
Target
R(x,s)
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment