Dans les environnements pervasifs, le constant changement du contexte d'utilisation des applications et des services distribués (i.e., des ressources) impose de nouvelles exigences pour la définition des solutions de contrôle d'accès. Celles-ci concernait notamment la sensibilité au contexte et la mise en œuvre distribuée des politiques d'accès. Pour prendre en compte ces besoins, nous proposons une famille de modèles de contrôle d'accès, appelé CxtBAC (Context-Based Access Control), qui se compose de huit modèles conceptuels et permet d'explorer les informations contextuelles caractérisant les entités suivantes : le propriétaire de la ressource, l'environnement, l'utilisateur et la ressource elle-même. Contrairement aux propositions existantes, basées sur le modèle RBAC (Role-Based Access Control), la famille de modèle proposé est centrée sur la notion de contexte et non de rôle. Par conséquent, les décisions d'accès aux ressources protégées sont prises en considérant les informations contextuelles qui caractérisent la situation des entités impliquées. Pour décrire les règles d'accès, les permissions sont associées à des contextes d'accès et les utilisateurs sont associés dynamiquement à ces dernières. Les modèles proposés sont indépendants du langage de spécification de la politique de sécurité. Dans le cadre de cette thèse, nous proposons une solution pour la mise en ?uvre basée sur un formalisme d'ontologies.

La sécurité est un élément crucial dans le développement d'un système d'information. On ne peut pas concevoir un système bancaire sans préoccupation sécuritaire. La sensibilité des données d'un système hospitalier nécessite que la sécurité soit la composante majeure d'un tel logiciel. Le contrôle d'accès est un des nombreux aspects de la sécurité. Il permet de définir les conditions de l'exécution d'actions dans un système par un utilisateur. Entre les différentes phases de conception d'une politique de contrôle d'accès et son application effective sur un système déployé, de nombreuses étapes peuvent introduire des erreurs ou des failles non souhaitables. L'utilisation de méthodes formelles est une réponse à ces préoccupations dans le cadre de la modélisation de politiques de contrôle d'accès. L'algèbre de processus EB3 permet une modélisation formelle de systèmes d'information. Son extension EB3SEC a été conçue pour la spécification de politiques de contrôle d'accès. Le langage ASTD, combinaison des statecharts de Harel et des opérateurs de EB3, permet de modéliser graphiquement et formellement un système d'information. Cependant, ces deux méthodes manquent d'outils de vérification et de validation qui permettent de prouver ou de vérifier des propriétés de sécurité indispensables à la validation de politiques de contrôle d'accès. De plus, il est important de pouvoir prouver que l'implémentation d'une politique correspond bien à sa spécification abstraite. Cette thèse définit des règles de traduction de EB3 vers ASTD, d'ASTD vers event-B et vers B. Elle décrit également une architecture formelle exprimée en B d'un filtre de contrôle d'accès pour les systèmes d'information. Cette modélisation en B permet de prouver des propriétés à l'aide du prouveur B ou de vérifier des propriétés avec ProB, un vérificateur de modèles. Enfin, une stratégie de raffinement B pour obtenir une implémentation de ce filtre de contrôle d'accès est présentée. Les raffinements B étant prouvés, l'implémentation correspond donc au modèle initial de la politique de contrôle d'accès

Au fil des années, la technologie sans contact NFC s'est imposée dans notre quotidien au travers des différents services proposés. Les cas d'utilisation sont nombreux allant des cartes de fidélité, des cartes de transport, des cartes de paiement sans contact jusqu'aux cartes de contrôle d'accès. Cependant, les premières générations des cartes NFC ont une sécurité minimale reposant sur l'hypothèse de leur non-clonabilité. De multiples vulnérabilités ont été découvertes et leur exploitation a permis des copies frauduleuses. Afin de remédier à ces vulnérabilités, une nouvelle génération de cartes à la sécurité augmentée a vu le jour. Ces cartes permettent une authentification avec un lecteur basée sur des algorithmes de chiffrements symétriques tels qu'AES, DES, et 3DES. Elles sont plus robustes que la première génération mais ont subi des également une attaque en reverse-engineering. Pour garantir et améliorer le niveau de sécurité du système de contrôle d'accès, nous proposons dans le cadre de l'opération neOCampus, la dématérialisation sécurisée de la carte sans contact sur un smartphone muni de la technologie NFC. Cette dématérialisation nous permet d'exploiter la puissance de calcul et la capacité de stockage du smartphone afin de déployer des algorithmes d'authentification plus robustes. Cependant, l'OS du smartphone ne peut être considéré comme un environnement de confiance. Afin de répondre à la problématique du stockage et du traitement sécurisés sur un smartphone, plusieurs solutions ont été proposées : les Secure Elements (SE), les Trusted Platform Module (TPM), les Trusted Execution Environment (TEE) et la virtualisation. Afin de stocker et de traiter de manière sécurisée les données d'authentification, le TEE apparait comme la solution idéale avec le meilleur compromis sécurité/performances. Cependant, de nombreux smartphones n'embarquent pas encore de TEE. Pour remédier à cette contrainte, nous proposons une architecture basée sur l'utilisation de TEEs déportés sur le Cloud. Le smartphone peut le contacter via une liaison Wi-Fi ou 4G. Pour se faire, un protocole d'authentification basé sur IBAKE est proposé. En plus de ce scénario nominal, deux autres scenarii complémentaires ont été proposés permettant d'accompagner le développement et la démocratisation des TEE non seulement dans le monde des smartphones mais aussi sur des dispositifs peu onéreux comme le Raspberry Pi 3. Ces architectures déploient le même algorithme d'authentification que le scénario nominal. Nous proposons aussi une architecture hors ligne permettant à un utilisateur de s'authentifier à l'aide d'un jeton de connexion en cas d'absence de réseaux sans fil. Cette solution permet de relâcher la contrainte sur la connectivité du smartphone à son Cloud. Nous procédons à une évaluation de l'architecture de dématérialisation et de l'algorithme d'authentification en terme de performances et de sécurité. Les opérations cryptographiques du protocole d'authentification sont les plus coûteuses. Nous avons alors procédé à leur évaluation en nous intéressant en particulier aux opérations de chiffrement IBE et à la génération de challenges ECC. Nos implémentations ont été évaluées pour l'infrastructure Cloud et l'environnement mobile. Nous avons ensuite procédé à une validation du protocole d'authentification sur les trois architectures sélectionnées à l'aide de l'outil Scyther. Nous avons montré, que pour les trois scenarii, la clé de session négociée via le protocole d'authentification restait secrète durant tout le protocole. Cette caractéristique nous garantit que les données d'authentification chiffrées avec cette clé resteront secrètes et que la phase d'identification de la personne est protégée tout en préservant l'ergonomie du système existant. / Over the years, the Near Field Communication technology has emerged in our daily lives through a variety of services. There are several use cases for contactless cards : loyalty cards, metro and bus cards, payment cards and access control cards. However, the first version of these cards has a low security level that is based on the assumption that the cards can not be cloned. To address this issue, a new version of NFC cards has been developed. It allows an authentication with the NFC reader through symmetric encryption algorithms such as AES, DES or 3DES. These cards are more robust that the previous ones. However, these cards have also undergone a reverseengineering attack. We propose, in the context of the neOCampus project, to replace the contactless cards with a smartphone equipped with the NFC capabilities. This process, called dematerialization, allows us to take advantage of the computational power and the storage capabilities of the smartphone to deploy more complex and robust authentication algorithms. However, the OS of the smartphone can not be considered as a trusted environment for the storage and the processing of sensitive data. To address these issues, several solutions were proposed : Secure Elements (SE), Trusted Platform Module (TPM), Trusted Execution Environment (TEE) and Virtualization. In order to store and process securely authentication data, the TEE seems to be the best trade-off between security and performances. Nevertheless, many smartphones do not embeed TEE and it is necessary to negotiate agreements with the TEE manufacturers in order to deploy a secure application on it. In order to figure out these issues, we propose to set up an architecture with a TEE in the Cloud. The smartphone has a secure Cloud that can be reached through a Wi-Fi or 4G connection. The reader has also its own secure Cloud reachable with an Ethernet link. An authentication protocol based on IBAKE is also proposed. In addition to this scenario, two other scenarios were proposed to follow the development and democratization of the TEE on the smartphones and on some inexpensive devices such as Raspberry Pi 3. These alternative architectures deploy the same authentication protocol as the main scenario. We propose an offline architecture allowing a user to authenticate using a connection token. This solution relaxes the connectivity constraint between the smartphone and its secure Cloud. We perform an evaluation of our architecture and of the authentication algorithm in terms of performances and security. The cryptographical operations of the authentication protocol are the most consuming operations in term of performance. We have chosen to target these operations especially the encryption with the IBE and the ECC challenges generation. Our implementations have been evaluated for a Cloud infrastructure and a mobile-like environment. We also perform a formal verification of the authentication protocol through the three considered architectures with Scyther. We showed that, for the three scenarios, that the session key negotiated through the authentication protocol remains secret during the overall execution of the protocol. These characteristic guarantee that the authentication data encrypted with this key will remain secret and that this step of the algorithm will be secure while preserving the ergonomy of the existing system.

La thèse présente les résultats de recherche sur une méthode de contrôle distribué et coordonné pour la régulation des accès autoroutiers. Le trafic autoroutier est représenté par le modèle Cell Transmission Model (CTM). L'objectif de contrôle principal est de d'obtenir une distribution uniforme de la densité des véhicules sur des portions d'autoroute. Équilibrer la densité est un nouvel objectif de trafic qui peut potentiellement réduire le nombre et l'intensité des accélérations et décélérations et peut par conséquent permettre des voyages plus sécurisés et confortables tout en diminuant la consommation de carburant et les émissions de polluants. En outre, cet objectif prend en compte les paramètres de trafic standards tels que le Temps de Trajet Total et la Distance Totale Parcourue. Une architecture modulaire distribuée est proposée pour le contrôleur. Cela permet de déterminer les décisions optimales à prendre en utilisant uniquement des informations d'état locales et en provenance des contrôleurs voisins.La contribution débute par l'analyse d'ensembles d'équilibre de CTM. L'objectif de cette étude est d'obtenir les conditions qui assurent l'existence et l'unicité des états stationnaire qui sont équilibrées. Dans l'ensemble des états stationnaire, nous sommes intéressés à la sélection du point qui maximise la Distance Totale Parcourue. Sont discutés ensuite les aspects de la mise en œuvre et les limites de la méthode proposée. Enfin, plusieurs études de cas sont présentées appuyant les résultats d'analyse et examinant l'efficacité de la méthode proposée.La majeure partie de la thèse vise à concevoir un dispositif de commande optimale pour équilibrer la densité du trafic routier. L'optimisation est réalisée de manière répartie. En utilisant les propriétés de contrôlabilité, l'ensemble des sous-systèmes devant être contrôlés par des feux aux rampes d'accès sont identifiés. Le problème d'optimisation est alors formulé comme de Nash du jeu dans un environnement non coopératif. Le jeu est résolu en le décomposant en une série de jeux à deux joueurs hiérarchiques et compétitifs. Le processus d'optimisation emploie des canaux de communication qui correspond à la structure de commutation de l'interconnexion de système. L'approche alternative pour équilibrer emploie la théorie des systèmes multi-agents. Chacun des contrôleurs est pourvu d'une structure à rétroaction assurant que les états au sein de son sous-système atteignent des valeurs communes par l'évaluation de protocoles de consensus. Dans ces structures, un problème de contrôle optimal minimisant le Temps de Trajet Total est formulé. Le contrôleur distribué fondé sur le jeu de Nash est validé grâce des simulations microscopiques Aimsun. Le scénario de test comprend des données de trafic provenant de la rocade sud de Grenoble. / The thesis presents the results of research on distributed and coordinated control method for freeway ramp metering. The freeway traffic is represented by the Cell-Transmission Model. The primary control objective is to provide a uniform distribution of vehicle densities over freeway links. Density balancing is a new traffic objective which can potentially reduce the number and intensity of acceleration and deceleration events and therefore, it can make a travel more safety and comfortable while decreasing fuel consumption and emissions. In addition, the objective takes into account standard traffic metrics like Total Travel Distance and Total Travel Spent. For the controller, a distributed modular architecture is assumed. It enables to compute the optimal decisions by using only local state information and some supplementary information arriving from the neighbouring controllers.The contributing part begins with the analysis on equilibrium sets of the Cell-Transmission Model. The goal of this study is to derive the conditions that assure the existence and the uniqueness of the balanced equilibrium states. The next step is to find a set of inputs such that the resulting equilibrium state is balanced. In the set of balanced equilibria, we are interested in the selection of the point that maximizes the Total Travel Distance. In the sequel, the implementation aspects and limitations of the proposed method are discussed. Finally, several case studies are presented to support the analysis results and to examine the effectiveness of the proposed method.The major part of the thesis aims on a design of an optimal controller for balancing the traffic density. The optimization is performed in a distributed manner. By using controllability properties, the set of subsystems to be controlled by local ramp meters are identified. The optimization problem is then formulated as a non-cooperative Nash game. The game is solved by decomposing it into a set of two-players hierarchical and competitive games. The process of optimization employs the communication channels matching the switching structure of system interconnectivity. The alternative approach of balancing employs the theory of multi-agent systems. Each of the controllers is provided with a feedback structure assuring that the states within its local subsystem achieve common values by evaluating consensus protocols. Under these structures, an optimal control problem to minimize the Total Travel Spent is formulated. The distributed controller based on the Nash game is validated via Aimsun micro-simulations. The testing scenario involves the traffic data collected from the south ring of Grenoble.

Cette thèse traite des problèmes et des défis de sécurité dans l’Internet des Objets (IdO). L’évolution de l’Internet classique vers l’Internet des Objets crée de nombreux challenges dans la manière de sécuriser les communications et soulève des problèmes liés au contraintes de l’internet des objets à savoir : objets à faibles ressources d’énergie et de calculs, hétérogénéité nuisant à l’interopérabilité des objets, taille du réseau de plus en plus grande, ... etc. En effet, Internet s’est développé d’un réseau d’ordinateurs personnels et de serveurs vers un immense réseau connectant des milliards d’objets intelligents communicants. Ces objets seront intégrés dans des systèmes complexes et utiliseront des capteurs et actionneurs pour observer et interagir avec leur environnement physique. Les exigences des interactions entre objets communicants en termes de sécurité dépendent du contexte qui évolue dans l’espace et le temps. Par conséquent, la définition de la politique de sécurité doit être adaptative et sensible au contexte. Un des problèmes auxquels nous nous sommes intéressés est le contrôle d’accès efficace à base de cryptographie d’attributs : « Attributes Based Encryption (ABE) ». Les schémas ABE (CP-ABE et KP-ABE) présentent plusieurs atouts pour l’implémentation d’un contrôle d’accès cryptographique. Par contre, ces schémas posent des défis opérationnels à cause de leurs complexités et leur surcoût élevé en termes de temps d’exécution et consommation énergétique. Pour pallier cet inconvénient, nous avons exploité l’hétérogénéité d’environnement Internet des Objets pour proposer des versions collaboratives et distribuées de ces schémas de contrôle d’accès cryptographique. Nos solutions réduisent considérablement le coût en termes d’énergie nécessaire à l’exécution. Le deuxième inconvénient des schémas ABE est l’inexistence de mécanismes efficaces de gestion de clés. Nous avons proposé des solutions pour le problème de révocation d’attributs dans le schéma CP-ABE, Ces solutions, en plus de leur efficacité, répondent à des exigences de sécurité différentes selon le cas d’applications. Nous avons proposé également, une solution à base de CP-ABE pour le problème du « grouping proof ». Le « grouping proof » consiste à fournir une preuve sur la coexistence, dans le temps et l’espace, d’un ensemble d’objets. Parmi les applications de notre solution, on peut citer le payement NFC et la sécurisation de l’accès aux locaux sensibles. / In this thesis, we deal with security challenges in the Internet of Things. The evolution of the Internet toward an Internet of Things created new challenges relating to the way to secure communications given the new constraints of IoT, namely: resource constrained objects, heterogeneity of network components, the huge size of the network, etc. Indeed, the Internet evolved from a network of computers and servers toward a huge network connecting billions of smart communicating objects. These objects will be integrated into complex systems and use sensors and actuators to observe and interact with their physical environment. The security requirements of the interactions between smart objects depend on the context which evolves in time and space. Consequently, the definition of the security policies should be adaptive and context-aware. In this thesis, we were interested in the problem of access control in IoT relying on Attribute based Encryption (ABE). Indeed, ABE schemes present many advantages in implementing a cryptographic fine-grained access control. However, these schemes raise many implementation challenges because of their complexity and high computation and energy overheads. To overcome this challenge, we leveraged the heterogeneity of IoT to develop collaborative and distributed versions of ABE schemes. Our solutions reduce remarkably the overhead in terms of energy consumption and computation. The second limitation of ABE schemes is the absence of efficient attribute/key revocation techniques. We have proposed batch based mechanisms for attribute/key revocation in CP-ABE. We demonstrated the efficiency of the proposed solutions through simulations. Finally, we have proposed a CP-ABE based solution for the problem of grouping proof. This problem consists of providing the proof that a set of objects are present simultaneously (same time and same location). The propose solution has many applications such as enforcing the security of NFC based payments and the access to sensitive locations.

Cette thèse étudie des problèmes de contrôle d'accès et de qualité de service (QdS) dans les réseaux ad hoc utilisant la norme IEEE 802.11. Dans la première partie de notre travail, nous proposons des améliorations pour la norme 802.11 de base qui ne tient pas compte de la QdS. Au niveau du contrôle d'admission, nous proposons un algorithme d'ordonnancement des flux multimédia qui attribue la priorité aux paquets de manière moins stricte que dans l'algorithme EDF et nous comparons les deux algorithmes par simulation. Au niveau du contrôle d'accès, nous proposons un algorithme qui modifie dynamiquement la fenêtre de contention, et nous effectuons des simulations pour montrer l'amélioration de l'équité entre les stations. Nous nous intéressons par la suite à la différenciation des services, et nous étudions la coexistence de deux classes de service, dont les fenêtres de contention évoluent de manière différente, et évaluons leurs performances en termes de débit et de délai moyen. Ce qui nous amène, dans la deuxième partie de notre travail, à présenter une étude complète de la différenciation des services de l'amendement 802.11e. Nous proposons un cadre analytique général modélisant la méthode d'accès EDCA à l'aide de chaînes de Markov, et définissons quatre méthodes de différenciation, et évaluons les performances des classes en termes de débit, délai moyen et taux de perte. Des approximations pour les réseaux de grande taille nous ont permis d'obtenir, pour un indice de performance fixé, une expression simple de celui de toutes classes en fonction de celui de l'une d'entre elles. Nous déterminons ensuite la relation entre les différents indices de performance des classes, et comparons les différentes méthodes de différenciation, malgré la nature différente de leurs paramètres. De plus, nous établissons analytiquement et vérifions par simulation les conditions d'équivalence, entre les méthodes de différenciation basées sur la distribution du temps de retrait, qui produisent les mêmes performances en termes de débit, délai moyen et taux de perte. Et dans ces conditions, nous analysons l'effet du choix de la distribution sur la gigue. Nos résultats représentent des outils importants pour l'aide à la décision en vue d'atteindre des objectifs de QdS. / This thesis deals with access control and quality of service (QoS) issues in ad hoc networks. In the first part, we propose enhancements of the legacy 802.11 standard which lacks of QoS. For admission control, we propose a scheduling algorithm for multimedia traffic, in which priority is provided to packets with a less strict way than the EDF algorithm, and we compare both algorithms by simulation. For access control, we propose an algorithm that tunes dynamically the contention window, and we use simulations to show improvement of fairness between stations. Then we are interested in service differentiation, and we analyze the coexistence of two service classes having their contention window evolving in different ways, and we evaluate their performances in terms of throughput and mean delay. This leads us, in the second part of this thesis, to present a complete study of service differentiation in the 802.11e amendment. We propose a general analytical framework in which we model the EDCA access scheme by Markov chains. We define and study four differentiation schemes and evaluate class performances in terms of throughput, mean delay and drop ratio. Using approximations for large networks, we derive, for a given class performance index, a simple expression of this index in the other classes. That allows us to determine the relationship between class performances, and compare the differentiation schemes even if the nature of their parameters is different. Moreover, we determine analytically and verify by simulation equivalence conditions, between differentiation schemes based on backoff time distribution, that produce the same performances in terms of throughput, mean delay and drop ratio. Then, in these conditions, we analyze the effect of backoff time distribution on jitter. Our results are important tools for decision making in order to meet QoS objectives.

Dans le domaine médical, la numérisation des documents et l’utilisation des dossiers patient électroniques (DPE, ou en anglais EHR pour Electronic Health Record) offrent de nombreux avantages, tels que la facilité de recherche et de transmission de ces données. Les systèmes informatiques doivent reprendre ainsi progressivement le rôle traditionnellement tenu par les archivistes, rôle qui comprenait notamment la gestion des accès à ces données sensibles. Ces derniers doivent en effet être rigoureusement contrôlés pour tenir compte des souhaits de confidentialité des patients, des règles des établissements et de la législation en vigueur. SGAC, ou Solution de Gestion Automatisée du Consentement, a pour but de fournir une solution dans laquelle l’accès aux données du patient serait non seulement basée sur les règles mises en place par le patient lui-même mais aussi sur le règlement de l’établissement et sur la législation. Cependant, cette liberté octroyée au patient est source de divers problèmes : conflits, masquage des données nécessaires aux soins ou encore tout simplement erreurs de saisie. Pour effectuer ces vérifications, les méthodes formelles fournissent des moyens fiables de vérification de propriétés tels que les preuves ou la vérification de modèles. Cette thèse propose des méthodes de vérification adaptées à SGAC pour le patient : elle introduit le modèle formel de SGAC, des méthodes de vérifications de propriétés. Afin de mener ces vérifications de manière automatisée, SGAC est modélisé en B et Alloy ; ces différentes modélisations donnent accès aux outils Alloy et ProB, et ainsi à la vérification automatisée de propriétés via la vérification de modèles ou model checking. / Abstract : In healthcare, data digitization and the use of the Electronic Health Records (EHR) offer several benefits, such as the reduction of the space occupied by data, or the ease of data search or data exchanges. IT systems must gradually take up the archivist’s role by managing the accesses over sensitive data, which have to be compliant with patient wishes, hospital rules, as well as laws and regulations. SGAC, or Solution de Gestion Automatisée du Consentement (Automated Consent Management Solution), aims to provide a solution in which access to patient data would be based on patient rules, hospital rules and laws. However, the freedom granted to the patient can cause several problems : conflicts, concealment of crucial data needed to treat the patient adequately, and data-capture errors. Therefore, verification and validation of policies are essential : formal methods provide reliable ways, such as proofs or model checking, to conduct verifications of properties. This thesis provides verification methods applied on SGAC for the patient : it introduces the formal model of SGAC, methods to verify properties such as data access resolution, hidden data detection or redundant rule identification. Modeling of SGAC in B and Alloy provides access to the tools Alloy and ProB, and thus, automated property verification through model checking.

Cette thèse démontre l'importance des informations réseau inter-couche pour les applications réseaux. Cette dissertation présente une nouvelle architecture de contrôle d'accès dans laquelle le contrôleur est mutualisé dans le Cloud. Cette architecture permet d'adresser un marché clé pour des clients ne pouvant acheter du matériel spécialisé. Plusieurs verrous techniques ont du être résolus pour pouvoir implémenter cette architecture, en effet les informations du réseau privé ne sont plus disponible au niveau du contrôleur ce qui l'empêche de correctement contrôler l'activité des utilisateurs. Une première implémentation est présentée dans le chapitre 2, elle utilise des équipements spécialisés capable d'interagir avec le contrôleur centralisé. Cette implémentation comportant des faiblesses, nous nous sommes intéressés à une approche par réseaux logiciels. Une solution innovante pour partager des informations inter-couche à l'extérieur d'un réseau SDN est présentée dans le chapitre 3. Elle permet d'intercepter et de modifier des flux de données utilisateurs à la volée afin de transmettre des informations à l'intérieur de la couche applicative. Cette solution a été implémentée dans le contrôleur OpenDaylight et montre des résultats très encourageants. Couplée au contrôleur centralisé, cette solution permet de fournir une solution complète de contrôle d'accès réseau qui est simple à déployer et configurer et extensible aisément. / This thesis presents the importance of cross-layer network information for network applications in the context of network access control. The dissertation exposes a novel architecture in which a network access controller is mutualized in the Cloud. This architecture allows to address a key market segment for clients unwilling to buy expensive hardware to control their network. Multiple challenges come into play when hosting the controller remotely. Indeed cross-layer information are no longer available which prevents the controller from correctly controlling users activity. A first implementation to share cross-layer information is presented in chapter 2. It leverages specialized session border controllers to send these data in the application protocol, here HTTP. Then chapter 3 presents an innovative solution for the cross-layering problem which allows to intrumentalize network flows with SDN protocols. The solution focuses on a web portal redirection but is extendable to any kind of protocols. The implementation permits to intercept and modify flows in order to input cross-layer data within another network protocol. This solution was implemented in the OpenDaylight OpenFlow controller and shows great results. The mutualized approach coupled with the SDN cross-layer framework allow to build flexible networks with almost no configuration of on-site equipments. The central network controller reduces the overal cost of the solution by being mutualized among multiple clients. Moreover, having the ability to intrumentalize network traffic in software allows to implement any kind of custom behavior on the runtime.

Dans cette thèse, nous concevons trois nouveaux mécanismes d'authentification basés sur l'identité des utilisateurs. Par conséquent, nous apportons des améliorations sur le contrôle d'accès à différents types de réseaux tels que les réseaux domestiques, les réseaux gouvernementaux et les réseaux cellulaires. L'identité se base sur des gabarits biométriques publics, des chaînes de caractères simples comme l’adresses e-mail ou l’identifiant (login). La première solution concerne l'utilisation de données biométriques dans les mécanismes d'authentification des réseaux domestiques (Home Network HN). Nous voulons personnaliser l'accès de chaque utilisateur dans le HN et prévenir les utilisateurs illégitimes (en passant par la passerelle domestique « Home Gateway (HG) ») d'avoir accès aux services. Nous proposons une nouvelle méthode d'authentification biométrique qui respecte la contrainte de ne pas sauvegarder les données biométriques (Biometric Template (BT)) des utilisateurs dans le HG. Pour satisfaire cette contrainte, nous proposons d'utiliser la méthode de « Fuzzy Vault » pour cacher un secret utilisé pour l'authentification. Un logiciel génère une identité biométrique révocable (BioID) en utilisant une transformation fonctionnelle. Ce BioID est utilisé par le mécanisme du fuzzy vault pour cacher une clé de session secrète. La deuxième solution propose des mécanismes d'authentification pour les passeports biométriques (e-Passeports). Les paramètres de chiffrement sont générés en utilisant les données biométriques et, ainsi, ils seront personnalisés pour l'utilisateur. Notre proposition introduit un nouveau mécanisme d'authentification pour le passeport biométrique utilisant le protocole Diffie-Hellman de partage de clé basé sur les courbes elliptiques (ECDH). Ce protocole est nécessaire pour générer une clé de session utilisée pour authentifier le voyageur et le système d'inspection (IS) et ainsi sécuriser l'échange des données entre eux. Notre protocole peut utiliser les points "minuties" d'une empreinte digitale et le code de l'iris du détenteur du passeport électronique. Dans la troisième solution, nous avons travaillé sur le réseau cellulaire et nous avons utilisé une chaîne de caractères simple (l’adresse e-mail de l’utilisateur) comme identifiant pour accéder aux services. Nous avons choisi l'IP Multimedia Subsystem (IMS) qui est une architecture de recouvrement pour la fourniture de services multimédia, comme support. Nous avons conçu un nouveau mécanisme d'authentification aux services en utilisant la cryptographie basée sur l'identité (IBC). L'objectif était d'authentifier les utilisateurs en utilisant leurs identifiants public et privé pour surmonter les faiblesses connues du protocole «Authentication and Key Agreement (AKA) ». Nous nous sommes concentrés sur les tentatives d'écoute et d’usurpation d'identité qui peuvent avoir lieu dans le scénario classique de l’IMS et nous avons montré comment la solution proposée peut prévenir ces attaques. Nous avons ensuite proposé d'ajouter une vérification par lot au niveau du Bootstrapping Server Function (BSF) pour diminuer le délai de vérification des signatures et le temps de réponse de l’authentification. / In this thesis, we design three new authentication mechanisms based on user identity. Therefore, we bring improvements in access control for different classes of networks such as Home Network, Governmental Network and Cellular Network. The identity can be biometric public features, simple strings (email addresses, login...), etc. The first solution concerns the use of biometric in Home Network' authentication mechanisms. In the Home Network (HN) case study, we aim at personalizing the access of each user in the HN and preventing illegitimate users (passing by the Home Gateway (HG)) to have any access. We propose a new biometric authentication method which respects the constraint of the non storage of the users' Biometric Template (BT) in the HG. To satisfy this constraint, we propose using the fuzzy vault method to hide a secret that should be used for authentication. A software generates a revocable biometric identity (BioID) using a functional transformation. This BioID is used in the fuzzy vault mechanisms to hide a secret session key. The second solution proposes e-Passport authentication mechanisms. The cryptographic parameters are generated using the biometric templates and hence, personalized for the user. In travel document case study, we present our proposal which introduces a new e-Passport authentication mechanisms based on the Elliptic Curve Diffie-Hellman (ECDH) Key Agreement protocol. This protocol is needed to generate a session key used to authenticate the traveler and the Inspection System (IS) to exchange secure data. Our protocol is defined using minutiae data (fingerprint) and iris code of the e-Passport holder. In the third solution, we worked on the Cellular Network and we used a simple string, like email addresses, as identifier to access to services. We choose the IP Multimedia Subsystem (IMS) which is an overlay architecture for the provision of multimedia services. We design a new service authentication mechanism relying on Identity Based Cryptography (IBC) for the IMS architecture. The goal was to authenticate the users using their public and private identifiers to overcome known weaknesses in the Authentication and Key Agreement (AKA) protocol. We focused on the eavesdropping and impersonation attacks that can take place in classical IMS scenario and we showed how our proposed solution can prevent against these attacks. We, then, proposed to add a Batch Verification on the Bootstrapping Server Function (BSF) to decrease signature verification delay and the authentication response time.

Dans le domaine médical, la numérisation des documents et l’utilisation des dossiers patient électroniques (DPE, ou en anglais EHR pour Electronic Health Record) offrent de nombreux avantages, tels que le gain de place ou encore la facilité de recherche et de transmission de ces données. Les systèmes informatiques doivent reprendre ainsi progressivement le rôle traditionnellement tenu par les archivistes, rôle qui comprenait notamment la gestion des accès à ces données sensibles. Ces derniers doivent en effet être rigoureusement contrôlés pour tenir compte des souhaits de confidentialité des patients, des règles des établissements et de la législation en vigueur. SGAC, ou Solution de Gestion Automatisée du Consentement, a pour but de fournir une solution dans laquelle l’accès aux données du patient serait non seulement basée sur les règles mises en place par le patient lui-même mais aussi sur le règlement de l’établissement et sur la législation. Cependant, cette liberté octroyée au patient est source de divers problèmes : conflits, masquage des données nécessaires aux soins ou encore tout simplement erreurs de saisie. C’est pour cela que la vérification et la validation des règles d’accès sont cruciales : pour effectuer ces vérifications, les méthodes formelles fournissent des moyens fiables de vérification de propriétés tels que les preuves ou la vérification de modèles.Cette thèse propose des méthodes de vérification adaptées à SGAC pour le patient : elle introduit le modèle formel de SGAC, des méthodes de vérifications de propriétés telles l’accessibilité aux données ou encore la détection de document inaccessibles. Afin de mener ces vérifications de manière automatisée, SGAC est modélisé en B et Alloy ; ces différentes modélisations donnent accès aux outils Alloy et ProB, et ainsi à la vérification automatisée de propriétés via la vérification de modèles ou model checking / In healthcare, data digitization and the use of the Electronic Health Records (EHR) offer several benefits, such as reduction of the space occupied by data, or the ease of data search or data exchanges. IT systems must gradually act as the archivists who manage the access over sensitive data. Those have to be checked to be consistent with patient privacy wishes, hospital rules, and laws and regulations.SGAC, or Solution de Gestion Automatisée du Consentement, aims to offer a solution in which access to patient data would be based on patient rules, hospital rules and laws. However, the freedom granted to the patient can cause several problems: conflicts, hiding of the needed data to heal the patient or simply data-capture error. Therefore, verification and validation of policies are crucial: to conduct this verification, formal methods provide reliable ways to verify properties like proofs or model checking.This thesis provides verification methods applied on SGAC for the patient: it introduces the formal model of SGAC, verification methods of properties such as data reachability or hidden data detection. To conduct those verification in an automated way, SGAC is modelled in B and Alloy; these different models provide access to the tools Alloy and ProB, and thus, automated property verification with model checking