Dissertationen zum Thema „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

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écu risé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'exploitati on de données provenant d'un service déployé sur le terrain.

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

Le montant annuel de la fraude européenne à la carte de paiement se monte à plus d’1,5 milliard d’euros. Cette manne aiguise l’appétit des groupes criminels qui exploitent la moindre faille de la monétique (écosystème de la carte de paiement). Les cinq principaux acteurs de la monétique (porteurs, émetteurs, accepteurs, acquéreurs et systèmes de paiement) s’appuient pourtant sur des systèmes et réseaux normalisés dont la sécurité est encadrée par des standards internationaux contraignants. Néanmoins, la fraude monétique ne cesse de progresser alors que les moyens de lutte (étatiques, collaboratifs ou individuels) restent limités.Après étude de la fraude monétique, cette thèse propose différentes actions (passives,réactives et proactives) visant à améliorer la lutte contre la fraude monétique. D’abord,il convient de mieux connaître la fraude en étudiant la provenance des données volées et plus seulement leur usage. Ensuite l’expertise de ces fraudes doit être améliorée, en développant par exemple une captation du progrès scientifique. Une expertise qui doit être en partie transmise aux enquêteurs afin qu’ils puissent conduire leurs enquêtes. Enquêtes qui peuvent être dynamisées par des opérations réactives associant investigateurs et sachants techniques. Enfin, de manière proactive, les enquêtes et analyses de demain doivent être facilitées par les technologies monétiques conçues aujourd’hui
Every year, payment card fraud exceeds 1.5 billion euros in Europe. Organised crime groups are exploiting any vulnerability possible to take a piece of this lucrative activity. Even though the five principal entities in the payment card industry (cardholders, issuers,acceptors, acquirers and payment system providers) are implementing binding security measures through out standardized systems and networks, fraud continues to increase. Efforts by the state, industry collaboration, and individuals have been unsuccessful in decreasing criminal advances. Having analysed the elements of payment card fraud, this thesis proposes several actions (passive, reactive and proactive) to help improve the fight against this fraud. First, itis relevant to gain knowledge of the source of the card details and not to focus only on its reuse. Next, forensic assessment has to be improved, for example by developing an increased scientific understanding of the technology. Such an expertise should then be passed on to investigators through effective training and knowledge transfer. Investigations should also be made more dynamic with reactive operations conducted in concert by investigators and technicians. Finally, in an ideal proactive spirit, future investigations and assessments should be oriented and facilitated by studying and influencing current payment card technology developments

La lutte contre la falsification et la contrefaçon de documents fiduciaires est un défi permanent. Pour sécuriser efficacement les billets de banque et les passeports, l’utilisation de matériaux moléculaires est une ressource de choix. La collaboration entre le laboratoire d’Organométallique pour l’Optique et Oberthur Technologies a permis d’élaborer deux nouveaux systèmes de sécurité. Ces sécurités sont basées, d’une part, sur l’utilisation de dérivés bipyridine changeant de couleur sous l’action des micro-ondes, et d’autre part sur l’utilisation de photochromes de type P et de type T offrant une succession de couleurs par passage successif sous lampes UV-Visible et chauffage. Après un premier chapitre faisant l’état de l’art des sécurités mises en place dans le domaine fiduciaire, les deux chapitres suivants décrivent les résultats obtenus sur le développement des deux nouvelles sécurités
Fighting against forgery and counterfeiting of secured documents is a constant challenge. To secure efficiently banknotes and passports, the use of molecular materials is an exclusive way. The collaboration between the Laboratory of Organometallic for Optics and Oberthur Technologies made possible to develop two new security systems. These securities are based , on one hand, on the use of bipyridine derivatives with colours changing under microwaves, and, on the other hand, on the use of P-type and T-type photochromic compounds with a succession of colours changing under UV-Visible lights irradiation and heating. After a first chapter making an overview of the last innovations in the security field, the last two chapters describe the results obtained on the development of two new secured devices

L'intelligence artificielle basée sur les réseaux de neurones profonds(DNN) est de plus en plus importante dans de multiples domaines d'application, en particulier dans les systèmes critiques où ces algorithmes pourraient être utilisés pour la prise de décision dans des systèmes automatisés voire autonomes. Cependant, pour envisager cette intégration, les réseaux neuronaux ainsi que les composants matériels qui les exécutent doivent répondre à un haut niveau de garanties pour assurer la sécurité des utilisateurs et de l'environnement. L'injection de fautes est une technique largement utilisée pour vérifier et valider un composant qui doit fournir des garanties de sécurité (selon des normes telles que l'ISO 26262).Ce travail se place dans le contexte l'injection de fautes pour les accélérateurs matériels dédiés à l'exécution de réseaux neuronaux.L'objectif est de fournir un formalisme 1) pour raisonner sur la propagation des données dans un accélérateur matériel, et finalement2) pour proposer des campagnes d'injection de fautes précises avec un ensemble limité d'expériences. Nous avons défini une méthodologie basée sur la modélisation formelle de l'architecture matérielle qui identifie les instants et les données vulnérables aux corruptions pendant l'inférence d'un DNN. Cette modélisation permet de tracer dans l'architecture la propagation des corruptions silencieuses des données(SDC) causées par des fautes permanentes de type "stuck-at" ou des fautes transitoires de type "bit-flip". Elle permet également d'identifier les fautes ayant le même effet sur le système, ce qui aide à construire une relation d'équivalence. Les classes d'équivalence de fautes associées sont utilisées pour calculer une métrique de couverture par rapport à une stratégie d'injection de fautes exhaustive. Le modèle proposé permet d'évaluer les stratégies d'injection de fautes en fonction de leur couverture, afin de déterminer si ces stratégies sont capables de tester toutes les défaillances du système qui pourraient entraîner des pannes dangereuses.Un outil appelé FIXME (Flows Inspector X Modelling hardware Errors) a été développé en SCALA pour calculer efficacement des ensembles de fautes ayant un effet équivalent pour une architecture, ainsi que le taux de couverture des stratégies d'injection.Cette méthode est évaluée sur un type d'accélérateurs de réseaux neuronaux appelés "streaming" qui implémente chaque couche d'une topologie de réseau donnée en tant que composant matériel. Les résultats illustrent l'efficacité de la méthode pour identifier précisément les fautes matérielles qui peuvent avoir un effet sur le calcul, et pour calculer efficacement la couverture de n'importe quelle stratégie d'injection de fautes. Cela ouvre la voie à une méthodologie plus avancée pour identifier les composants matériels qui sont cruciaux pour l'exécution d'un réseau de neurones
Artificial intelligence based on deep neural networks (DNN) isbecoming increasingly important in multiple application domains,particularly in critical systems where these algorithms could be usedfor decision-making in automated or even autonomous systems. However,in order to consider this integration, neural networks as well as thehardware components that execute them must meet a high level ofguarantees to ensure the safety of users and the environment. Faultinjection is a widely used technique to verify and validate acomponent that must provide safety guarantees (according to standardssuch as ISO 26262).This work focuses on the context of fault injection for hardwareaccelerators dedicated to the execution of neural networks. Theobjective is to provide a formalism 1) to reason on the datapropagation in a hardware accelerator, and eventually 2) to proposeaccurate fault injection campaigns with a limited set of experiments.We have defined a methodology based on the formal modelling of thehardware that identifies the instants and the data vulnerable tocorruptions during the inference of a DNN. This modelling allows totrace in the architecture the propagation of silent data corruptions(SDC) caused by either permanent stuck-at or transient bit-flipfaults. It also allows to identify faults with the same effect on thesystem which helps construct an equivalence relation. The associatedfault equivalence classes are used to compute a coverage metric w.r.t.an exhaustive fault injection strategy. The proposed model enables theassessment of fault injection strategies based on their coverage, inorder to determine whether these strategies are able to test allsystem malfunctions that may result in dangerous failures.A tool called FIXME (Flows Inspector X Modelling hardware Errors) hasbeen developed in SCALA to efficiently compute sets of faults withequivalent effect for an architecture, as well as the coverage rate ofinjection strategies.This method is evaluated on a type of neural network acceleratorscalled "streaming" which implements each layer of a given networktopology as a hardware component. The results illustrate theeffectiveness of the method in precisely identifying the hardwarefaults that can have an effect on the calculation, and in efficientlycomputing coverage of any fault injection strategy. This paves the wayfor a further methodology to identify the hardware component that arecrucial for a neural network execution

Alors que le droit de la responsabilité connaît une tendance à l’objectivation, il peut paraître incongru d’accorder aux prestataires techniques un régime dit de « responsabilité limitée ». Une telle démarche ne contribue certainement pas à l’objectif affiché par la responsabilité civile depuis la révolution industrielle : l’indemnisation du dommage. Pourtant, ce régime dérogatoire au droit commun trouve toute sa cohérence dès lors qu’il est mis en perspective avec les notions de « convergence », de « neutralité de l’Internet », ou, tout simplement, avec les nombreuses libertés fondamentales dont l’exercice est décuplé sur la toile. Il est, en réalité, une réponse à une autre révolution ; celle du monde des communications dont Internet à bouleverser les fondamentaux. Construit sur une idéologie fondée sur la neutralité, le réseau Internet est certainement devenu l’un des enjeux majeurs de notre société. Il est tant un vecteur de liberté qu’un accélérateur d’innovation dynamisée par les perspectives de relance offerte par la « Net économie ». Toutefois, ces espoirs ne peuvent être satisfaits qu’à la seule condition d’instaurer un climat de confiance. Confiance pour les prestataires de services qui ne peuvent développer leurs modèles d’affaires qu’en ayant une visibilité sur les risques juridiques encourus. Confiance pour les utilisateurs d’Internet qui doivent être rassurés quant à la protection de leurs droits et quant au respect de leurs libertés. La prise en compte de ces impératifs, parfois difficilement conciliables, a abouti à un compromis consistant à faire des prestataires techniques des vecteurs de libertés tout en les obligeant à contribuer à la cessation des contenus illicites. Nouvel Eldorado pour certains, source de tous les maux pour d’autres, la responsabilité limitée accordée aux prestataires techniques par l’intermédiaire de la LCEN est un sujet de controverse. Faut-il permettre à de nouveaux services de bénéficier d’un tel régime ? Le législateur doit-il revoir sa copie et abroger le régime de responsabilité des prestataires techniques ? Faut-il envisager, ainsi que le préconise une partie de la doctrine, une « troisième voie » ? Malgré ces interrogations légitimes, cette étude permettra de faire apparaître que la LCEN est une loi équilibrée qui ne doit ni être revisitée ni interprétée de manière à objectiver la responsabilité des prestataires techniques. Les enjeux en termes de développement de l’économie numérique ainsi que ceux relatifs au respect des libertés fondamentales sont trop importants et justifient le régime de responsabilité limitée des prestataires techniques
Whereas the liability law has a tendency to be objective, it could seem disparate to grant intermediary service providers a limited liability. This approach doesn’t have part in civil liability’s objectives since the industrial revolution: the compensation of harm. Nevertheless, it departs from the ordinary law and seems coherent if it is compared with « convergence » and « the Internet neutrality » notions, or, basically, with the several fundamental liberties used a lot on the Internet. In reality, it is a response to another revolution; those of communications world whose the Internet has disrupted the basics. Developed on an ideology based on neutrality, the Internet network is certainly become one of the main challenges of our society. It promotes liberties and innovation, which is enhanced by the “Net economy”. However, all these hopes can be satisfied on condition that to introduce a confidence atmosphere. A confidence for Internet service providers who are able to develop their business models if they have a visibility concerning the risks. A confidence for the Internet users who have to not be worried about their rights’ protection and liberties’ respect. All of this lead to a compromise that promotes liberties but forces them to be involved in the stopping of unlawful contents. New Eldorado for few people, source of troubles for others, the limited liability granted Internet service providers is a controversial subject. Should we allow any new services to benefit from this liability? Should the legislator abrogate the liability of Internet service providers? Should we consider as the doctrine does a « third way»? In spite of these questions, this study will prove that the LCEN is a balanced law, which doesn’t have to amend. The challenges concerning the development of Net economy as well as the respect of fundamental liberties are essential and justify the limited liability of Internet service providers

Toute la difficulté se résume à déterminer comment le droit prend en compte cette nouvelle technologie de l'edi. Il existe un double phénomène : d'une part, la technique est obligée de prendre en compte le droit, c'est ainsi que l'on a recouru a l'analyse fonctionnelle afin d'etablir la reconnaissance juridique des messages e. D. I. Considérés comme equivalents à un ecrit papier. D'autre part, le droit doit s'adapter à la technique, il adopte alors des règles juridiques issues soit d'un droit déja existant, un droit d'emprunt; soit il crée de nouvelles règles juridiques, un droit créateur. Ainsi s'opère la reconnaissance juridique des e. D. I. Qui constitue la première etape. Une fois établie cette reconnaissance, il convient de doter cette nouvelle technologie d'un régime juridique. Là réside la difficulté de déterminer s'il y a confusion ou distinction entre securite et confidentialité. Nous opterons pour une distinction de fond basée sur la nature juridique du régime juridique de la protection des e. D. I. La securité des edi nous semble dominée par une protection de nature contractuelle alors que la confidentialité des edi s'avere dominée par une protection légale. Il est evident que dans chaque régime, une composante contractuelle ou légale existe mais se revèle insuffisante, defaillante. En effet, si la protection légale de la securité des edi se revèle parcellaire, la protection contractuelle de la confidentialité des edi parait insuffisante. Enfin, une telle protection rencontre bien evidemment des limites : c'est notre troisième etape. Les premières limites sont apportées par le droit de la concurrence et le principe de transparence, les secondes par des principes de puissance publique.

Cette thèse porte sur l'étude de différents aspects de la sécurité des protocoles de vote électronique à distance. Ces protocoles décrivent comment organiser des élections par Internet de manière sécurisée. Ils ont notamment pour but d'apporter des garanties de secret du vote, et de vérifiabilité - ie, il doit être possible de s'assurer que les votes sont correctement comptabilisés. Nos contributions portent sur deux aspects principaux. Premièrement, nous proposons une nouvelle technique d'analyse automatique de propriétés d'équivalence, dans le modèle symbolique. De nombreuses propriétés en lien avec la vie privée s'expriment comme des propriétés d'équivalence, telles que le secret du vote en particulier, mais aussi l'anonymat ou la non-traçabilité. Notre approche repose sur le typage: nous mettons au point un système de typage qui permet d'analyser deux protocoles pour prouver leur équivalence. Nous montrons que notre système de typage est correct, c'est-à-dire qu'il implique effectivement l'équivalence de traces, à la fois pour des nombres bornés et non bornés de sessions. Nous comparons l'implémentation d'un prototype de notre système avec les autres outils existants pour l'équivalence symbolique, sur divers protocoles de la littérature. Cette étude de cas montre que notre procédure est bien plus efficace que la plupart des autres outils - au prix d'une perte de précision (notre outil peut parfois échouer à prouver certaines équivalences). Notre seconde contribution est une étude des définitions du secret du vote et de la vérifiabilité - ou, plus précisément, la vérifiabilité individuelle, une propriété qui requiert que chaque votant soit en mesure de vérifier que son propre vote a bien été pris en compte. Nous prouvons, aussi bien dans les modèles symboliques que calculatoire, que le secret du vote implique la vérifiabilité individuelle, alors même que l'intuition et des résultats voisins déjà établis semblaient indiquer que ces deux propriétés s'opposent. Notre étude met également en évidence une limitation des définitions existantes du secret du vote par jeux cryptographiques : elles supposent une urne honnête, et par conséquent expriment des garanties significativement plus faibles que celles que les protocoles visent à assurer. Nous proposons donc une nouvelle définition (par jeu) du secret du vote, contre une urne malhonnête. Nous relions notre définition à une notion de secret du vote par simulation, pour montrer qu'elle apporte des garanties fortes. Enfin, nous menons une étude de cas sur plusieurs systèmes de vote existants
In this thesis we study several aspects of the security of remote electronic voting protocols. Such protocols describe how to securely organise elections over the Internet. They notably aim to guarantee vote privacy - ie, votes must remain secret -and verifiability - it must be possible to check that votes are correctly counted. Our contributions are on two aspects. First, we propose a new approach to automatically prove equivalence properties in the symbolic model. Many privacy properties can be expressed as equivalence properties, such as in particular vote privacy, but also anonymity or unlinkability. Our approach relies on typing: we design a type system that can typecheck two protocols to prove their equivalence. We show that our type system %, together with some additional conditions on the messages exchanged by the protocols, soundly implies trace equivalence, both for bounded and unbounded numbers of sessions. We compare a prototype implementation of our typechecker with other existing tools for symbolic equivalence, on a variety of protocols from the literature. This case study shows that our procedure is much more efficient than most other tools - at the price of losing precision (our tool may fail to prove some equivalences). Our second contribution is a study of the definitions of privacy and verifiability - more precisely, individual verifiability, a property that requires each voter to be able to check that their own vote is counted. We prove that, both in symbolic and computational models, privacy implies individual verifiability, contrary to intuition and related previous results that seem to indicate that these two properties are opposed. Our study also highlights a limitation of existing game-based definitions of privacy: they assume the ballot box is trusted, which makes for significantly weaker guarantees than what protocols aim for. Hence we propose a new game-based definition for vote privacy against a dishonest ballot box. We relate our definition to a simulation-based notion of privacy, to show that it provides meaningful guarantees, and conduct a case study on several voting schemes

La sécurité informatique, aussi connue comme la cyber-sécurité, est toujours un sujet d'actualité dans la recherche en sciences informatiques. Comme les cyber-attaques grandissent de plus en plus en volume et en sophistication, la protection des systèmes ou réseaux d'information devient une tâche difficile. Les chercheurs dans la communauté de recherche prêtent une attention constante à la sécurité, en particulier ils s'orientent vers deux directions principales: (i) - la conception des infrastructures sécurisées avec des protocoles de communication sécurisés et (ii) - surveillance / supervision des systèmes ou des réseaux afin de trouver et de remédier des vulnérabilités. La dernière vérifie que tout ce qui a été conçu dans la première fonctionne correctement et en toute sécurité, ainsi détectant les violations de sécurité. Ceci étant le sujet principal de cette thèse.Cette dissertation présente un cadre de surveillance de la sécurité en tenant en compte des différents types de jeu de données d'audit y compris le trafic de réseaux et les messages échangés dans les applications. Nous proposons également des approches innovantes fondées sur l'apprentissage statistique, la théorie de l'information et de l'apprentissage automatique pour prétraiter et analyser l'entrée de données. Notre cadre est validé dans une large gamme des études de cas, y compris la surveillance des réseaux traditionnels TCP / IP (v4) (LAN, WAN, la surveillance de l'Internet), la supervision des réseaux de objets connectés utilisant la technologie 6LoWPAN (IPv6), et également, l’analyse des logs d'autres applications. Enfin, nous fournissons une étude sur la tolérance d’intrusion par conception et proposons une approche basée sur l’émulation pour détecter et tolérer l’intrusion simultanément.Dans chaque étude de cas, nous décrivons comment nous collectons les jeux de données d'audit, extrayons les attributs pertinents, traitons les données reçues et décodons leur signification de sécurité. Pour attendre ces objectifs, l'outil MMT est utilisé comme le cœur de notre approche. Nous évaluons également la performance de la solution et sa possibilité de marcher dans les systèmes “à plus grande échelle” avec des jeux de données plus volumineux
Computer security, also known as cyber-security or IT security, is always an emerging topic in computer science research. Because cyber attacks are growing in both volume and sophistication, protecting information systems or networks becomes a difficult task. Therefore, researchers in research community give an ongoing attention in security including two main directions: (i)-designing secured infrastructures with secured communication protocols and (ii)-monitoring/supervising the systems or networks in order to find and re-mediate vulnerabilities. The former assists the later by forming some additional monitoring-supporting modules. Whilst, the later verifies whether everything designed in the former is correctly and securely functioning as well as detecting security violations. This is the main topic of this thesis.This dissertation presents a security monitoring framework that takes into consideration different types of audit dataset including network traffic and application logs. We propose also some novel approaches based on supervised machine learning to pre-process and analyze the data input. Our framework is validated in a wide range of case studies including traditional TCP/IPv4 network monitoring (LAN, WAN, Internet monitoring), IoT/WSN using 6LoWPAN technology (IPv6), and other applications' logs. Last but not least, we provide a study regarding intrusion tolerance by design and propose an emulation-based approach to simultaneously detect and tolerate intrusion.In each case study, we describe how we collect the audit dataset, extract the relevant attributes, handle received data and decode their security meaning. For these goals, the tool Montimage Monitoring Tool (MMT) is used as the core of our approach. We assess also the solution's performance and its possibility to work in "larger scale" systems with more voluminous dataset

La généralisation de transactions commerciales et des services sur des supports non-sécurisés a rendu nécessaire l'utilisation de protocoles permettant de garantir aux participants la confidentialité des données aussi bien que l'identification des correspondants. De nombreux protocoles proposés se sont révélés incorrects. Leur importance économique a motivé l'introduction de méthodes formelle pour la détection d'erreurs. Dans cette thèse, nous nous intéressons aux problèmes liés à l'analyse automatique de ces protocoles. Nous donnons une sémantique opérationnelle aux spécifications de haut niveau habituellement utilisées, étendons le cadre standard de l'analyse pour prendre en compte les propriétés des opérateurs algébriques pour la recherche de failles et considérons le problème de la vérification de protocoles. Nous réduisons ces problèmes à des problèmes d'accessibilité pour des systèmes de transitions définis par des règles de réécriture sur des ensembles. Cette réduction permet de donner la complexité de ces problèmes, et est une première étape vers une résolution par des outils entièrement automatiques
Commercial transactions and services over insecure networks have lead to the use of security protocols. These protocols ought to provide both data confidentiality and participants authentication, but many of those proposed up to date have turned out to be flawed. Their economical importance has motivated the introduction of formal verification. In this dissertation, we investigate the problems raised by the automatic analysis of such protocols. We give an operationnal semantics to high-level protocol specifications, extend the standard Dolev-Yao framework to algebraic operators and finally consider the problem of protocol verification. We reduce these problems to reachability problems. This reduction is a first steptoward the implementation of an automatic analysis tool

Dans une transaction type de m-commerce (commerce mobile), un client mobile se connecte à un serveur marchand pour effectuer des achats. La sécurisation de ces transactions est une tâche indispensable puisqu'elles transmettent des données sensibles, telles que les coordonnées bancaires des clients. De ce fait, le développement du marché du m-commerce s'avère être étroitement lié au niveau de sécurité offert par les réseaux qui les véhiculent. Cette thèse se propose d'étudier les besoins de sécurité, puis d'offrir des schémas de sécurité appropriés pour les applications de m-commerce, et ce dans différents contextes de propagation. Dans les premiers travaux de la thèse, nous nous sommes intéressés au contexte du m-commerce sur le WAP1. X. Nous avons ainsi proposé le protocole WSET pour sécuriser le paiement du m-commerce sur le WAP1. X. Ce protocole est inspiré des protocoles SET et WTLS, et permet de contourner la faille du “WAP Gap”, ainsi qu'une nouvelle faille identifiée, celle du “marchand malhonnête”. WSET offre la sécurité de bout en bout des coordonnées bancaires entre le client et la passerelle de paiement. Nous nous sommes ensuite focalisés sur le déploiement de l'application d'enchères sur les réseaux adhoc. Ce nouveau type de WLAN représente en effet un support de déploiement attrayant pour cette application de par les nouvelles possibilités qu'il offre (absence d'infrastructure, rapidité et faible coût de déploiement, ubiquité et auto-gestion). Cependant, ces réseaux de nature radio présentent plusieurs vulnérabilités. Pour que le déploiement des enchères sur les réseaux ad hoc soit possible, nous nous sommes penchés d'abord sur la sécurisation du réseau ad hoc support. Un schéma de sécurité distribué et auto-géré a alors été défini pour le protocole de routage OLSR régissant le réseau ad hoc. Ce schéma assure l'intégrité des messages de contrôle tout en respectant les caractéristiques des réseaux ad hoc. Enfin, une architecture d'un modèle d'enchères déployé sur les réseaux ad hoc a été spécifiée. Ce modèle original permet la mise en place spontanée d'une application d'enchères n'importe où et n'importe quand, respectant ainsi les caractéristiques de leur réseau de déploiement. A ce modèle d'enchères, nous avons ensuite introduit des schémas répondant à ses besoins fondamentaux : l'intégrité des mises et l'équité de l'enchérissement. Nous avons proposé un algorithme de sécurité distribué, basé sur les techniques de la cryptographie à seuil, et assurant l'intégrité des offres. La considération de l'équité, ainsi que des paramètres du réseau de déploiement, a enfin permis de calculer la durée des tours théorique et nécessaire à l'équité de l'enchérissement
In a typical m-commerce (mobile commerce) transaction, a mobile client connects to a merchant server in order to carry out purchases. Securing these transactions is a fundamental task since they transmit critical data, such as the client credit card number. Therefore, the development of the m-commerce becomes closely related to the security level offered by their networks support. This thesis aims to study the security requirements, and then to offer suitable securing schemes to m-commerce applications conducted in various contexts of propagation. In the first works, we have focused on the context of m-commerce over WAP1. X. We have then proposed a protocol, WSET, securing the m-commerce payment over the WAP1. X mobile networks. This protocol is inspired from the SET and WTLS protocols, and avoids two security flaws: the well known “WAP Gap” flaw; and a new identified security flaw which we have named the “the dishonest merchant”. WSET offers an end to end security to the payment data between the client and the payment gateway. In the following works, we have focused on the deployment of auctions over ad hoc networks. In fact, this new kind of WLAN represents an attractive deployment support for this application, due to the new possibilities that it offers (absence of infrastructure, rapidity and low cost of deployment, ubiquity, and self-management). However, these radio networks present many vulnerabilities. .

Cette thèse porte sur l'étude de différents aspects de la sécurité des protocoles de vote électronique à distance. Ces protocoles décrivent comment organiser des élections par Internet de manière sécurisée. Ils ont notamment pour but d'apporter des garanties de secret du vote, et de vérifiabilité - ie, il doit être possible de s'assurer que les votes sont correctement comptabilisés. Nos contributions portent sur deux aspects principaux. Premièrement, nous proposons une nouvelle technique d'analyse automatique de propriétés d'équivalence, dans le modèle symbolique. De nombreuses propriétés en lien avec la vie privée s'expriment comme des propriétés d'équivalence, telles que le secret du vote en particulier, mais aussi l'anonymat ou la non-traçabilité. Notre approche repose sur le typage: nous mettons au point un système de typage qui permet d'analyser deux protocoles pour prouver leur équivalence. Nous montrons que notre système de typage est correct, c'est-à-dire qu'il implique effectivement l'équivalence de traces, à la fois pour des nombres bornés et non bornés de sessions. Nous comparons l'implémentation d'un prototype de notre système avec les autres outils existants pour l'équivalence symbolique, sur divers protocoles de la littérature. Cette étude de cas montre que notre procédure est bien plus efficace que la plupart des autres outils - au prix d'une perte de précision (notre outil peut parfois échouer à prouver certaines équivalences). Notre seconde contribution est une étude des définitions du secret du vote et de la vérifiabilité - ou, plus précisément, la vérifiabilité individuelle, une propriété qui requiert que chaque votant soit en mesure de vérifier que son propre vote a bien été pris en compte. Nous prouvons, aussi bien dans les modèles symboliques que calculatoire, que le secret du vote implique la vérifiabilité individuelle, alors même que l'intuition et des résultats voisins déjà établis semblaient indiquer que ces deux propriétés s'opposent. Notre étude met également en évidence une limitation des définitions existantes du secret du vote par jeux cryptographiques : elles supposent une urne honnête, et par conséquent expriment des garanties significativement plus faibles que celles que les protocoles visent à assurer. Nous proposons donc une nouvelle définition (par jeu) du secret du vote, contre une urne malhonnête. Nous relions notre définition à une notion de secret du vote par simulation, pour montrer qu'elle apporte des garanties fortes. Enfin, nous menons une étude de cas sur plusieurs systèmes de vote existants
In this thesis we study several aspects of the security of remote electronic voting protocols. Such protocols describe how to securely organise elections over the Internet. They notably aim to guarantee vote privacy - ie, votes must remain secret -and verifiability - it must be possible to check that votes are correctly counted. Our contributions are on two aspects. First, we propose a new approach to automatically prove equivalence properties in the symbolic model. Many privacy properties can be expressed as equivalence properties, such as in particular vote privacy, but also anonymity or unlinkability. Our approach relies on typing: we design a type system that can typecheck two protocols to prove their equivalence. We show that our type system %, together with some additional conditions on the messages exchanged by the protocols, soundly implies trace equivalence, both for bounded and unbounded numbers of sessions. We compare a prototype implementation of our typechecker with other existing tools for symbolic equivalence, on a variety of protocols from the literature. This case study shows that our procedure is much more efficient than most other tools - at the price of losing precision (our tool may fail to prove some equivalences). Our second contribution is a study of the definitions of privacy and verifiability - more precisely, individual verifiability, a property that requires each voter to be able to check that their own vote is counted. We prove that, both in symbolic and computational models, privacy implies individual verifiability, contrary to intuition and related previous results that seem to indicate that these two properties are opposed. Our study also highlights a limitation of existing game-based definitions of privacy: they assume the ballot box is trusted, which makes for significantly weaker guarantees than what protocols aim for. Hence we propose a new game-based definition for vote privacy against a dishonest ballot box. We relate our definition to a simulation-based notion of privacy, to show that it provides meaningful guarantees, and conduct a case study on several voting schemes

Le vote est un outil central au bon fonctionnement de toute démocratie. Malgré son utilisation lors d'élections à grands enjeux, le vote électronique n'apporte pas encore le même niveau de sécurité que le vote papier. En particulier, des menaces déjà existantes telles que la coercition et l'achat de vote risquent de gagner en ampleur et d'impacter les résultats.Au cours de cette thèse, nous étudions les solutions académiques permettant de faire face à ces phénomènes, à savoir les notions de coercion-resistance et de receipt-freeness.Sur ces sujets, nous identifions des limites des définitions existantes et proposons de nouvelles définitions permettant de modéliser de plus larges scénarios d'attaque.En plus de ces améliorations théoriques et pratiques, nous proposons des stratégies efficaces pour éliminer certains risques, comme les attaques à l'italienne et l'achat de vote. Pour cela, nous développons une boîte à outils reposant sur des primitives dites de multi-party computation, qui permettent à différents participants d'évaluer une fonction sur des données chiffrées. Cela nous permet de proposer de nouvelles méthodes de dépouillement offrant une propriété de tally-hiding, qui contrecarre les attaques à l'italienne. Ces méthodes peuvent notamment s'appliquer à d'autres types de scrutin que le vote uninominal, comme par exemple le vote préférentiel.Pour ce qui concerne l'achat de vote, une autre contribution de cette thèse est de généraliser la notion de receipt-freeness afin qu'elle réponde davantage à ce risque, comparée aux notions existantes. Nous proposons par ailleurs une solution modulaire qui permet de réaliser cette notion de receipt-freeness, et donc de mettre à mal les stratégies d'achat de vote. Cette solution s'appuie sur de nouvelles primitives de chiffrement, appelées traceable encryptions
Voting is a central tool for the proper functioning of any democracy. Despite its use in high-stakes elections, electronic voting does not yet provide the same level of security as paper voting. In particular, existing threats such as coercion and vote buying may increase and impact the results.In this thesis, we study academic solutions to address these phenomena, namely the notions of coercion-resistance and receipt-freeness.On these topics, we identify some limitations on the existing definitions and propose new definitions to model more attack scenarios.Besides these theoretical contributions, we propose practical strategies to eliminate certain risks, such as Italian attacks and vote buying. To this end, we develop a toolbox based on multi-party computation primitives, which allow different participants to evaluate a function on encrypted data. This leads to new methods for computing the tally, which counter Italian attacks thanks to the tally-hiding property. These methods can be applied to other types of voting than uninominal voting, such as preferential voting.With respect to vote buying, another contribution of this thesis is to generalize the notion of receipt-freeness so that it is more relateed to this threat, compared to existing notions. We also propose a modular solution that realizes this notion of receipt-freeness, and thus defeat vote buying. This solution relies on new encryption primitives, called traceable encryptions

Cette thèse a pour objet d'étude le paradigme de la gestion des identités numériques entre organisations. L'accent est porté sur l'usager, consommateur de services hébergés par des organisations dans un environnement ouvert. Le terme "environnement ouvert" résume l'idée d'un environnement où il ne peut exister d'autorité centrale régissant toutes les mises en relation entre entités qui le peuplent, ni tous les accès que ces dernières requièrent. Ainsi, dans un tel environnement, diverses entités, potentiellement inconnues, ont à établir des relations qui visent, dans ces travaux, à satisfaire les conditions de contrôle d'accès des fournisseurs de services et à donner à l'usager des moyens de contrôle et de confiance envers les organisations. Le WEB au travers de l'Internet est une implémentation qui constitue un tel environnement. L'emploi de tiers de confiance et leur potentielle croissance au sein d'un tel environnement sont des propositions argumentées. En effet, les certificats numériques sont une réalisation technologique qui permet la diffusion d'informations certifiées issues de tiers de confiance, et les échanges d'informations certifiées entre usagers et organisations sont une réponse aux deux objectifs précédents. Cela suppose donc le déploiement d'une architecture globale d'échanges de certificats. La thèse repose sur un modèle de négociation de confiance permettant l'établissement graduel d'une relation de confiance, potentiellement entre inconnus, reposant sur des tiers de confiance et intégrant l'idée d'une diffusion d'information maîtrisée. Il est alors justifié que les échanges de certificats sont une implémentation pertinente de ce concept. La réalisation d'une possible architecture, à l'échelle globale, implique de nombreuses problématiques, dont les principales sont décrites et étudiées. Cette architecture suppose notamment des échanges entre tiers de confiance et organisations au sujet des usagers, ce qui représente une menace potentielle pesant sur le respect de la vie privée des usagers. L'enrichissement de l'environnement des usagers est identifié comme une condition au déploiement d'une architecture permettant d'adresser cette problématique. À cette fin, il est étudié l'emploi d'un schéma de signature permettant de bâtir des certificats offrant la non-associativité des transactions de génération et de présentation, la présentation sélective de contenu, les preuves de possessions et les preuves de propriétés sur le contenu. Ces propriétés permettent notamment de réaliser le statut d'anonymat au sens de la non-associativité. Le statut d'anonymat des interlocuteurs au sein des négociations de confiance et les problématiques que ce statut engendre sont alors étudiés. Des négociations conduites par l'usager impliquent des problématiques d'ergonomie et d'utilisabilité. Un outil de gestion des identités numériques mis à disposition des usagers est une première réponse. Une interface graphique de l'agent de négociation pour l'usager est décrite à cette fin. Les notions d'automatisation des négociations de confiance sont introduites dans le but de proposer une solution complémentaire permettant d'assister l'utilisateur. Le modèle est au départ relativement "dissymétrique", phénomène accentué par une vision centrée sur l'utilisateur faisant de l'usager le chef d'orchestre de la diffusion de ses informations. Puis, au travers d'une étude sur l'universalité d'un agent de négociation, ce modèle est affiné pour aboutir à la description d'un agent de négociation s'adaptant autant à l'environnement utilisateur comme outil de gestion des identités numériques, qu'à celui des organisations employé à des fins de contrôle d'accès aux applications. %Cela nous conduit à étudier les problématiques d'intégration d'un tel agent avec les applications existantes, notamment au regard du concept de couche pervasive de gestion des identités. L'idée de l'universalité d'un tel agent implique l'étude des problématiques d'interopérabilité et de standardisation, incluant le besoin d'espaces de noms communs et de protocoles interopérables. Il est pour cela présenté une mise en oeuvre des certificats anonymes basée sur la diffusion publique de méta-données des générateurs ayant aboutie à l'élaboration d'un schéma de données XML baptisé x23. Enfin, le concept d' "identité en tout lieu" et l'emploi de ce travail dans les environnements informatiques pervasifs et ubiquitaires sont discutés.

La sécurité informatique, aussi connue comme la cyber-sécurité, est toujours un sujet d'actualité dans la recherche en sciences informatiques. Comme les cyber-attaques grandissent de plus en plus en volume et en sophistication, la protection des systèmes ou réseaux d'information devient une tâche difficile. Les chercheurs dans la communauté de recherche prêtent une attention constante à la sécurité, en particulier ils s'orientent vers deux directions principales: (i) - la conception des infrastructures sécurisées avec des protocoles de communication sécurisés et (ii) - surveillance / supervision des systèmes ou des réseaux afin de trouver et de remédier des vulnérabilités. La dernière vérifie que tout ce qui a été conçu dans la première fonctionne correctement et en toute sécurité, ainsi détectant les violations de sécurité. Ceci étant le sujet principal de cette thèse.Cette dissertation présente un cadre de surveillance de la sécurité en tenant en compte des différents types de jeu de données d'audit y compris le trafic de réseaux et les messages échangés dans les applications. Nous proposons également des approches innovantes fondées sur l'apprentissage statistique, la théorie de l'information et de l'apprentissage automatique pour prétraiter et analyser l'entrée de données. Notre cadre est validé dans une large gamme des études de cas, y compris la surveillance des réseaux traditionnels TCP / IP (v4) (LAN, WAN, la surveillance de l'Internet), la supervision des réseaux de objets connectés utilisant la technologie 6LoWPAN (IPv6), et également, l’analyse des logs d'autres applications. Enfin, nous fournissons une étude sur la tolérance d’intrusion par conception et proposons une approche basée sur l’émulation pour détecter et tolérer l’intrusion simultanément.Dans chaque étude de cas, nous décrivons comment nous collectons les jeux de données d'audit, extrayons les attributs pertinents, traitons les données reçues et décodons leur signification de sécurité. Pour attendre ces objectifs, l'outil MMT est utilisé comme le cœur de notre approche. Nous évaluons également la performance de la solution et sa possibilité de marcher dans les systèmes “à plus grande échelle” avec des jeux de données plus volumineux
Computer security, also known as cyber-security or IT security, is always an emerging topic in computer science research. Because cyber attacks are growing in both volume and sophistication, protecting information systems or networks becomes a difficult task. Therefore, researchers in research community give an ongoing attention in security including two main directions: (i)-designing secured infrastructures with secured communication protocols and (ii)-monitoring/supervising the systems or networks in order to find and re-mediate vulnerabilities. The former assists the later by forming some additional monitoring-supporting modules. Whilst, the later verifies whether everything designed in the former is correctly and securely functioning as well as detecting security violations. This is the main topic of this thesis.This dissertation presents a security monitoring framework that takes into consideration different types of audit dataset including network traffic and application logs. We propose also some novel approaches based on supervised machine learning to pre-process and analyze the data input. Our framework is validated in a wide range of case studies including traditional TCP/IPv4 network monitoring (LAN, WAN, Internet monitoring), IoT/WSN using 6LoWPAN technology (IPv6), and other applications' logs. Last but not least, we provide a study regarding intrusion tolerance by design and propose an emulation-based approach to simultaneously detect and tolerate intrusion.In each case study, we describe how we collect the audit dataset, extract the relevant attributes, handle received data and decode their security meaning. For these goals, the tool Montimage Monitoring Tool (MMT) is used as the core of our approach. We assess also the solution's performance and its possibility to work in "larger scale" systems with more voluminous dataset

Ce travail étudie le principal conflit d’Internet et les changements générés par l’affrontement entre les réseaux de file sharing et les détenteurs des droits de propriété intellectuelle. Les tentatives d’opposition de ce phénomène sont en fait porteuses d’une transformation radicale de la gouvernance d’Internet, dans le cadre de laquelle l’approche normative s’affaiblit à l’avantage du contrôle technologique. Notre recherche se développe comme une analyse des débats juridiques et technologiques américains, visant à illustrer les lignes de développement de la théorie critique et de l’appareil normatif construit en réponse aux pratiques de partage. La première partie est donc consacrée à la définition de l’exception numérique, c’est-à-dire à la naissance d’Internet comme espace de communication non commercial, et à la fondation de la critique d’Internet après la privatisation des infrastructures, coïncidant avec la naissance de la cyberlaw. La seconde partie illustre l’évolution du débat critique, à travers la légitimation du tournant technologique du copyright et le rapprochement du cyberdroit américain et du discours technologique, développés dans le contexte des débats des ingénieurs sur l’internet enhancement et le trusted system. La troisième partie, pour conclure, aborde l’histoire technologique et judiciaire des réseaux de file sharing, proposant une définition sociologique de la pratique à travers une confrontation avec les interprétations économiques (disruptive technology) et anthropologiques (hi-tech gift economy) produites par la littérature en argument
This work is about the main Internet conflict and maine changes generated by the struggles between file sharing networks and copyright owners. Governance attemps to nullify peer-to-peer networks dramatically change regulation philosophy wherein legislative approach is weakened in favour of technological control. This research is developped as an analysis of juridical and technological debates in U. S. A. , with the goal of represent the developments of both critical theory and norms building as an answer of share practices. Its first part is dedicated to the definition of digital exception, that is Internet birth as a free and non commercial space, and to the foundation of Internet criticism after privatization of infrastructures, that coincide with cyberlaw emergence. Its second part represents critical debate evolution, across legitimation of technological turn of copyright law and incoming of American cyberlaw towards technological approach of «Internet enhancement» and «trusted system» debates. Finally, its third part deals with the judicial and technological history of file sharing networks, in the goal of suggesting a sociological definition of these practises, by compared economics (disruptive tecnology) and anthropological (hi-tech gift economy) interpretations produced by literature about this argument

Les Systèmes de Transport Intelligents Coopératifs (C-ITS) représentent une approche avancée dans le transport moderne. Ces systèmes exploitent les technologies de communication, telles que ETSI ITS-G5 et Cellular Vehicle-to-Everything (C-V2X), pour améliorer la sécurité routière et le flux de trafic. Au cœur des C-ITS se trouve le concept de perception coopérative, une caractéristique transformatrice qui permet aux Véhicules Coopératifs et Autonomes (CAVs) et aux unités d'infrastructure routière de partager et d'analyser collectivement les données de divers capteurs, y compris les caméras, le lidar et le radar. Cette coopération est facilitée par l'échange de Messages de Perception Coopérative (CPM), qui fournissent une description des objets routiers détectés, via des réseaux de communication. L'objectif principal est d'améliorer la conscience environnementale des CAVs, en particulier dans des scénarios complexes comme les conditions d’obstructions. Cependant, plusieurs défis surviennent avec l'augmentation du volume de données généré par les CAVs et les capteurs d'infrastructure. Ces défis incluent mais ne se limitent pas à :- Surcharge de Données dans les Réseaux de Communication : Le volume croissant de données générées par les capteurs embarqués conduit à des réseaux de communication congestionnés. Cette congestion peut retarder ou empêcher la transmission d'informations cruciales dans les CPMs, empêchant les CAVs de recevoir des informations pertinentes, qui peuvent être essentielles pour une navigation sûre et une opération efficace.- Méthodes Inefficaces de Contrôle de la Congestion et d'Allocation des Ressources : Les méthodes actuelles du contrôle de la congestion et d'allocation des ressources peuvent ne pas gérer efficacement le volume élevé de trafic de données dans les réseaux C-ITS. Ces méthodes échouent souvent à considérer la criticité de certains scénarios contextuels de données qui peuvent conduire à une utilisation sous-optimale des ressources réseau. Cette inefficacité peut entraîner que les informations de perception soient dépriorisées ou perdues, affectant davantage la capacité des CAVs à percevoir et répondre précisément à leurs environnements de conduite.Cette thèse, intitulée « Résilience de la Perception Coopérative et Augmentée des Véhicules Autonomes Connectés par C-ITS », se concentre sur les défis d'amélioration de la résilience et de la qualité des systèmes de perception coopérative et augmentée des CAVs. Elle propose des mécanismes robustes pour aborder les problèmes clés à travers deux contributions principales. La première, intitulée « Stratégies de Perception Coopérative et Augmentée Intelligentes pour les CAVs à travers des Techniques d'Apprentissage par Renforcement », se concentre sur le développement de stratégies intelligentes utilisant l'apprentissage par renforcement pour optimiser la perception coopérative des CAVs. Les méthodes proposées dans le cadre de cette contribution permettent aux CAVs d’adapter continuellement leur partage de données à l’état actuelle de l’environnement, améliorant ainsi la sécurité et l'efficacité dans diverses conditions de conduite. La deuxième contribution, « Allocation de Ressources Adaptative pour une Perception Coopérative et Augmentée Optimisée des CAVs », aborde la gestion des ressources dans les systèmes C-ITS. Elle propose une allocation adaptative des ressources de communication dans le réseau ITS-G5, optimisant l'échange d'informations entre les CAVs et l'infrastructure routière. Cette approche vise à réduire la congestion du canna et assurer une perception environnementale fiable et en temps réel pour les CAVs, contribuant ainsi à la résilience et à la qualité améliorées des systèmes de perception coopérative et augmentée
Cooperative Intelligent Transport Systems (C-ITS) represent an advanced approach in modern transportation. They leverage communication technologies, such as ETSI ITS-G5 and Cellular Vehicle-to-Everything (C-V2X), to enhance road safety and traffic flow. Central to C-ITS is the concept of cooperative perception, a transformative feature that enables Cooperative and Autonomous Vehicles (CAVs) and roadside infrastructure units to share and collectively analyze data from various sensors, including cameras, lidar, and radar. This cooperation is facilitated through the exchange of Cooperative Perception Messages (CPM), which provide a high-level description of detected road objects, via communication networks. The primary objective is to enhance the environmental awareness of CAVs, especially in complex scenarios like non-line-of-sight conditions. However, several challenges arise with the increasing volume of data generated by CAVs and infrastructure sensors. These challenges includes but not limited to:- Data Overloads in Communication Networks: The growing volume of data generated by onboard sensors leads to congested communication networks. This congestion can delay or prevent the transmission of crucial information in CPMs, impairing CAVs’ from receiving timely and relevant information, which may be essential for safe navigation and efficient operation.- Inefficient Congestion Control and Resource Allocation Methods: Current methods may not effectively manage the high volume of data traffic in C-ITS networks. They often fail to consider the criticality of certain data contextual scenarios that can lead to suboptimal utilization of network resources. This inefficiency can result in perception information being deprioritized or lost, further affecting the CAVs ability to accurately perceive and respond to their driving environments.This thesis, titled « Resilience of Cooperative and Augmented Perception of Autonomous Vehicles Connected by C-ITS, » focuses on the challenges of improving the resilience and quality of cooperative and augmented perception systems for CAVs. It proposes robust mechanisms to address key issues through two main contributions. The first, titled « Intelligent Cooperative and Augmented Perception Strategies for CAVs through Reinforcement Learning Techniques, » focuses on the development of intelligent strategies using reinforcement learning to optimize the cooperative perception of CAVs. These strategies allow CAVs to continuously adapt their data sharing to the current state of the environment, thus improving safety and efficiency in various driving conditions. The second contribution, « Adaptive Resource Allocation for Optimized Cooperative and Augmented Perception of CAVs, » addresses resource management in C-ITS systems. It proposes an adaptive allocation of communication resources in the ITS-G5 network, optimizing the exchange of information between CAVs and roadside infrastructure. These methods aim to reduce channel congestion and ensure reliable and real-time perception for CAVs, thus contributing to the improved resilience and quality of cooperative and augmented perception systems

Les méthodes formelles ont fait leurs preuves dans l’étude des protocoles de sécurité et plusieurs outils existent, permettant d’automatiser ces vérifications. Hélas, ils se montrent parfois dans l’incapacité d’analyser certains protocoles, à cause des primitives cryptographiques employées ou des propriétés que l’on cherche à démontrer. On étudie deux systèmes existants: un protocole de vote par internet Norvégien et un protocole pour les votes en réunion du CNRS. Nous analysons les garanties de sécurité qu’ils proposent, dans différents scénarios de corruption. Malgré les résultats réutilisables obtenus, ces preuves démontrent également la difficulté de les effectuer à la main. Une nouvelle piste dans l’automatisation de telles preuves pourrait alors venir des systèmes de types. Basés sur le développement récent d’un système de types permettant de traiter des propriétés d’équivalence, nous l’avons utilisé afin de démontrer des propriétés comme l’anonymat du vote. Nous avons appliqué cette méthode Helios, un système de vote par internet bien connu. Il existe une autre famille de protocoles de sécurité : les APIs. Ces interfaces permettent l’utilisation d’informations stockées dans des dispositifs sécurisés sans qu’il soit normalement possible de les en ex- traire. Des travaux récents montrent que ces interfaces sont également vulnérables. Cette thèse présente un nouveau design d’API, incluant une fonctionnalité de révocation, rarement présente dans les solutions existantes. Nous démontrons, par une analyse formelle, qu’aucune combinaison de commandes ne permet de faire fuir des clefs sensées rester secrètes, même si l’adversaire parvient à en brute-forcer certaines
Formal methods have been used to analyze security protocols and several tools have even been developed to tackle automatically different proof techniques and ease the verification of such protocols. However, for electronic voting and APIs, current tools tend to reach their limits because they can’t handle some cryptographic primitives, or the security properties, involved in those protocols. We work on two cases studies of existing and deployed systems: a Norwegian e-voting protocol and a CNRS boardroom voting protocol. We analyze them using the applied pi-calculus model and we discuss in details about their security properties, in different corruption scenarios. Even including several reusable results, these proofs are complex and, therefore, expose a real need for automation. Thus, we focus on a possible lead in direction of this needed automation: type-systems. We build upon a recent work describing a new type-system designed to deal with equivalence properties, in order to apply this on the verification of equivalence-based properties in electronic voting like ballot-secrecy. We present an application of this method through Helios, a well-known e-voting system. Another family of advanced security protocols are APIs: secure interfaces devoted to allow access to some information stored into a secured trusted hardware without leaking it outside. Recet work seems to show that these interfaces are also vulnerable. In this thesis, we provide a new design for APIs, including revocation. In addition, we include a formal analysis of this API showing that a malicious combination of API’s commands does not leak any key, even when the adversary may brute-force some of them

La transposition de la directive relative aux services de paiement du 13 novembre2007 en droit français est à l’origine de la création d’une nouvelle catégorie d’acteurs bancaires : l’établissement de paiement. La fourniture de services de paiement cesse ainsi d’être du domaine exclusif des établissements de crédit pour devenir l’activité principale des établissements de paiement. S’il est vrai que cette nouvelle répartition des activités bancaires ébranle le monopole bancaire, elle n’y met cependant pas fin. Pour une meilleure lisibilité et un contrôle plus efficace des acteurs, il est proposé une mutation du système bancaire grâce à d’une part une scission complète des activités bancaires, et d’autre part une indépendance des établissements de paiement face aux établissements de crédit. La sécurisation du marché des paiements dépend également de l’encadrement des opérations de paiement. La préservation de la confiance du consommateur est essentielle au bon fonctionnement du marché des services de paiement
The transposition into French law of the Payment Services Directive of 13November 2007 led to the creation of a new category of players in the banking sector: the payment institution. The provision of payment services is no longer the sole domain of credit institutions but becomes the main activity of payment institutions. Although this new distribution of banking activities undermines thebanking monopoly, it does not terminate it. For a better legibility of the bankingsystem and a more efficient control of banking institutions, it is proposed amutation of the banking system through on the one hand, a complete separation of banking activities, and on the other hand payment institutions independence from credit institutions. Securing the payments services market also depends on the supervision of payment transactions. Preserving consumer’s trust is essential to awell-functioning payment services market

Les méthodes formelles ont fait leurs preuves dans l’étude des protocoles de sécurité et plusieurs outils existent, permettant d’automatiser ces vérifications. Hélas, ils se montrent parfois dans l’incapacité d’analyser certains protocoles, à cause des primitives cryptographiques employées ou des propriétés que l’on cherche à démontrer. On étudie deux systèmes existants: un protocole de vote par internet Norvégien et un protocole pour les votes en réunion du CNRS. Nous analysons les garanties de sécurité qu’ils proposent, dans différents scénarios de corruption. Malgré les résultats réutilisables obtenus, ces preuves démontrent également la difficulté de les effectuer à la main. Une nouvelle piste dans l’automatisation de telles preuves pourrait alors venir des systèmes de types. Basés sur le développement récent d’un système de types permettant de traiter des propriétés d’équivalence, nous l’avons utilisé afin de démontrer des propriétés comme l’anonymat du vote. Nous avons appliqué cette méthode Helios, un système de vote par internet bien connu. Il existe une autre famille de protocoles de sécurité : les APIs. Ces interfaces permettent l’utilisation d’informations stockées dans des dispositifs sécurisés sans qu’il soit normalement possible de les en ex- traire. Des travaux récents montrent que ces interfaces sont également vulnérables. Cette thèse présente un nouveau design d’API, incluant une fonctionnalité de révocation, rarement présente dans les solutions existantes. Nous démontrons, par une analyse formelle, qu’aucune combinaison de commandes ne permet de faire fuir des clefs sensées rester secrètes, même si l’adversaire parvient à en brute-forcer certaines
Formal methods have been used to analyze security protocols and several tools have even been developed to tackle automatically different proof techniques and ease the verification of such protocols. However, for electronic voting and APIs, current tools tend to reach their limits because they can’t handle some cryptographic primitives, or the security properties, involved in those protocols. We work on two cases studies of existing and deployed systems: a Norwegian e-voting protocol and a CNRS boardroom voting protocol. We analyze them using the applied pi-calculus model and we discuss in details about their security properties, in different corruption scenarios. Even including several reusable results, these proofs are complex and, therefore, expose a real need for automation. Thus, we focus on a possible lead in direction of this needed automation: type-systems. We build upon a recent work describing a new type-system designed to deal with equivalence properties, in order to apply this on the verification of equivalence-based properties in electronic voting like ballot-secrecy. We present an application of this method through Helios, a well-known e-voting system. Another family of advanced security protocols are APIs: secure interfaces devoted to allow access to some information stored into a secured trusted hardware without leaking it outside. Recet work seems to show that these interfaces are also vulnerable. In this thesis, we provide a new design for APIs, including revocation. In addition, we include a formal analysis of this API showing that a malicious combination of API’s commands does not leak any key, even when the adversary may brute-force some of them

Chaque jour, une guerre invisible pour les données se déroule entre les sites de commerce électronique et les acteurs qui,en siphonnent les données, sont appelés "scrapers'' . Les sites de commerce électronique détiennent les données au cœur du conflit et souhaitent les fournir uniquement aux utilisateurs légitimes. Les scrapers veulent un accès illimité et continu aux données susmentionnées pour en tirer profit. Pour atteindre cet objectif, les scrapers envoient de grandes quantités de requêtes aux sites de commerce électronique, ce qui leur cause des problèmes financiers. Cela a conduit l'industrie de la sécurité à s'engager dans une course aux armements contre les scrapers afin de créer de meilleurs systèmes pour détecter et contrer leurs activités. À l'heure actuelle, la bataille se poursuit, mais les scrapers semblent avoir le dessus, notamment grâce à leur utilisation de Proxies IP Résidentiels (RESIPs). Dans cette thèse, nous visons à rééquilibrer la balance des forces en introduisant de nouvelles techniques de détection et d'atténuation qui surmontent les limitations des méthodes actuelles. Nous proposons une technique inspirée des "pots de miel'' qui piège les scrapers en leur faisant croire qu'ils ont obtenu les données visées tandis qu'ils reçoivent des informations modifiées. Nous présentons deux nouvelles techniques de détection basées sur des mesures de réseau qui identifient les requêtes émanant de scrapers cachés derrière les infrastructures RESIP. À travers un partenariat en cours avec Amadeus IT Group, nous validons nos résultats en utilisant des données opérationnelles réelles. Conscients que les scrapers ne cesseront pas de chercher de nouvelles façons d'éviter la détection et l'atténuation, nous offrons des contributions qui peuvent aider à élaborer les prochaines armes défensives pour lutter contre les scrapers. Nous proposons une caractérisation complète des RESIPs, la plus puissante arme actuellement à la disposition des scrapers. De plus, nous examinons la possibilité d'acquérir des renseignements sur les menaces liées aux scrapers en les géolocalisant lorsqu'ils envoient des demandes via un RESIP
Every day an invisible war for data takes place between e-commerce websites and web scrapers. E-commerce websites own the data at the heart of the conflict and would like to provide it only to genuine users. Web scrapers aim to have illimited and continuous access to the above-mentioned data to capitalize on it. To achieve this goal, scrapers send large amounts of requests to e-commerce websites, causing them financial problems. This led the security industry to engage in an arms race against scrapers to create better systems to detect and mitigate their requests. At present, the battle continues, but scrapers appear to have the upper hand, thanks to the usage of Residential IP Proxies (RESIPs). In this thesis, we aim to shift the balance by introducing novel detection and mitigation techniques that overcome the limitations of current state-of-the-art methods. We propose a deceptive mitigation technique that lures scrapers into believing they have obtained their target data while they receive modified information. We present two new detection techniques based on network measurements that identify scraping requests proxied through RESIPs. Thanks to an ongoing collaboration with Amadeus IT Group, we validate our results on real-world operational data. Being aware that scrapers will not stop looking for new ways to avoid detection and mitigation, this thesis provides additional contributions that can help in building the next defensive weapons for fighting scrapers. We propose a comprehensive characterization of RESIPs, the strongest weapon currently at the disposal of scrapers. Moreover, we investigate the possibility of acquiring threat intelligence on the scrapers by geolocating them when they send requests through a RESIP

L’objectif de ce travail de thèse est le développement de techniques de détection d’intrusions et de corrélation d’alertes spécifiques aux systèmes de contrôle industriels (ICS). Cet intérêt est justifié par l’émergence de menaces informatiques visant les ICS, et la nécessité de détecter des attaques ciblées dont le but est de violer les spécifications sur le comportement correct du processus physique.Dans la première partie de nos travaux, nous nous sommes intéressés à l’inférence automatique de spécifications pour les systèmes de contrôle séquentiels et ce à des fins de détection d’intrusions. La particularité des systèmes séquentiels réside dans leur logique de contrôle opérant par étapes discrètes. La détection d’intrusions au sein de ces systèmes a été peu étudiée malgré leur omniprésence dans plusieurs domaines d’application. Dans notre approche, nous avons adopté le formalisme de la logique temporelle linéaire (LTL) et métrique (MTL) permettant de représenter des propriétés temporelles d’ordre qualitatif et quantitatif sur l’état des actionneurs et des capteurs. Un algorithme d’inférence de propriétés a été développé afin d’automatiser la génération des propriétés à partir de motifs de spécifications couvrant les contraintes les plus communes. Cette approche vise à pallier le nombre conséquent de propriétés redondantes inférées par les approches actuelles.Dans la deuxième partie de nos travaux, nous cherchons à combiner l’approche de détection d’intrusions développée dans le premier axe avec des approches de détection d’intrusions classiques. Pour ce faire, nous explorons une approche de corrélation tenant compte des spécificités des systèmes industriels en deux points: (i) l’enrichissement et le prétraitement d’alertes venant de domaines différents (cyber et physique), et (ii) la mise au point d’une politique de sélection d’alertes tenant compte du contexte d’exécution du processus physique. Le premier point part du constat que, dans un système industriel, les alertes qui sont remontées au corrélateur sont caractérisées par des attributs hétérogènes (attributs propres aux domaines cyber et physique). Cependant, les approches de corrélation classiques présupposent une certaine homogénéité entre les alertes. Afin d’y remédier, nous développons une approche d’enrichissement des alertes du domaine physique par des attributs du domaine cyber sur la base d’informations relatives aux protocoles supportés par les contrôleurs et à la distribution des variables du processus au sein des contrôleurs. Le deuxième point concerne le développement d’une politique de sélection d’alertes qui adapte dynamiquement les fenêtres de sélection des alertes selon l’évolution des sous-processus.Les résultats de l’évaluation de nos approches de détection et de corrélation montrent des performances améliorées sur la base de métriques telles que le nombre de propriétés inférées, le taux de réduction des alertes et la complétude des corrélations
The objective of this thesis is to develop intrusion detection and alert correlation techniques geared towards industrial control systems (ICS). Our interest is driven by the recent surge in cybersecurity incidents targeting ICS, and the necessity to detect targeted attacks which induce incorrect behavior at the level of the physical process.In the first part of this work, we develop an approach to automatically infer specifications over the sequential behavior of ICS. In particular, we rely on specification language formalisms such as linear temporal logic (LTL) and metric temporal logic (MTL) to express temporal properties over the state of the actuators and sensors. We develop an algorithm to automatically infer specifications from a set of specification patterns covering the most recurring properties. In particular, our approach aims at reducing the number of redundant and unfalsifiable properties generated by the existing approaches. To do so, we add a pre-selection stage which allows to restrict the search for valid properties over non redundant portions of the execution traces. We evaluate our approach on a complex physical process steered by several controllers under process oriented attacks. Our results show that a significant reduction in the number of inferred properties is possible while achieving high detection rates.In the second part of this work, we attempt to combine the physical domain intrusion detection approach developed in the first part with more classical cyber domain intrusion detection approaches. In particular, we develop an alert correlation approach which takes into account some specificities of ICS. First, we explore an alert enrichment approach that allows to map physical domain alerts into the cyber domain. This is motivated by the observation that alertscoming from different domains are characterized by heterogeneous attributes which makes any direct comparison of the alerts difficult. Instead, we enrich the physical domain alerts with cyber domain attributes given knowledge about the protocols supported by the controllers and the memory mapping of process variables within the controllers.In this work, we also explore ICS-specific alert selection policies. An alert selection policy defines which alerts will be selected for comparison by the correlator. Classical approaches often rely on sliding, fixed size, temporal windows as a basis for their selection policy. Instead, we argue that given the complex interdependencies between physical subprocesses, agreeing on analert window size is challenging. Instead, we adopt selection policies that adapt to the state of the physical process by dynamically adjusting the size of the alert windows given the state of the subprocesses within the physical process. Our evaluation results show that our correlator achieves better correlation metrics in comparison with classical temporal based approaches

Dans les systèmes d'informations, les outils de détection produisent en continu un grand nombre d'alertes.Des outils de corrélation permettent de réduire le nombre d'alertes et de synthétiser au sein de méta-alertes les informations importantes pour les administrateurs.Cependant, la complexité des règles de corrélation rend difficile leur écriture et leur maintenance.Cette thèse propose par conséquent une méthode pour générer des règles de corrélation de manière semi-automatique à partir d’un scénario d’attaque exprimé dans un langage de niveau d'abstraction élevé.La méthode repose sur la construction et l'utilisation d’une base de connaissances contenant une modélisation des éléments essentiels du système d’information (par exemple les nœuds et le déploiement des outils de détection). Le procédé de génération des règles de corrélation est composé de différentes étapes qui permettent de transformer progressivement un arbre d'attaque en règles de corrélation.Nous avons évalué ce travail en deux temps. D'une part, nous avons déroulé la méthode dans le cadre d'un cas d'utilisation mettant en jeu un réseau représentatif d'un système d'une petite entreprise.D'autre part, nous avons mesuré l'influence de fautes touchant la base de connaissances sur les règles de corrélation générées et sur la qualité de la détection
Information systems produce continuously a large amount of messages and alerts. In order to manage this amount of data, correlation system are introduced to reduce the alerts number and produce high-level meta-alerts with relevant information for the administrators. However, it is usually difficult to write complete and correct correlation rules and to maintain them. This thesis describes a method to create correlation rules from an attack scenario specified in a high-level language. This method relies on a specific knowledge base that includes relevant information on the system such as nodes or the deployment of sensor. This process is composed of different steps that iteratively transform an attack tree into a correlation rule. The assessment of this work is divided in two aspects. First, we apply the method int the context of a use-case involving a small business system. The second aspect covers the influence of a faulty knowledge base on the generated rules and on the detection

La stabilité et le développement des nations dépendent grandement de leurs Infrastructures Critiques (IC). Vu leur importance, de nombreuses menaces guettent leurs systèmes d’information - aussi appelés Infrastructures d’Information Critiques (IIC) -, parmi elles: les atteintes à l’intégrité de leurs données et processus informatisés ainsi que les abus pouvant survenir au cours des collaborations avec d’autres parties. L’intégrité d’une information, qui est sa propriété de ne pas être altérée, est primordiale pour les IIC puisqu’elles manipulent et génèrent des informations devant nécessairement être correctes et fiables. Dans un contexte de mondialisation et d’ouverture, les IC ne peuvent évoluer sans collaborer avec leur environnement. Toutefois, cela n’est pas sans risques puisque les ressources qu’elles engagent peuvent faire l’objet de corruptions et de sabotages. Tentant de réduire les risques de corruptions pouvant émaner de l’intérieur comme de l’extérieur, nous avons œuvré à l’amélioration du mécanisme de contrôle d’accès. Incontournable, il vise à limiter les actions auxquelles peuvent prétendre les utilisateurs légitimes du système, conformément à la politique de sécurité de l’organisation. La pertinence et la finesse de cette dernière impacte grandement l’efficacité du mécanisme. Ainsi, les modèles de contrôle d’accès sont utilisés pour faciliter l’expression et l’administration desdites politiques. OrBAC est un modèle riche et dynamique, satisfaisant plusieurs besoins des IIC, en revanche il reste limité quant à la prise en charge de l’intégrité, aussi bien en contexte localisé que distribué. Ainsi, nous avons proposé une extension d’OrBAC pour les environnements localisés, Integrity-OrBAC (I-OrBAC), qui tient compte de contraintes réelles liées à l’intégrité pour statuer sur les requêtes d’accès. I-OrBAC intègre des paramètres issus de l’application de méthodes d’analyse de risques pour refléter les besoins des ressources passives et apprécier, à leur juste valeur, les habilitations des sujets. Cela nous a orientés vers une modélisation en multi-niveaux d’intégrité qui favorisera la priorisation des biens sensibles, comme la stipule les programmes de protection des IC. Dans I-OrBAC, les niveaux d’intégrité servent aussi bien à contraindre l’attribution des privilèges qu’à la rendre plus flexible : ces niveaux restreignent les accès pour garantir que seuls les utilisateurs chevronnés accèdent aux ressources sensibles, mais permettent aussi aux sujets de différents rôles de réaliser une même tâche, étant bien sûr assujettis à des niveaux seuils différents. Pour rendre I-OrBAC proactif - non limité à statuer uniquement sur les requêtes d’accès - nous avons proposé un algorithme qui vise à déterminer le sujet le plus adéquat, parmi les rôles prioritaires, pour la réalisation d’une tâche sans attendre que les sujets n’en fassent la requête. L’algorithme est décrit par un système d’inférence pour faciliter sa compréhension tout en favorisant la conduite de raisonnements logiques et la dérivation de conclusions. Nous avons proposé une implémentation de notre modèle dans le cadre d’une étude de cas tirée du projet européen FP7 CRUTIAL relatif aux réseaux de transport et de distribution d’électricité. Finalement, pour pallier les problèmes issus des collaborations, nous avons fait appel aux contrats électroniques pour étendre I-OrBAC aux environnements distribués - l’extension Distributed IOrBAC (DI-OrBAC). Ces pactes servent non seulement à définir le contexte, les clauses ainsi que les activités à réaliser mais aussi à prévenir l’occurrence de litiges et à les résoudre. Toutefois, nous avons dû concevoir des mécanismes adaptés à notre modèle I-OrBAC pour leur négociation et leur application.

Dans cette thèse, je propose trois contributions principales : dans notre première contribution, nous étudions l'architecture d'identité WebRTC et plus particulièrement son intégration aux algorithmes de délégation d'authentification existants. Cette intégration n'a pas encore été étudiée jusqu'à présent. Dans cette perspective, nous implémentons les composants de l'architecture d'identité WebRTC ce qui nous permet de montrer que cette architecture n'est pas particulièrement adaptée à une intégration aux protocoles de délégation d'authentification existants tels qu'OpenID Connect. Pour répondre à RQ1, nous montrons ensuite comment la position centrale des fournisseurs d'identité dans l'écosystème du Web est renforcée par leur intégration à l'établissement de session WebRTC, posant ainsi un risque supplémentaire contre la discrétion des utilisateurs. Dans l'écosystème Web, la norme est l'architecture des services en silo dont les utilisateurs sont captifs. C'est en particulier le cas des systèmes de délégation d'authentification, pour lesquels la plupart du temps, il n'est pas possible de choisir son fournisseur d'identité. Afin de répondre à RQ3, nous réalisons une étude afin de déterminer pour quelles raisons les utilisateurs ne peuvent pas choisir leur fournisseur d'identité sur Web. Notre étude montre que bien que ce choix soit possible en théorie, l'absence d'implémentation de certains standards par les sites webs et les fournisseurs d'identité empêche ce choix en pratique. Dans notre seconde contribution, nous cherchons à donner plus de contrôle à l'utilisateur. Pour ce faire et en réponse à RQ2, nous proposons une extension de la spécification WebRTC afin de permettre la négociation des paramètres d'identité. Un prototype d'implémentation est proposé afin de valider notre proposition. Cette implémentation révèle certaines limites dues à l'API d'identité WebRTC empêchant notamment d'obtenir un retour sur le niveau d'authentification de l'autre utilisateur ainsi que l'impossibilité de changer de fournisseur d'identité en cours de session. Nous proposons ensuite une API Web permettant aux utilisateurs de choisir leur fournisseur d'identité lors d'une authentification sur un site tiers via une interface de sélection d'identité contrôlée par le navigateur. Répondant à RQ3, notre API repose sur une réutilisation de l'architecture d'identité WebRTC dans un scénario client-serveur. Nous présentons une implémentation de notre solution, basée sur une extension du navigateur Firefox, afin d'en démontrer l'utilisabilité. Nos résultats montrent qu'à long terme, l'adoption de cette API pourrait réduire la charge d'implémentation pour les développeurs de sites Web et permettre aux utilisateurs de préserver leur discrétion en choisissant des fournisseurs d'identité de confiance
In this thesis, we propose three main contributions : In our first contribution we study the WebRTC identity architecture and more particularly its integration with existing authentication delegation protocols. This integration has not been studied yet. To fill this gap, we implement components of the WebRTC identity architecture and comment on the issues encountered in the process. In order to answer RQ1, we then study this specification from a privacy perspective an identify new privacy considerations related to the central position of identity provider. In the Web, the norm is the silo architecture of which users are captive. This is even more true of authentication delegation systems where most of the time it is not possible to freely choose an identity provider. In order to answer RQ3, we conduct a survey on the top 500 websites according to Alexa.com to identify the reasons why can't users choose their identity provider. Our results show that while the choice of an identity provider is possible in theory, the lack of implementation of existing standards by websites and identity providers prevent users to make this choice. In our second contribution, we aim at giving more control to users. To this end and in order to answer RQ2, we extend the WebRTC specification to allow identity parameters negotiation. We present a prototype implementation of our proposition to validate it. It reveals some limits due to the WebRTC API, in particular preventing to get feedback on the other peer's authentication strength. We then propose a web API allowing users to choose their identity provider in order to authenticate on a third-party website, answering RQ2. Our API reuse components of the WebRTC identity architecture in a client-server authentication scenario. Again, we validate our proposition by presenting a prototype implementation of our API based on a Firefox extension. Finally, in our third contribution, we look back on RQ1 and propose a trust and security model of a WebRTC session. Our proposed model integrates in a single metric the security parameters used in the session establishment, the encryption parameters for the media streams, and trust in actors of the communication setup as defined by the user. Our model objective is to help non-expert users to better understand the security of their WebRTC session. To validate our approach, we conduct a preliminary study on the comprehension of our model by non-expert users. This study is based on a web survey offering users to interact with a dynamic implementation of our model

Les applications Machine-to-Machine (M2M) fournissent plus de confort aux utilisateurs et permettent une utilisation optimale des ressources. Toutefois, ces applications ne présentent pas que des avantages. Ces dernières peuvent engendrer des problèmes de sécurité, voire porter atteinte à la vie privée de leurs utilisateurs. Dans cette thèse, nous nous intéressons à la sécurité des applications M2M, et plus précisément à l'authentification et la préservation de la vie privée d'utilisateurs d'équipements M2M dotés d'une carte SIM. Dans une première partie, nous proposons cinq nouvelles primitives cryptographiques, à savoir un schéma de signature partiellement aveugle, deux schémas de codes d'authentification de messages, ainsi que deux schémas d'attestations anonymes. Ces nouvelles primitives sont plus efficaces, voire fournissent des fonctionnalités nouvelles par rapport aux schémas de l'état de l'art et sont adaptées aux environnements limités en ressources telles que les cartes SIMs. En nous appuyant sur ces primitives, nous construisons de nouveaux protocoles préservant la vie privée des utilisateurs. Plus précisément, nous introduisons un nouveau système de paiement anonyme efficace. Nous proposons également un protocole d’authentification et d’identification anonyme pour la nouvelle génération de cartes SIMs connue sous le nom d'Embedded SIM. Par ailleurs, nous construisons un système d'accréditations anonymes. Enfin, nous spécifions un système de vote électronique efficace rendant inutile toute forme de coercition à l'encontre d'un électeur. La sécurité de toutes nos contributions est prouvée dans le modèle de l'oracle aléatoire sous des hypothèses classiques
Machine to Machine (M2M) applications enable a better management of resources and provide users With greater cornfort. Unfortunately, they also entail serious security and privacy concerns. ln this thesis, we focus on M2M security, and particularly on the authentication and privacy issues of M2M applications involving a SIM card. ln the first part, we design five new cryptographic primitives and formally prove that they meet the expected security requirements. More precisely, they consist of a partially blind signature scheme, a sequential aggregate Message Authentication Codes (MAC) scheme, an algebraic MAC scheme and two pre-Direct Anonymous Attestation (pre-DAA) schemes. Some of the proposed schemes aim to achieve a particular property that was not provided by previous constructions whereas others intend to improve the efficiency of state-of-the-art schemes. Our five schemes do not require the userls device to compute pairings. Thus, they are suitable for resource constrained environments such as SIM cards. ln a second part, we rely on these primitives to propose new privacy-preserving protocols. More specifically, we design an efficient private eCash system. We also propose a protocol enabling anonymous authentication and identification of embedded SIMs (eSlMs). Furthermore, we rely on our algebraic MAC scheme to build a practical Keyed-Verification Anonymous Credentials (KVAC) system. Finally, based on our sequential aggregate MAC scheme, we introduce a remote electronic voting system that is coercion-resistant and practical for real polls. The security of our protocols is formally proven in the Random Oracle Model (ROM) under classical computational assumptions

De nos jours, l’e-commerce est devenu un écosystème complexe où de multiples solutions (en termes de plateforme) sont possibles et réalisables pour un e-commerçant. En parallèle, un nouveau paradigme a fait son apparition, celui du Cloud Computing. Malgré les avantages certains qu’il apporte, peu des plateformes existantes sont pensées pour fonctionner sur une architecture Cloud. De plus, face à la complexité d’obtenir une plateforme d’e-commerce (PE) sécurisée, flexible et évolutive s’appuyant sur des applications et services hétérogènes existants et répondant aux besoins des e-commerçants, il est légitime de se demander si une PE basée sur le Cloud permettrait de réellement simplifier les difficultés rencontrées par les e-commerçants. Cette thèse propose de valider la pertinence de l’utilisation du Cloud dans un contexte d’e-commerce avant de proposer les principes architecturaux d’une PE ouverte, évolutive et sécurisée basée sur une architecture de Cloud. De plus, la mise en œuvre d’une PE par un e-commerçant, n’est pas orientée utilisateur. Face à ceci, nous proposons un mécanisme orienté utilisateur simplifiant la mise en œuvre d’une PE tout en assurant un haut degré de sécurité au sein de celle-ci. Enfin, nous nous sommes également intéressés à répondre à la question suivante dans un contexte d’e-commerce : Comment assurer qu’aucune inférence d’activités sur une taille constatée d’une BD ne puisse être réalisée par des entités non autorisées ? Pour y répondre, nous proposons une solution de sécurité de dissimulation de données orientée utilisateur permettant de résoudre la propriété de confidentialité forte des données au sein des SGBDR
Nowadays, e-commerce has become a complex ecosystem where multiple solutions (in terms of platforms) are possible and feasible for e-merchant. Concurrently, a new paradigm called Cloud Computing has emerged. Despite some advantages it brings, few of these platforms have been designed to operate on a Cloud architecture. Thus, because of the complexity to design a flexible and scalable e-commerce platform (EP), based on existing heterogeneous applications/services and fulfilling the needs of e-merchants, it is legitimate to ask ourself if a PE based on the Cloud would really simplify the difficulties faced by e-merchants. This thesis aims to validate the relevance of using the Cloud Computing in the e-commerce context and propose the architectural principles of an open, scalable and secure EP based on a Cloud architecture. In addition, the EP used by e-merchants are not user-centric EP. As a consequence, we propose a user-centric mechanism simplifying the design and implementation of an EP while ensuring a high security level. Finally, we tried to answer the following question: How to ensure that no activity inference on a database size, in an e-commerce context, can be achieved by unauthorized entities? As a response, we propose a user-centric security solution of data concealment to resolve the property of strong data confidentiality within relational database management system (RDBMS)

Les codes correcteurs d'erreurs sont utilisés pour reconstituer les données numériques, qui sont sujettes à des altérations lors de leur stockage et de leur transport. Il s'agit là de l'utilisation principale des codes correcteurs mais ils peuvent encore être employés en cryptographie. Ils sont dans ce contexte un outil permettant, entre autres choses, de chiffrer des données et d'authentifier des personnes. Ces différents aspects sont traités dans ce document. Pour commencer, nous étudions la classe de codes cycliques possédant un ensemble de définition de la forme {1, 2^i+1, 2^j+1}, où i et j désignent des entiers positifs distincts. Nous concentrons notre attention sur la caractérisation des codes trois-correcteurs appartenant à cette classe ainsi que sur la distribution de poids de ces codes. Nous améliorons l'algorithme de Schaub, qui donne une minoration de la distance minimale des codes cycliques. Nous mettons en oeuvre cet algorithme pour calculer l'immunité spectrale de fonctions booléennes. Cette quantité est reliée à la distance minimale de codes cycliques et est importante pour garantir la sécurité dans certains cryptosystèmes de chiffrement à flot. Dans un second temps, nous proposons une solution pour accélérer le calcul des racines de polynômes dans des corps finis de caractéristique deux. Ce calcul est la phase la plus lente du déchiffrement des cryptosystèmes de type McEliece basés sur les codes de Goppa binaires classiques. Nous fournissons une analyse de la complexité de l'algorithme sous-jacent baptisé BTZ. Nous achevons nos travaux par une étude des protocoles d'authentification à bas coût, dérivés du protocole HB, en adoptant une approche basée sur le problème du décodage par syndrome, plutôt que par l'approche standard, fondée sur le problème LPN.

Dans la nécessité de développer des véhicules sûrs, confortables, économiques et à faible impact environnemental, les voitures sont de plus en plus équipées d'organes qui emploient des capteurs, actionneurs et systèmes de commande automatiques.Or ces systèmes, critiques pour la sécurité et le confort des passagers, peuvent mal-fonctionner en présence d'une défaillance (défaut).Dans le cadre du diagnostic à bord, plusieurs approches à base de modèle sont développées dans ce travail afin de détecter, localiser et estimer un défaut capteur ou actionneur, et pour détecter la perte de stabilité du véhicule.Ces méthodes reposent sur une synthèse robuste pour les systèmes incertains à commutation.Elles sont validées en simulation avec le logiciel CarSim, et sur les données réelles de véhicule dans le cadre du projet INOVE
Modern vehicles are increasingly equipped with new mechanisms to improve safety, comfort and ecological impact. These active systems employ sensors, actuators and automatic control systems. However, in case of failure of one these components, the consequences for the vehicle and the passengers safety could be dramatic. In order to ensure a higher level of reliability within on board diagnosis, new methodologies for sensor or actuator fault detection, location and estimation are proposed. These model based approaches are extended for robust synthesis for switched uncertain systems. In addition, a method for detecting critical stability situation is presented. The validation of the different methods is illustrated with simulations using CarSim, and application on real vehicle data within the INOVE project

L'établissement de la confiance est un problème qui se pose en permanence dans la vie quotidienne. Nous avons toujours besoin d'évaluer la confiance que l'on a en quelqu'un avant de décider d'entreprendre une action avec. Il s'agit bien évidemment d'une question très importante pour les applications de l'Internet où il est de plus en plus rare d'engager une transaction avec des personnes ou des entités que l'on connaîtrait au préalable. La confiance est un élément clé pour le développement et le bon fonctionnement des applications d'e-commerce et par extension de tous les services qui amènent à des interactions avec des inconnus.Le but de cette thèse est de proposer une infrastructure de gestion de la confiance qui permette à chaque participant d'exprimer sa propre politique de confiance ; politique qui guidera le comportement des applications qui fournissent ou qui permettent d'accéder à des services. Cette infrastructure met en œuvre des mécanismes de négociation qui vont permettre d'établir une confiance mutuelle entre les différents participants d'une transaction. Un des points importants de notre proposition est d'offrir un langage d'expression des politiques qui permet d'utiliser toutes les sources d'informations disponibles telles que les qualifications (credentials), la notion de réputation, de recommandation, de risque pour exprimersa politique de confiance.