This repo contains the formal models for verifying the L1RP protocol described in the paper Practical EMV Relay Protection, Section VII, as well as the models for the mobile versions of Visa/Mastercard.
The file Mobile_Visa.spthy is an edited version of the Visa.spthy with changes made by the owner of the repository.