easychair3.spec 382 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
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
Christian Müller's avatar
Christian Müller committed
6
	!Conf(x,p) -> Ass += (x,p)
Christian Müller's avatar
Christian Müller committed
7
forallmay x:A,p:P
Christian Müller's avatar
Christian Müller committed
8
9
	(Ass(x,p) ∧ O(x,p)) -> Acc += (x,p)
loop {
Christian Müller's avatar
Christian Müller committed
10
11
	forall xa:A,xb:A,p:P (Ass(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
	forallmay x:A,p:P (Ass(x,p) ∧ O(x,p)) -> Acc += (x,p)
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
O(x:A,p:P,r:R): G ¬ Conf(x:A,p:P)
Christian Müller's avatar
Christian Müller committed
17

Christian Müller's avatar
Christian Müller committed
18
19
Target

Christian Müller's avatar
Christian Müller committed
20
Read(xa:A,xb:A,p:P)
Christian Müller's avatar
Christian Müller committed
21
22
23
24

Causality

a:A