conference_linear_small.spec 287 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
Workflow

forallmay x:X,p:P
	True -> Conf += (x,p)
forall x:X,p:P,r:R
	(¬ Conf(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
forallmay y:X,x:X,p:P
	(¬ Conf(x,p) ∧ ¬ Conf(y,p)) -> Comm += (x,y,p)

Declassify

O(x:X,p:P,r:R): ¬ Conf(xt:X,p:P)

Target

Comm(xt:X, yt:X, pt:P)

Causality

a:X