Protocols by Invariants