This tutorial describes how to reason about cryptographic protocols in perfect cryptography models using ordinary program invariants.