@inproceedings{basinGettingChipCard2024, title = {Getting {{Chip Card Payments Right}}}, booktitle = {{{FM}}'2024}, author = {Basin, David and Hofmeier, Xenia and Sasse, Ralf and {Toro-Pozo}, Jorge}, year = {2024}, month = sep, publisher = {Springer}, address = {Milan}, abstract = {EMV is the international protocol standard for smart card payments and is used in billions of payment cards worldwide. Despite the standard's advertised security, various issues have been previously uncovered, deriving from logical flaws that are hard to spot in EMV's lengthy and complex specification. We have formalized various models of EMV in Tamarin, a symbolic model checker for cryptographic protocols. Tamarin was extremely effective in finding critical flaws, both known and new, and in many cases exploitable on actual cards. We report on these past problems as well as followup work where we verified the latest, improved version of the protocol, the EMV kernel C8. This work puts C8's correctness on a firm, formal basis, and clarifies which guarantees hold for C8 and under which assumptions. Overall our work supports the thesis that cryptographic protocol model checkers like Tamarin have an essential role to play in improving the security of real-world payment protocols and that they are up to this challenge.}, langid = {english} }