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

forall x
	True -> R += (x)
forall x,s
    O(x,s) -> S += (x)

Declassify

O(x,s): R(xt)

Target

S(xt)