notebook.spec 278 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14
Workflow

loop {
	choose {
		forallmay x:User, i:Info
			Written(i, x) → Read += (x, i)
	} {
		forallmay x:User, i:Info
			Oracle(i, x) → Written += (i, x)
	}
}

Declassify

Christian Müller's avatar
Christian Müller committed
15
Oracle(i:Info,x:User): Written(i:Info, u:User)
16 17 18 19 20

Target

Read(u:User, info:Info)

Christian Müller's avatar
Christian Müller committed
21 22 23
Causality

ac:User