Workflow

forallmay x:X,p:P
    True -> Conf += (x,p)
forall x:X,p:P
    True -> Assign += (x,p)
forall x:X,p:P
    (Assign(x,p) ∧ O(x,p)) -> Report += (x,p)
forallmay y:X,x:X,p:P
    (Report(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)

Declassify

O(x:X,p:P): ¬ Conf(xt:X,p:P)

Target

Comm(xt:X, yt:X, pt:P)

Causality

a:X