conference_unrolled_withB.spec 557 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
Workflow

forallmay x:A,p:P
	True → Conf += (x,p)
forallmay x:A,p:P
	B(x,p) → Assign += (x,p)
forall x:A,p:P,r:R
	(Assign(x,p) ∧ Oracle(x,p,r)) → Review += (x,p,r)
forall xa:A,xb:A,p:P,r:R 
	(Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,p,r)
forallmay x:A,p:P,r:R 
	(Assign(x,p)) → Review += (x,p,r)
forall xa:A,xb:A,p:P,r:R 
	(Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,p,r)
forallmay x:A,p:P,r:R 
	(Assign(x,p)) → Review += (x,p,r)

Declassify

Oracle(x:A,p:P,r:R): ¬ Conf(xat:A,p:P)

Target

Read(xat:A, p:P, rt:R)

Causality

a:A