conference.spec 394 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
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) ∧ O(x,p,r)) → Review += (x,p,r)
loop {
	forall x:A,y:A,p:P,r:R (Assign(x,p) ∧ Review(y,p,r)) → Read += (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(xt:A,p:P)

Target

Read(xt:A, pt:P, rt:R)