Academic literature on the topic 'Monnaie électronique – Mesures de sûreté'

La démocratisation du réseau Internet a favorisé la naissance du commerce électronique entre professionnels et particuliers, mais c'est la confiance notamment dans les moyens de paiement électronique qui lui permettra de se développer. C'est pourquoi à côté de la carte bancaire, d'autres systèmes particuliers de paiement en ligne ont été mis en place pour permettre les micro-paiements. Pour parvenir à une sécurité optimale, les professionnels utilisent essentiellement des moyens de protection numérique dont la signature électronique et la certification. Mais à côté de ces moyens classiques, de nouvelles techniques de sécurisation basées sur la biométrie ont vu le jour et avec elles leur lot de questions relatives notamment à la protection de la vie privée et des données personnelles. Cette évolution rapide des techniques transactionnelles a nécessité que le législateur intervienne pour adapter certaines règles consacrant ainsi la preuve et la signature électroniques. Le législateur a également dû créer un cadre juridique spécifique allégé pour permettre le développement des moyens de paiements de monnaie électronique. Mais la confiance passe toujours par la protection, ce qui explique que les dispositions protectrices du consommateur et de ses données bancaires aient été renforcées. La nécessité pour le cybermarchand d'obtenir la confiance du consommateur l'a poussé à se mobiliser dans ce sens et a également donné naissance à de nouveaux professionnels de la confiance (prestataires de services de certification, labels) Enfin, la question de l'identification des consommateurs du point de vue de leur capacité juridique demeure toujours source d'incertitude pour le cybermarchand auquel l'incapacité de l'internaute peut être opposée pour obtenir l'annulation de la transaction. Aujourd'hui le paiement en ligne a atteint un niveau de sécurité optimal et après la révolution d'un pan entier de notre droit il est normal que des ajustements soient nécessaires.

Les transactions sur mobile suscitent depuis quelques années un intérêt grandissant. Cette thèse se place dans le contexte d'un tel service géré par un opérateur de téléphonie mobile. Les transactions sont réalisées entre souscrivants du service uniquement à l'aide de monnaie électronique privative émise par l'opérateur. Le problème de cette thèse réside dans la sécurisation de ces types de services. Nous proposons dans cette thèse une architecture permettant de garantir une sécurité de bout-en-bout entre l'application et la plateforme de paiement. Celle-ci est basée sur l'utilisation conjoint d'un élément de sécurité SE et d'un environnement d'exécution sécurisée TEE. Différentes transactions ont été considérées, paiement marchand et transferts entre particuliers, ainsi que différents modes, tout-connecté, déconnecté ou semi-connecté. Les protocoles proposés ont été vérifiés formellement et leurs performances ont été étudiées. Une étude comparative entre différents algorithmes de classification est également réalisée pour les adapter à la détection de la fraude. A cet effet, le système de paiement et le comportement de ses utilisateurs a été modélisé pour créer un générateur de données synthétiques. Une validation préliminaire de ce simulateur a été réalisée. L'originalité du simulateur est qu'il se base sur l'exploitation de données provenant d'un service déployé sur le terrain
Mobile-based transactions have driven growing attention for the past few years. This thesis focuses on mobile-based transaction systems which are managed by a mobile network operator. In such a context, transactions are carried out with electronic money emitted by the operator by the subscribers of the service only. This thesis addresses the problem of securing such services. We propose an architecture which achieves end-to-end security between the payment platform and the payment application in the mobile device. Is is based on a Secure Element (SE) and a Trusted Execution Environment. Several types of transactions were considered such as payments or transfers as well as different modes based on the connection availability of the various actors. The protocols proposed were formally verified. Their performances were also taken into account. Several classification algorithms were compared to be adapted to the fraud detection problem in mobile-based systems. To achieve this, the payment platform and the user's behavior were modeled to create a synthetic data generator. The latter is preliminarily validated in the thesis. The originality of this simulator is that it is based on data from an existing system

Les autorités publiques ainsi que les acteurs privés se sont efforcés, depuis quelques années, de mettre en place diverses dispositions juridiques et technologiques concourant à la sécurité des paiements en ligne, vecteur essentiel de la confiance et du développement du commerce électronique. L'objectif de ce travail de recherche est de présenter le processus de co-régulation avec lequel les institutions nationales et internationales ont abordé les divers aspects juridiques du paiement en ligne (assouplissement du régime juridique des technologies cryptographiques, reconnaissance de l'écrit et la signature électroniques, statut des établissements de monnaie électronique, standardisation des procédés techniques et lutte contre la cybercriminalité), dans le but d'équilibrer, de manière consensuelle et concomitante, des enjeux sécuritaires et des enjeux économiques (croissance économique et protection du consommateur). L'Union européenne est au cœur, et souvent à l'initiative de ce chantier juridique, manifestant ainsi, par des dispositions générales, une volonté d'harmonisation d'un régime juridique lié au paiement en ligne sécurisé
Public authorities, along with private entities, have been striving for several years to implement various legal and technological provisions working towards online payment security, which is an essential vehicle for trust in electronic commerce and its expansion. The aim of this research is to present the coregulation procedure used by national and international institutions to approach the various legal aspects of online payments (more flexible regulations for encryption technologies, acknowledgement of electronic writings and signatures, status of electronic currency establishments, standardization of technical processes, and fight against cyberfraud), with the aim of balancing both security and economic stakes (economic growth and consumer protection) in a consensual and concomitant manner. The European Union is at the heart, and often the initiator, of this judicial edifice, thus displaying through general clauses a strong will to harmonize the legal system in regard to secure online payment

Dans cette thèse, nous exposons nos contributions à l'amélioration de l'écosystème du Mobile Money en identifiant ses défis majeurs et en proposant des solutions adaptées. Ces solutions visent à renforcer la sécurité et l'interopérabilité des services de Mobile Money, tout en prenant en compte les capacités limitées des terminaux mobiles. Pour ce faire, nous avons réaliséun état des lieux qui met en lumière des enjeux clés, tels que l'absence de fédération, de traçabilité et d'interopérabilité entre les plateformes Mobile Money des opérateurs de téléphonie mobile, ces dernières étant gérées par des bases de données distinctes.La blockchain est présentée comme une solution pour améliorer la sécurité, la transparence et la fiabilité des transactions. L'outil BTOOLS, un logiciel open source compatible avec plusieurs plateformes, a été développé pour générer des transactions blockchain sécurisées à l'aide de services cryptographiques. Une nouvelle architecture de Mobile Money intégrant lablockchain et l'USSD a également été proposée pour garantir une interconnexion transparente entre les différents acteurs de l'écosystème, y compris les banques, les MNO, les régulateurs et les clients.Le protocole « Mobile Money Using Blockchain » (2MUB) est un élément central des contributions de la thèse. Il a été développé en deux versions, la seconde apportant des améliorations en matière d'interopérabilité de traçabilité et de fédération.Ce protocole utilise une architecture décentralisée basée sur des smart contracts pour définir les règles decompensation entre les acteurs du Mobile Money. Trois scénarii d'implémentation ont été proposés : deux via lecanal USSD, et un via TCP/IP.Enfin, une plateforme expérimentale a été développée pour valider le protocole 2MUB. Elle utilise Node.js, Ganache, Hardhat et Sepolia pour implémenter une blockchain à deux niveaux, et son interface utilisateur est accessible via USSD grâce à Africa’s Talking. Des analyses ont montré le bon fonctionnement de la solution proposée
In this thesis, we present our contributions to the improvement of the Mobile Money ecosystem by identifying its major challenges and proposing suitable solutions. These solutions aim to enhance the security and interoperability ofMobile Money services while considering the limited capabilities of mobile devices. To achieve this, weconducted a state-of-the-art analysis that highlights key issues, such as the lack of federation, traceability, and interoperability between the Mobile Money platforms of mobile network operators (MNOs), as these are managed by separate databases.Blockchain is proposed as a solution to improve the security, transparency, and reliability of transactions. The BTOOLS tool, an open-source software compatible with multiple platforms, was developed to generate secure blockchain transactions using cryptographic services. A new Mobile Money architecture integrating blockchain and USSD was also proposed to ensure seamless interconnection between the various actors in the ecosystem, including banks, MNOs, regulators, and customers.The "Mobile Money Using Blockchain" (2MUB) protocol is a central element of the thesis contributions. It was developed in two versions, with the second offering improvements in terms of interoperability, traceability, and federation. Thisprotocol uses a decentralized architecture based on smart contracts to define settlement rules among Mobile Money participants. Three implementation scenarios were proposed: two via the USSD channel, and one via TCP/IP.Finally, an experimental platform was developed to validate the 2MUB protocol. It uses Node.js, Ganache, Hardhat, and Sepolia to implement a two-layer blockchain, with its user interface accessible via USSD through Africa’s Talking. Analyses have shown that the proposed solution functions well

Cette thèse traite des méthodes d'évaluation de haut niveau, proche des applications. Une méthode d'évaluation d'application sur cartes à puces, complémentaire aux méthodes existantes, a été définie durant de la thèse. Le but est de détecter les anomalies présentes sur cartes à puce (et plus précisément sur l'application de la carte à puce) et de fournir une documentation accrue sur cette erreur ainsi que les raisons déclencheurs de cette erreur. L'utilisateur de l'outil configure un ensemble de propriétés correspondant aux comportements attendus de l'application qu'il va vérifier. Afin de connaître la conformité du comportement de l'application carte vis à vis de la théorie (spécifications), la première étape est la génération de l'oracle, élément de référence lors d'une activité de vérification et validation. Nous nous sommes orientés vers une technique plus intelligente basée sur un algorithme génétique prenant en entrée un ensemble de logs de transaction qui permet de générer automatiquement un ensemble de propriétés (c'est à dire un ensemble de comportements locaux et attendus de l'application carte). La méthode de vérification est développée grâce au framework WSCT. Nous avons utilisé une applet JavaCard développée au laboratoire afin de tester la faisabilité de la méthode pour deux cas d'usages : lors de la phase de test, la méthodologie peut être utilisée en parallèle de la méthode utilisée par l'entreprise de certification et lors du développement de l'application, l'utilisation de cette méthodologie permet un guidage du développement, ce qui permet de l'utiliser dans le cadre de l'enseignement du développement JavaCard et de l'évaluation d'applications
This thesis deals with high-level evaluation of applications in smartcards. The proposed method combines observation of the communication and detection of violated properties. The goal is to detect anomalies on smart cards (and more precisely on its implementation) and provide a better documentation on this error and on the reasons that triggered this error. We can know on the fly if an application has an error of implementation. The user of the tool configures a set of properties corresponding to the expected behavior of the application. To ascertain compliance of the behavior of the card application with the theory (specifications), the first step is the generation of the oracle, reference used during verification and validation activity. We quickly directed to a smarter technique to target the most interesting behaviors to check for our study. We worked on a generation method based on a genetic algorithm taking as input a set of transaction logs to automatically generate a set of properties (i. E. A set of local and expected behaviors of the applications). The evaluation methodology is developed through the WSCT framework. Two plugins were created and used to communicate with the smart card application, but also to observe and detect an abnormality in the behavior of the application. We used a JavaCard applet developed in the laboratory to test the feasibility of the method for two use cases: during the test phase, the methodology can be used in parallel by the certification firm and during the development of an application, for example, allowing improving the teaching of the JavaCard development and the evaluation of application

Les “smart-devices” tels les smartphones, tablettes et même les montres ont été largement démocratisés au cours de la dernière décennie. Dans nos sociétés occidentales, on ne garde plus seulement son ordinateur personnel chez soi, on le transporte dans la poche arrière de son pantalon ou bien autour de son poignet. Ces outils ne sont d’ailleurs plus limités, en termes d’utilisation, à de la simple communication par SMS ou bien téléphone, on se fie à eux pour stocker nos photos et données personnelles, ces dernières parfois aussi critiques que des données de paiement bancaires, on gère nos contacts et finances, se connecte à notre boite mail ou un site marchand depuis eux. . . Des exemples récents nous fournissent d’ailleurs un aperçu des tâches de plus en plus complexes que l’on confie à ces outils : l’Estonie autorise l’utilisation de smartphones pour participer aux scrutins nationaux et en 2017, la société Transport for London a lancé sa propre application autorisant l’émulation d’une Oyster card et son rechargement pour emprunter son réseau de transports publics. Plus les services se complexifient, plus la confiance qui leur est accordée par les groupes industriels et les utilisateurs grandit. Nous nous intéressons ici aux protocoles cryptographiques qui définissent les échanges entre les outils et entités qui interviennent dans l’utilisation de tels services et aux garanties qu’ils proposent en termes de sécurité (authentification mutuelle des agent, intégrité des messages circulant, secret d’une valeur critique…). Moult exemples de la littérature et de la vie courante ont démontré que leur élaboration était hautement vulnérable à des erreurs de design. Heureusement, des années de recherches nous ont fournis des outils pour rendre cette tâche plus fiable, les méthodes formelles font partie de ceux-là. Il est possible de modeler un protocole cryptographique comme un processus abstrait qui manipule des données et primitives cryptographiques elles aussi modélisées comme des termes et fonctions abstraites. On met le protocole à l’épreuve face à un attaquant actif et on peut spécifier mathématiquement les propriétés de sécurité qu’il est censé garantir. Ces preuves de sécurité peuvent être automatisées grâce à des outils tels que ProVerif ou bien Tamarin. L’une des grandes difficultés lorsque l’on cherche à concevoir et prouver formellement la sécurité d’un protocole de niveau industriel réside dans le fait que ce genre de protocole est généralement très long et doit satisfaire des propriétés de sécurité plus complexes que certains protocoles universitaires. Au cours de cette thèse, nous avons souhaité étudier deux cas d’usage : le vote électronique et le paiement mobile. Dans les deux cas, nous avons conçu et prouvé la sécurité d’un protocole répondant aux problématiques spécifiques à chacun des cas d’usage. Dans le cadre du vote électronique, nous proposons le protocole Belenios VS, une variante de Belenios RF. Nous définissons l’écosystème dans lequel le protocole est exécuté et prouvons sa sécurité grâce à ProVerif. Belenios VS garantit la confidentialité du vote et le fait qu’un utilisateur puisse vérifier que son vote a bien fait parti du résultat final de l’élection, tout cela même si l’outil utilisé par le votant est sous le contrôle d’un attaquant. Dans le cadre du paiement, nous avons proposé la première spécification ouverte de bout en bout d’une application de paiement mobile. Sa conception a pris en compte le fait qu’elle devait pouvoir s’adapter à l’écosystème de paiement déjà existant pour être largement déployable et que les coûts de gestion, de développement et de maintenance de la sécurité devait être optimisés
The last decade has seen the massive democratization of smart devices such as phones, tablets, even watches. In the wealthiest societies of the world, not only do people have their personal computer at home, they now carry one in their pocket or around their wrist on a day to day basis. And those devices are no more used simply for communication through messaging or phone calls, they are now used to store personal photos or critical payment data, manage contacts and finances, connect to an e-mail box or a merchant website... Recent examples call for more complex tasks we ask to such devices: Estonia voting policy allows the use of smart ID cards and smartphones to participate to national elections. In 2017, Transport for London launched the TfL Oyster app to allow tube users to top up and manage their Oyster card from their smartphone. As services grow with more complexity, so do the trust users and businesses put in them. We focus our interest into cryptographic protocols which define the exchanges between devices and entities so that such interaction ensure some security guarantees such as authentication, integrity of messages, secrecy… Their design is known to be an error prone task. Thankfully, years of research gave us some tools to improve the design of security protocols, among them are the formal methods: we can model a cryptographic protocol as an abstract process that manipulates data and cryptographic function, also modeled as abstract terms and functions. The protocol is tested against an active adversary and the guarantees we would like a protocol to satisfy are modeled as security properties. The security of the protocol can then be mathematically proven. Such proofs can be automated with tools like ProVerif or Tamarin. One of the big challenge when it comes to designing and formally proving the security an “industrial- level” protocol lies in the fact that such protocols are usually heavier than academic protocols and that they aim at more complex security properties than the classical ones. With this thesis, we wanted to focus on two use cases: electronic voting and mobile payment. We designed two protocols, one for each respective use case and proved their security using automated prover tools. The first one, Belenios VS, is a variant of an existing voting scheme, Belenios RF. It specifies a voting ecosystem allowing a user to cast a ballot from a voting sheet by flashing a code. The protocol’s security has been proven using the ProVerif tool. It guarantees that the vote confidentiality cannot be broken and that the user is capable of verifying their vote is part of the final result by performing a simple task that requires no technical skills all of this even if the user’s device is compromised – by a malware for instance. The second protocol is a payment one that has been conceived in order to be fully scalable with the existing payment ecosystem while improving the security management and cost on the smartphone. Its security has been proven using the Tamarin prover and holds even if the user’s device is under an attacker’s control

EMV est la norme implémentée pour sécuriser une transaction d'achat avec contact ou sans contact (NFC) entre un appareil de paiement d'un client et un PoS. Elle représente un ensemble de messages de sécurité échangés entre les acteurs de la transaction, garantissant plusieurs propriétés de sécurité importantes. En effet, plusieurs chercheurs ont analysé le fonctionnement de la norme EMV afin de vérifier sa fiabilité: ils ont identifié plusieurs vulnérabilités de sécurité qui représentent aujourd'hui des risques majeurs pour notre sécurité au quotidien. Par conséquent, nous sommes intéressés à proposer de nouvelles solutions qui visent à améliorer la fiabilité d’EMV. Dans un premier temps, nous présentons un aperçu du système de sécurité EMV et nous étudions ses vulnérabilités identifiées dans la littérature. En particulier, il existe deux vulnérabilités de sécurité EMV, qui mènent à des risques dangereux menaçant à la fois les clients et les commerçants. Par conséquent, nous sommes intéressés dans la deuxième étape à répondre à ces deux faiblesses. Nous examinons d'abord une sélection des travaux qui ont été conçus pour résoudre ces vulnérabilités. Ensuite, afin d'obtenir de meilleurs résultats par rapport à ces travaux, nous proposons un nouveau système pour le paiement avec contact et NFC qui intègre 4 mécanismes de sécurité innovants. Enfin, dans la troisième étape, nous adaptons notre premier mécanisme de sécurité dans le contexte d'une nouvelle architecture de paiement NFC. Cette architecture est particulièrement destinée aux petits commerçants, leur permettant de profiter de leurs smartphones NFC pour une utilisation directe en tant que des lecteurs NFC
EMV is the standard implemented to secure the communication, between a client’s payment device and a PoS, during a contact or NFC purchase transaction. It represents a set of security messages, exchanged between the transaction actors, guaranteeing several important security properties. Indeed, researchers in various studies, have analyzed the operation of this standard in order to verify its reliability: unfortunately, they have identified several security vulnerabilities that, today, represent major risks for our day to day safety. Consequently, in this thesis, we are interested in proposing new solutions that improve the reliability of this standard. In the first stage, we introduce an overview of the EMV security payment system and we survey its vulnerabilities identified in literature. In particular, there are two EMV security vulnerabilities that lead to dangerous risks threatening both clients and merchants: (1) the confidentiality of banking data is not guaranteed, (2) the authentication of the PoS is not ensured to the client’s device. Therefore, our interests move in the second stage to address these two weaknesses. We first review a selection of the related works that have been implemented to solve these vulnerabilities, and then, in order to obtain better results than the related works, we propose a new secure contact and NFC payment system that includes four innovative security mechanisms. Finally, in the third stage, we adapt our first security mechanism in the context of a new NFC payment architecture. This architecture is especially destined for small merchants, allowing them to take advantage of their NFC smartphones for use directly as NFC readers

Les “smart-devices” tels les smartphones, tablettes et même les montres ont été largement démocratisés au cours de la dernière décennie. Dans nos sociétés occidentales, on ne garde plus seulement son ordinateur personnel chez soi, on le transporte dans la poche arrière de son pantalon ou bien autour de son poignet. Ces outils ne sont d’ailleurs plus limités, en termes d’utilisation, à de la simple communication par SMS ou bien téléphone, on se fie à eux pour stocker nos photos et données personnelles, ces dernières parfois aussi critiques que des données de paiement bancaires, on gère nos contacts et finances, se connecte à notre boite mail ou un site marchand depuis eux. . . Des exemples récents nous fournissent d’ailleurs un aperçu des tâches de plus en plus complexes que l’on confie à ces outils : l’Estonie autorise l’utilisation de smartphones pour participer aux scrutins nationaux et en 2017, la société Transport for London a lancé sa propre application autorisant l’émulation d’une Oyster card et son rechargement pour emprunter son réseau de transports publics. Plus les services se complexifient, plus la confiance qui leur est accordée par les groupes industriels et les utilisateurs grandit. Nous nous intéressons ici aux protocoles cryptographiques qui définissent les échanges entre les outils et entités qui interviennent dans l’utilisation de tels services et aux garanties qu’ils proposent en termes de sécurité (authentification mutuelle des agent, intégrité des messages circulant, secret d’une valeur critique…). Moult exemples de la littérature et de la vie courante ont démontré que leur élaboration était hautement vulnérable à des erreurs de design. Heureusement, des années de recherches nous ont fournis des outils pour rendre cette tâche plus fiable, les méthodes formelles font partie de ceux-là. Il est possible de modeler un protocole cryptographique comme un processus abstrait qui manipule des données et primitives cryptographiques elles aussi modélisées comme des termes et fonctions abstraites. On met le protocole à l’épreuve face à un attaquant actif et on peut spécifier mathématiquement les propriétés de sécurité qu’il est censé garantir. Ces preuves de sécurité peuvent être automatisées grâce à des outils tels que ProVerif ou bien Tamarin. L’une des grandes difficultés lorsque l’on cherche à concevoir et prouver formellement la sécurité d’un protocole de niveau industriel réside dans le fait que ce genre de protocole est généralement très long et doit satisfaire des propriétés de sécurité plus complexes que certains protocoles universitaires. Au cours de cette thèse, nous avons souhaité étudier deux cas d’usage : le vote électronique et le paiement mobile. Dans les deux cas, nous avons conçu et prouvé la sécurité d’un protocole répondant aux problématiques spécifiques à chacun des cas d’usage. Dans le cadre du vote électronique, nous proposons le protocole Belenios VS, une variante de Belenios RF. Nous définissons l’écosystème dans lequel le protocole est exécuté et prouvons sa sécurité grâce à ProVerif. Belenios VS garantit la confidentialité du vote et le fait qu’un utilisateur puisse vérifier que son vote a bien fait parti du résultat final de l’élection, tout cela même si l’outil utilisé par le votant est sous le contrôle d’un attaquant. Dans le cadre du paiement, nous avons proposé la première spécification ouverte de bout en bout d’une application de paiement mobile. Sa conception a pris en compte le fait qu’elle devait pouvoir s’adapter à l’écosystème de paiement déjà existant pour être largement déployable et que les coûts de gestion, de développement et de maintenance de la sécurité devait être optimisés
The last decade has seen the massive democratization of smart devices such as phones, tablets, even watches. In the wealthiest societies of the world, not only do people have their personal computer at home, they now carry one in their pocket or around their wrist on a day to day basis. And those devices are no more used simply for communication through messaging or phone calls, they are now used to store personal photos or critical payment data, manage contacts and finances, connect to an e-mail box or a merchant website... Recent examples call for more complex tasks we ask to such devices: Estonia voting policy allows the use of smart ID cards and smartphones to participate to national elections. In 2017, Transport for London launched the TfL Oyster app to allow tube users to top up and manage their Oyster card from their smartphone. As services grow with more complexity, so do the trust users and businesses put in them. We focus our interest into cryptographic protocols which define the exchanges between devices and entities so that such interaction ensure some security guarantees such as authentication, integrity of messages, secrecy… Their design is known to be an error prone task. Thankfully, years of research gave us some tools to improve the design of security protocols, among them are the formal methods: we can model a cryptographic protocol as an abstract process that manipulates data and cryptographic function, also modeled as abstract terms and functions. The protocol is tested against an active adversary and the guarantees we would like a protocol to satisfy are modeled as security properties. The security of the protocol can then be mathematically proven. Such proofs can be automated with tools like ProVerif or Tamarin. One of the big challenge when it comes to designing and formally proving the security an “industrial- level” protocol lies in the fact that such protocols are usually heavier than academic protocols and that they aim at more complex security properties than the classical ones. With this thesis, we wanted to focus on two use cases: electronic voting and mobile payment. We designed two protocols, one for each respective use case and proved their security using automated prover tools. The first one, Belenios VS, is a variant of an existing voting scheme, Belenios RF. It specifies a voting ecosystem allowing a user to cast a ballot from a voting sheet by flashing a code. The protocol’s security has been proven using the ProVerif tool. It guarantees that the vote confidentiality cannot be broken and that the user is capable of verifying their vote is part of the final result by performing a simple task that requires no technical skills all of this even if the user’s device is compromised – by a malware for instance. The second protocol is a payment one that has been conceived in order to be fully scalable with the existing payment ecosystem while improving the security management and cost on the smartphone. Its security has been proven using the Tamarin prover and holds even if the user’s device is under an attacker’s control

Les transactions électroniques ont ouvert la voie à une multitude de possibilités déclinées sous diverses formes : le portail internet d’une banque pour consulter ses comptes, une carte à puce permettant d’ouvrir une porte ou de valider son titre de transport en commun, une application téléchargée sur un ordinateur ou un équipement mobile comme un assistant personnel numérique ou un téléphone portable. Cette dernière catégorie d’´equipement mobile est extrêmement porteuse en termes d’offres de services. En effet, un mobile est un équipement nomade, connecté à l’Internet avec des débits de plus en plus élevés, et il est aussi de plus en plus puissant. Avec l’avènement de la technologie NFC (Near Field Communication) et des architectures sécurisées, le mobile a maintenant la possibilité d’héberger des applications sensibles dans une puce sécurisée, appelée « Secure Element ». Contrairement aux facteurs de formes plastiques, le Secure Element est un environnement dynamique sur lequel on peut charger des applications qui seront accessibles par un lecteur comme un terminal de paiement ou un lecteur de badge d’accès à un bâtiment. On parle alors de service mobile sans-contact ou de service mobile NFC. Nous proposons dans cette thèse d’apporter plusieurs contributions pour faciliter le déploiement de services mobiles exploitant un Secure Element. L’adoption de ce type de service pour des applications `a forte valeur ajoutée passe par une infrastructure et des outils partagés par les différents acteurs. Dans un premier temps, nous proposons trois contributions pour l’aide au déploiement de services mobiles basé sur un Secure Element afin de : faciliter la personnalisation d’un Secure Element par un TSM non propriétaire de celui-ci, faciliter l’échange de clés pour le TSM et réaliser une transaction avec un téléphone mobile comme Terminal de Paiement Electronique). Dans un second temps, nous nous intéressons à l’analyse de la sécurité des transactions de paiement
Electronic transactions have paved the way for a multitude of services in various forms : a home banking web portal, an access control smart card opening a door or paying a transit fare, or an application downloaded onto a computer or a mobile device such a personal digital assistant or a mobile phone. The latter category of mobile equipment is extremely promising in terms of service offers. Indeed, a mobile handheld device is connected to the Internet with speeds higher and higher and is also more powerful. With the advent of the NFC (Near Field Communication) technology and secure architectures, mobile devices now has the ability to host sensitive applications in a secure chip, called « Secure Element ». Unlike plastic form factors, the Secure Element is a dynamic environment where you can download applications that will be accessible by a reader such as a point of sale or an access control reader. Those services are called mobile contactless services or NFC mobile services. We propose in this thesis several contributions to facilitate the deployment of mobile services based on a Secure Element. The adoption of this high added value services relies on an infrastructure and tools shared by different actors. As a first step, we propose three contributions to aid the deployment of mobile services Secure Element based allowing to: facilitate the personalization of a Secure Element by a TSM non-owner thereof, facilitate the exchange of keys for the TSM and perform a transaction with a mobile phone as a point of sale. In a second step, we focus on the analysis of payment transactions

Grâce à l'avènement des réseaux de télécommunications, de nombreux acteurs ont exprimé des besoins hétérogènes liés au transfert électronique sécurisé de document. Ces acteurs peuvent être professionnels (une entreprise souhaitant transmettre des plans de fabrication à un de ses fournisseurs), particuliers (un individu souhaitant partager ses photos de vacances avec un proche) ou gouvernementaux (une procédure administrative devant être envoyée au département d'une administration). L'hétérogénéité des besoins susnommés provient de la nature des documents traités, mais également des propriétés de sécurité à assurer. Afin de satisfaire ces différents besoins, de nombreux protocoles sécurisés de communication ont ainsi été développés. Néanmoins, il n'existe pas de bijection entre les protocoles et les besoins et il très souvent difficile d'associer à un besoin le protocole adéquat. Au cours de leur cycle de vie, les protocoles de communication existants peuvent être gérés (utilisés, créés et déployés) par trois rôles : l'utilisateur, le développeur de protocole et l'administrateur système. Chacun de ces derniers est confronté à un problème spécifique : Après avoir exprimé un besoin, l’utilisateur ne dispose pas de suffisamment de critères pour évaluer les protocoles candidats, et ne peut obtenir l’assurance que le protocole choisi satisfait bien le besoin exprimé. Le développeur de protocole doit faire face à des choix critiques lorsqu’il doit implémenter un nouveau protocole, particulièrement celui des bibliothèques de sécurité à utiliser. De plus, il n’existe pas de correspondance simple entre une propriété de sécurité et les outils cryptographiques, ce qui peut freiner le passage de la spécification à l’implémentation. L’administrateur système paye les conséquences des choix du développeur à travers la multiplication des bibliothèques de sécurité à déployer : chaque protocole peut ainsi être dépendant d’une librairie spécifique sans que l’administrateur ait la possibilité de remplacer, suivant le contexte, cette dépendance par une autre. Le premier objectif de nos travaux est de rechercher une solution à ces problèmes. Une approche par composition nous semble particulièrement viable : les composants logiciels permettent en effet d'isoler des fonctionnalités spécifiques à des fins de réutilisabilité et de composition. De plus, l'utilisation de tels composants permet à une application d'annoncer et de certifier certaines caractéristiques requises par ses utilisateurs. Dans le cadre de cette thèse, nous définissons la notion de composants de sécurité de haut niveau remplissant chacun une propriété de sécurité et disposant d'une interface générique permettant leur utilisation par différents protocoles et applications. Le second objectif de cette thèse est la conception de notre architecture appelée A. D. E. P. T. (Architecture pour les Documents Électroniques Plus leurs Transferts) et consacrée au transfert électronique de document. Cette architecture, paramétrée par des politiques de sécurité, tire partie des composants de sécurité de haut niveau grâce à un ou plusieurs assemblage(s) de ces composants adapté(s) aux besoins des différents rôles. Ces différents assemblages permettent d'illustrer les fonctionnalités de nos composants et de montrer leurs utilisations variées par les rôles susmentionnés
In our Information Era, various actors have expressed their needs related to electronic document transfer. These actors can be corporates (a company willing to send confidential schematics to its subcontractor), individuals (a person wishing to share his holiday pictures with his friend) or governments (an administration sending documents to another department). These needs are heterogeneous because they depend not only on the document being transferred, but also on the security properties to fulfill. To satisfy these different needs, numerous secure communication protocols have been developed. However, there is no bijection between the protocols and the needs: thus, it is difficult to associate the adequate protocol to a specific need. During their life cycles, the existing communication protocols can be managed (created, deployed, and used) by three roles, each of them having different objectives: non-expert user, protocol developer and system administrator. The first objective of this thesis is to help these roles find a solution to their problems. A component-based approach seems particularly suitable: in fact, software components allow to isolate specific functionalities for reuse and composition. Moreover, the use of such components enables applications to certify features which may be required by the users. In the context of this work, we define the notion of high level security components, each fulfilling a security property. These components have a generic interface which allows their use by various protocols and applications. The second objective of this thesis is to design an architecture named A. D. E. P. T. And dedicated to the electronic document transfer. This architecture, driven by security policies, relies on one or several assemblies of high level security components to satisfy users needs. These assemblies allow us to illustrate the functionalities of our components as well as their use by the aforementioned roles