Public-key cryptography (PKC) plays an important role for establishing secure communications in a payment standard named after its three founder companies: Europay, MasterCard, and Visa (EMV). However, if a sufficiently large and fault-tolerant (LFT) quantum computer is developed, it would break PKC in the future. Since the class of offline transactions of the EMV protocol rely on PKC security, it is necessary to transition EMV to quantum-resistant cryptography. Bettale, De Oliveira, and Dottax [1] proposed a post-quantum (PQ) version of an EMV offline transaction payment protocol. However, Bettale, De Oliveira, and Dottax [1] did not prove the security of the proposed PQ version of the protocol. To fill this gap, this thesis implemented the current and PQ version of the EMV offline transaction payment protocol in a formal verification tool for cryptographic protocols, called Tamarin. Tamarin is an established symbolic verification tool which has been previously used to analyze Transport Layer Security 1.3 [2] and the Attack Resilient Public Key Infrastructure [3]. Additionally, EMV has been analyzed in Tamarin before in a study conducted by Basin, Sasse, and Toro-Pozo [4] and the security properties defined in their work were used in this thesis, so that the results can be compared. Our analysis of the EMV post-quantum extension by Bettale, De Oliveira, and Dottax [1] suggests that the secrecy of important protocol values such as master key and private key is also achieved in the same model as Basin, Sasse, and Toro-Pozo [4] studied for the original protocol. However, the Tamarin models implemented by Basin, Sasse, and Toro-Pozo [4] assumed that all of the acting agents are honest, which makes the models weaker than desirable. Therefore, we suggest to continue the research for more comprehensive understanding of EMV security by building a model that allows the acting agents to be compromised.Julkisen avaimen salaus on tärkeä osa luomaan turvallisen keskusteluyhteyden kortin ja terminaalin välille EMV:ssä. Tarpeeksi tehokas ja virheetön kvanttikone pystyy murtamaan julkisen avaimen salauksen tulevaisuudessa. Transaktiot jotka tapahtuvat offline-tilassa, ovat täten haavoittuvaisia kvanttikoneiden kehityksen myötä. Tämän takia EMV:n on tärkeä siirtyä kvanttikoneita kestäviin salausalgoritmeihin. Bettale, De Oliveira ja Dottax [1] julkaisi ratkaisun ongelmaan ehdottamalla protokollan, jonka salausta kvanttitietokoneet eivät teoriassa pysty murtamaan. Artikkeli ei kuitenkaan todistanut ehdottamaansa protokollaa turvalliseksi, joten tämä diplomityö jatkaa tutkimusta implementoimalla ehdotetun kvanttiturvallisen protokollan työkalussa nimeltä Tamarin. Tamarin on vakiintunut symbolinen varmistustyökalu, joka on tarkoitettu kryptografian protokollien tutkimiseen. Aikaisemmin työkalulla on analysoitu esimerkiksi TLS 1.3 salausprotokollaa [2]. EMV:tä on myös aikaisemmin tutkittu Tamarinilla tutkijoiden Basin, Sasse ja Toro-Pozo [4] toimesta ja tässä diplomityössä käytetään heidän määrittelemiä turvallisuus ominaisuuksia (security properties), jotta tämän diplomityön tuloksia voidaan verrata aiempaan tutkimukseen. Diplomityössä saadut tulokset osoittavat, että tutkittujen protokollien salassapito ominaisuudet säilyvät kun tuloksia verrataan artikkelissa [4] saatuihin tuloksiin. Kuitenkin artikkelissa [4] tehdyt mallit olettivat, että kaikki protokollassa toimijat ovat rehellisiä, mikä tekee malleista heikkoja. Siksi tämä diplomityö kehottaa, että tutkimusta olisi hyvä jatkaa suuntaan, jossa protokollassa olevat toimijat voisivat olla myös epärehellisiä.
