Evaluation d'applications de paiement sur carte à puce
Germain Jolly · HAL (Le Centre pour la Communication Scientifique Directe) · 2016
This thesis deals with the methods of evaluation of high level, close to the applications. A method of evaluation of application on smart cards, complementary to the existing methods, was defined during the thesis. The aim is to detect the anomalies present on smart cards (and more precisely on the application of the smart card) and to provide an increased documentation on this error as well as the reasons triggering this error. The user of the tool configures a set of properties corresponding to the expected behaviors of the application that it will check. In order to know the conformity of the behavior of the map application with respect to the theory (specifications), the first step is the generation of the oracle, a reference element during a verification and validation activity. We have turned to a more intelligent technique based on a genetic algorithm that takes as input a set of transaction logs that automatically generates a set of properties (ie a set of local behaviors expected from the map application ). The verification method is developed using the WSCT framework. We used a JavaCard applet developed in the laboratory to test the feasibility of the method for two cases of use: during the test phase, the methodology can be used in parallel with the method used by the certification company and Of the development of the application, the use of this methodology allows a guidance of the development, which makes it possible to use it in the framework of the teaching of the development JavaCard and the evaluation of applications.