EMV Card: Generation of Test Cases based on SysML Models

The smart cards are increasingly used in several fields with critical data that require security. We cite, as example, the medical field and payment shopping with smart card. Therefore, the hardware and software security of smart cards is one of the key elements of the security of sensitive information handled. Currently, several scientific researchers are interested in studying and enhancing the smart cards security. The study of vulnerabilities is a prerequisite for building security guarantees of this type of devices. Indeed, each vulnerability can easily lead to an attack. In this paper, we generate vulnerability test cases based on models of Europay-MasterCard and Visa (EMV) specifications. We used SysML language to model the EMV transaction through machine state diagram. Then, we generated Event-B model that we exploit it to generate vulnerability and robustness test cases. This work aims to ensure the safety of EMV cards against attacks exploiting the vulnerability of the system.