conference_stubborn_withB.spec 397 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4
Workflow

forallmay x:A,p:P
    True → Conf += (x,p)
Christian Müller's avatar
Christian Müller committed
5
forall x:A,p:P
Christian Müller's avatar
Christian Müller committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
    B(x,p) → Assign += (x,p)
forall x:A,p:P
    (Assign(x,p) ∧ Oracle(x,p)) → Review += (x,p)
loop {
    forall xa:A,xb:A,p:P (Assign(xa,p) ∧ Review(xb,p)) → Read += (xa,xb,p)
    forallmay x:A,p:P (Assign(x,p)) → Review += (x,p)
}

Declassify

Oracle(x:A,p:P): ¬ Conf(xat:A,p:P)

Target

Read(xat:A, xbt:A, pt:P)