conference.spec 437 Bytes
Newer Older
1 2
Workflow

Christian Müller's avatar
Christian Müller committed
3
forallmay x:A,p:P
Christian Müller's avatar
Christian Müller committed
4
	True → Conf += (x,p)
Christian Müller's avatar
Christian Müller committed
5
forallmay x:A,p:P
6
	!Conf(x,p) → Assign += (x,p)
Christian Müller's avatar
Christian Müller committed
7
forall x:A,p:P,r:R
Christian Müller's avatar
Christian Müller committed
8
	(Assign(x,p) ∧ Oracle(x,p,r)) → Review += (x,p,r)
Christian Müller's avatar
Christian Müller committed
9
loop {
10
	forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,xb,p,r)
Christian Müller's avatar
Christian Müller committed
11
	forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
Christian Müller's avatar
Christian Müller committed
12 13
}

Christian Müller's avatar
Christian Müller committed
14 15
Declassify

Christian Müller's avatar
Christian Müller committed
16
Oracle(x:A,p:P,r:R): ¬ Conf(xat:A,p:P)
Christian Müller's avatar
Christian Müller committed
17

18 19
Target

Christian Müller's avatar
Christian Müller committed
20
Read(xat:A, xbt:A, pt:P, rt:R)
Christian Müller's avatar
Christian Müller committed
21 22 23 24

Causality

a:A