Verificación automática de protocolos criptográficos de seguridad

Abstract

[ES] Las tarjetas de crédito, el método de pago mayormente usado alrededor del mundo, hacen uso del protocolo EMV para poder comunicar la transacción bancaria de una forma cómoda y segura. La comunicación entre la tarjeta hacia la terminal y la terminal hasta el banco tiene que ser segura para que no se produzca fraude o ningún tipo de error. Actualmente, con la evolución de la tecnología nuevas formas de pago han surgido y entre ellas el modo sin contacto permitiendo hacer uso de las tarjetas para pagar con un pequeño “toque” a la terminal. El estudio The EMV Standard: Break, Fix, Verify estudia y analiza EMV creando un modelo, haciendo uso de la herramienta Tamarin, para poder comprobar la verificación y seguridad del protocolo de una forma automática. El estudio demuestra que el protocolo no es seguro al encontrar que varias de sus configuraciones se le pueden llevar a cabo distintos ataques como saltarse el PIN de seguridad y la verificación del propietario, cuando se está pagando por una gran cantidad de dinero, o ataques que permiten obtener servicios y productos de una forma completamente gratuita sin ningún tipo de cobro. En el trabajo actual se ha entendido y modelado haciendo uso de la herramienta Maude-NPA el protocolo EMV para poder reproducir y verificar de forma automática varios ataques. De esta forma se consigue modelar dos ataques para unas configuraciones del modelo contactless al tratarse de una tecnología más reciente y por tanto, vulnerable. El trabajo corrobora los ataques descubiertos en el estudio mencionado anteriormente y afirma que el protocolo EMV no es seguro para ciertas configuraciones del modelo contactless para las tarjetas VISA.

[EN] Credit cards, the most widely used payment method around the world, use the EMV protocol in order to communicate the banking transaction in a convenient and secure way. The communication between the card to the terminal and the terminal to the bank must be secure in order to avoid fraud or any kind of error. Currently, with the evolution of technology new ways of payment have emerged, including contactless mode, allowing cards to be used to pay with a small "touch" to the terminal. The study The EMV Standard: Break, Fix, Verify studies and analyzes EMV by creating a model, using the Tamarin tool, to verify the verification and security of the protocol automatically. The study shows that the protocol is not secure by finding that several of its configurations can be attacked in different ways such as bypassing the security PIN and owner verification, when paying for a large amount of money, or attacks that allow services and products to be obtained completely free of charge. In the current work, the EMV protocol has been understood and modeled using the MaudeNPA tool in order to automatically reproduce and verify several attacks. In this way two attacks have been modeled for some configurations of the contactless model as it is a more recent technology and consequently, vulnerable. The work corroborates the attacks discovered in the aforementioned study and affirms that the EMV protocol is not secure for certain configurations of the contactless model for VISA cards.