I will discuss how security and privacy can be reasoned about in what looks very like the ordinary wp- (hence also B-) style. The state is separated into "visible-" and "hidden" parts, using extra declarations, and then a modified refinement relation is introduced that "preserves ignorance" of the hidden part.

There are certain broad "structuring principles" that should apply if the method is to scale-up, and I'll discuss what they are.

As an example, I will derive The Dining Cryptographers protocol via a program algebra based on the restricted refinement relation, showing therefore that we haven't restricted refinement so much that soundness is retaind simply by being unable to refine anything at all.

The fetchingly named "Refinement Paradox" crops up along the way, and we'll see how it's not such a problem after all.

With any luck, B- and similar "refinement engines" might one day be able to carry out such proofs semi-mechanically.