Tamarin specifications for the verification of the zero-knowledge contingent payment protocol presented in: S. Bursuc and S. Mauw - "Contingent payments from two-party signing and verification for abelian groups". Experiments were run on Tamarin version 1.4.1.