Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs