Ce travail de thèse apporte une contribution aux recherches visant une meilleure connaissance des mécanismes d'accidents se produisant en ville et le développement de méthodes et d'outils permettant à des praticiens réalisant des études locales de sécurité, de disposer d'une meilleure connaissance des processus d'accident à l'oeuvre localement et des mesures possibles pour leur prévention. Dans un premier temps, à partir de l'analyse approfondie de plusieurs centaines de cas d'accidents s'étant produits sur le territoire français, nous décrivons quarante scénarios types d'accidents urbains n'impliquant pas de piétons. Une discussion relative aux moyens de prévention est proposée pour chacun d'entre eux en référence à la littérature internationale en sécurité routière. Ces résultats permettent de disposer, avec les travaux récemment achevés à I' sur les scénarios d'accidents de piétons, d'une connaissance d'ensemble des processus d'accidents les plus fréquemment à l'oeuvre en ville et sur les moyens susceptibles de les prévenir. Ils permettent également, avec un ensemble de méthodes de reconnaissance permettant l'affectation des accidents d'un échantillon local aux scénarios types préétablis, d'envisager leur utilisation dans le cadre d'études de sécurité réalisées par des ingénieurs locaux sur des terrains d'étude délimités. Dans un second temps, les investigations ont porté sur lopérationnalité d'outils méthodologiques de diagnostic s'appuyant sur ces scénarios types de référence. L'utilité relative de ces outils est d'abord évaluée sur deux terrains d'étude par comparaison avec des démarches d'étude diagnostique plus traditionnelles. Leur «utilisabilité» est ensuite étudiée au moyen d'entretiens auprès de praticiens ayant mis en oeuvre de tels outils méthodologiques, et par l'examen des résultats de leurs analyses. Les résultats confirment que l'accident urbain peut être modélisé sous forme de pathologies routières. Les scénarios types d'accidents constituent ainsi des outils utiles à la prévention.

Le chiffrement est sûrement une primitive fondamentale parmi les fonctions cryptogra- phiques. Cela rend possible à deux parties, d'ordinaire appelées Alice et Bob, de commu- niquer au travers d'un canal non sécurisé en permettant qu'un adversaire, Eve, ne puisse pas comprendre leur communication. Il pourrait sembler assez facile d'identifier les contraintes nécessaires pour le design d'un " bon " schéma de chiffrement. Il s'avère en réalité que la définition d'un modèle de sécurité rigoureux n'est pas trivial. Ceci dépend fortement du contexte. La sécurité même dépend du contexte. Ce document s'ouvre avec un chapitre d'introduction à la cryptographie à clé publique. Nous décrirons ensuite comment la sécurité d'une telle primitive est évaluée en définissant de façon rigoureuse un attaquant, en particulier cela signifie fixer son but et les moyens dont il dispose. La suite de ce document s'organise autour de deux parties. La première partie concerne l'anonymat révocable. Nous obtenons et présentons deux schémas pour garantir l'anonymat pour l'envoyeur d'un message chiffré mais avec la possibilité pour un troisième acteur de confiance, si le cas le nécessite, de révéler l'identité de l'envoyeur. Cette primitive a été appliquée dans les contextes du chiffrement à clé publique et du chiffrement broadcast. Dans la deuxième partie, nous nous dédions à l'étude et à l'amélioration d'un schéma de chiffrement à clé publique dont l'original est dû à Goldwasser et Micali. Notre travail généralise leur schéma en fournissant une famille de schémas de chiffrement. Notre travail est motivé par la recherche de l'amélioration de l'efficacité (en termes de bande passante) du schéma original, afin de pouvoir chiffrer des messages plus longs dans un chiffré de la même taille.

La question de la sécurité privée est un sujet d'actualité. Ce secteur en pleine expansion a fait l'objet de réglementations ces dernières décennies. Sa particularité tient en la privatisation d'un domaine régalien de l'intervention étatique. La sécurité privée pose ainsi la problématique du traitement de la mission de sécurité. Si le secteur privé investit de plus en plus le domaine de la sécurité, il se différencie du secteur public. La participation du secteur privé s'effectue par voie contractuelle qui obéit pour partie de ses aspects au droit commun, malgré l'objectif de maintien de l’ordre public. / The issue of private security is a hot topic. This rapidly expanding sector has been the subject of regulations in recent decades. Its peculiarity lies in the privatization of a sovereign domain reserved for state intervention. Private security then poses the problem of processing the security mission. We note that the private sector is investing more and more in the field of security while differentiating itself from the public sector. The participation of the private sector is done by contract which obeys most of its aspects in common law.

Cette thèse s’inscrit dans le cadre théorique très général de la sécurité des systèmes complexes. Son terrain d’application est la marine marchande. L’objectif de cette recherche est double : 1. Investiguer la gestion du risque d’abordage grâce à une démarche systémique s’intéressant à la fois aux conditions de l’échec et à celles du succès. 2. Explorer les liens entre les trois concepts liés à la sécurité que sont la Culture de sécurité, le Système de Management de la Sécurité et la Résilience. La culture de sécurité constitue un sous-ensemble de la culture organisationnelle globale. Elle se compose d’un ensemble de valeurs, de croyances, d’attitudes, de normes et de pratiques concernant la sécurité. Partagé par les membres d’une organisation, cet ensemble influence directement les comportements mis en oeuvre dans le cadre du travail. Dans le cadre de cette thèse, nous avons tout d’abord réalisé une analyse du domaine de travail du système du transport maritime, ainsi, qu’une étude des cas d’abordage entre navires répertoriés par le MAIB (Marine Accident Investigation Branch). Ces analyses ont permis, respectivement, d’identifier les barrières de défense du système et de mettre en évidence les principales causes à l’origine des accidents. Les études suivantes ont cherché à appréhender la culture de sécurité d’un armement réputé sûr, grâce à un couplage de méthodes qualitatives et quantitatives. L’analyse du système de management de l’armement a démontré que celui-ci était performant. Il s’appuie sur un solide système de retour d’expérience et se montre participatif. Une enquête portant sur le climat de sécurité a été menée auprès de plusieurs équipages, à l’aide d’un questionnaire inspiré de celui de Håvold. Elle montre qu’une grande majorité des opérateurs adhère à une culture de sécurité positive, bien que les scores soient significativement influencés par la fonction et par le niveau hiérarchique des répondants. Enfin, l’analyse de l’activité des chefs de quart en passerelle a mis en évidence des mécanismes de gestion diachronique et synchronique des risques externes (i.e. Risque de collision). Les résultats de ces différentes études conduisent à discuter de l’articulation entre Culture de Sécurité, Résilience et Système de Management de la Sécurité. La proposition d’un modèle tridimensionnel de la sécurité montre que la Culture de Sécurité semble en effet agir comme le médiateur des deux autres concepts. Elle permettrait également au système de conserver une importante part de sécurité gérée, malgré la forte composante de sécurité réglée liée aux contraintes réglementaires importantes du secteur. / This thesis belongs in the general theoretical area of the safety of complex systems. Its field of application is the merchant navy. Its object is twofold: 1. To investigate the management of collision risks by a systemic approach which takes into account both factors leading to failure and those leading to success; and, 2. To explore the links between three concepts of safety : Safety culture, Safety Management Systems and Resilience. Safety culture is a subset of the overall organizational culture. It consists of a set of values, beliefs, attitudes, norms and practices concerning safety. Shared by members of an organization, this directly influences behaviour at work. The first step in the research was to study the marine transportation system and collisions between merchant vessels listed by the United Kingdom’s Marine Accident Investigation Branch (MAIB), focussing on two areas: the safety barriers system and the main failures leading to accidents. Qualitative and quantitative methods were then applied to gain an understanding of the safety culture of a shipping company with a good safety record. Analysis of this company’s management system showed it to be effective: it was built on a strong reporting system and seemed to be participatory. A survey of the safety climate was conducted with several crews, using a questionnaire inspired by Håvold’s questionnaire. This showed that a large majority of the company’s personnel had a positive safety culture, although the scores were significantly influenced by the duty and the hierarchical level of individual respondents. Finally, the activities of bridge watchkeeping officers were studied to identify diachronic and synchronic mechanisms implemented to manage the collision risk. The results of these studies enable a discussion of the relationship between Safety Culture, Resilience and Safety Management System. A proposal for a generic three-dimensional safety model shows that Safety Culture seems to act as the mediator of the other two concepts. Safety Culture would also allow the system to maintain a significant portion of “managed safety”, complementing a strong element of “prescribed safety” flowing from regulation.

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.

Dans cette thèse, on s'intéresse à des schémas de chiffrement par blocs, c'est-à-dire que le chiffrement (et le déchiffrement) envoie un bloc de n bits sur un bloc de n bits. Il y a essentiellement deux grandes structures utilisées pour un schéma de chiffrement par blocs : la structure de Feistel (utilisée pour le DES) et la structure SPN (utilisée pour l'AES). L'étude de la sécurité de ces différents structures et schémas a permis de nombreuses avancées autant pratiques que théoriques. Nous présentons dans cette thèse des preuves de sécurité pour le schéma d'Even-Mansour itéré, le schéma paramétrable CLRW et le schéma de Feistel à clés alternées. Ces preuves utilisent une technique probabiliste, appelée coupling, introduite en cryptographie en 2002 par Mironov. Nous présentons cette technique dans le cadre des probabilités, puis la façon d'utiliser le coupling pour prouver la sécurité des schémas cités précédemment. Nous présentons également une étude de la sécurité du schéma d'Even-Mansour à deux tours pour certaines minimisations (même clés de tours ou même permutations internes par exemple) et, pour conclure, une comparaison des différentes techniques d'indistinguabilité / In this thesis, we study blockciphers, meaning that the encryption (and decryption) sends a block of n bits on a block of n bits. There is essentially two main structures used for a blockcipher: the Feistel structure (used for DES) and the SPN structure (used for AES). The study of the security of these structures and schemes has led to many practical and theoretical advances. We present in this thesis proofs of security for the iterated Even-Mansour scheme, the tweakable blockcipher CLRW and the key-alternating Feistel cipher. These proofs use a probabilistic technique, called coupling, introduced in cryptography in 2002 by Mironov. We present this technique in the context of probabilities, then we present how to use the coupling to prove the security for the schemes mentioned above. We also present an analysis of the security of the Even-Mansour cipher with two rounds and some properties (same round keys or same internal permutations for example) and, finally, we compare the different techniques to prove indistinguishability

Cette recherche est envisagée pour observer la place de l’Islam confrérique dans la sphère publique et dans la vie politique, économique et sociale au Sénégal, avec un accent particulier sur la notion de sécurité humaine. Notre ambition est d’intégrer une réflexion la plus large possible sur les différentes situations contrastées que connaît l’Islam confrérique dans ce pays de 12 millions d’habitants avec plus de 90% de musulmans. L’accent consiste à interroger ce qu’on a appelé « l’exceptionnalisme sénégalais » avec une tradition démocratique relativement ancienne et solide. Cette étude a comme objet général d’explorer la sécurité que posent l’organisation et le fonctionnement des confréries religieuses sénégalaises. Elle s’appuie sur la mise en comparaison des deux principales confréries – Mouride et Tidjane – qui sont d’obédience sunnite. Elle intègre un angle d’approche tenant compte de la diversité et de la particularité des contextes socioculturels, politiques, économiques et religieux dans l’ordre international marqué par des menaces incessantes sur la sécurité. Cette mise en perspective de dynamiques culturelles singulières favorise la compréhension de logiques comportementales attribuant du sens à des démarches de sécurité des « fidèles » auprès des Marabouts et des confréries. Il s’agit aussi d’évaluer les nouvelles manifestations religieuses et leurs conséquences en termes individuels et collectifs sur la République, la démocratie, la laïcité et la sécurité de la nation sénégalaise. / This research is intended to observe the place of brotherhood of Islam in the public sphere and the political, economic and social Senegal, with particular emphasis on the concept of human security. Our goal is to integrate thinking about the broadest possible contrasting the different situations facing brotherhood of Islam in this country of 12 million people with over 90% Muslim. The focus is to examine the so-called "Senegalese exceptionalism" with a relatively old democratic tradition and strong. This study explored as general purpose security posed by the organization and functioning of religious brotherhoods in Senegal. It relies on setting comparison of the two major guilds - and Mouride Tidjane - who are Sunni. It includes an angle of approach taking into account the diversity and unique socio-cultural contexts, political, economic and religious in the international order marked by constant threats to security. This perspective of cultural dynamics unique promotes understanding of behavioral logic of assigning meaning to approaches to security "faithful" to the Marabouts and fraternities. It is also evaluating new religious events and their consequences for individuals and groups on the Republic, democracy, secularism and security of the Senegalese nation.

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 sécurité des vaccins est évaluée par le biais du système de surveillance passive des manifestations cliniques indésirables (MCI). À cause du très grand nombre de personnes vaccinées lors des campagnes massives de vaccination contre l'influenza, si un effet secondaire modérément fréquent (ex. 1/1 000 vaccinés) survenait, le délai avant que la surveillance passive ait détecté un problème serait suffisamment long pour que des millions de personnes aient été vaccinés et que des milliers aient souffert de cet effet secondaire. Lors de la vaccination de masse contre l'influenza pandémique H1N1 en 2009, un projet pilote de surveillance électronique active de la sécurité du vaccin contre l'influenza pandémique chez plusieurs milliers de travailleurs de la santé a été mis sur pied. Cette surveillance visait à évaluer très rapidement la fréquence des problèmes de santé suffisamment sévères pour causer de l'absentéisme au travail ou une consultation médicale. La présente étude a évalué la qualité de cette surveillance par le biais de ses attributs comme définis dans le cadre de référence des Centers for Disease Control and Prevention (CDC) pour l'évaluation des systèmes de surveillance. Une méthodologie mixte (analyse quantitative et qualitative) a été utilisée. Les résultats montrent que la simplicité, la flexibilité, l'acceptabilité et la valeur prédictive positive (VPP) étaient des attributs plutôt acquis par le système de surveillance, mais que des déficiences étaient présentes dans le contrôle de la qualité des données, la sensibilité, la représentativité et la réactivité. Des recommandations ont été émises pour améliorer ce système, qui pourraient servir dans le cas d'une nouvelle pandémie ou s'intégrer au processus formel de surveillance de la vaccination saisonnière contre l'influenza.

Notre société utilise de nombreux systèmes de communications. Parce que ces systèmes sont omniprésents et sont utilisés pour échanger des informations sensibles, ils doivent être protégés. Cela est fait à l'aide de protocoles cryptographiques. Il est crucial que ces protocoles assurent bien les propriétés de sécurité qu'ils affirment avoir, car les échecs peuvent avoir des conséquences importantes. Malheureusement, concevoir des protocoles cryptographiques est notoirement difficile, comme le montre la régularité avec laquelle de nouvelles attaques sont découvertes. Nous pensons que la vérification formelle est le meilleur moyen d'avoir de bonnes garanties dans la sécurité d'un protocole: il s'agit de prouver mathématiquement qu'un protocole satisfait une certaine propriété de sécurité.Notre objectif est de développer les techniques permettant de vérifier formellement des propriétés d'équivalence sur des protocoles cryptographiques, en utilisant une méthode qui fournit de fortes garanties de sécurités, tout en étant adaptée à des procédures de preuve automatique. Dans cette thèse, nous défendons l'idée que le modèle Bana-Comon pour les propriétés d'équivalences satisfait ces objectifs. Nous soutenons cette affirmation à l'aide de trois contributions.Tout d'abord, nous étayons le modèle Bana-Comon en concevant des axiomes pour les fonctions usuelles des protocoles de sécurités, et pour plusieurs hypothèses cryptographiques. Dans un second temps, nous illustrons l'utilité de ces axiomes et du modèle en réalisant des études de cas de protocoles concrets: nous étudions deux protocoles RFID, KCL et LAK, ainsi que le protocole d'authentification 5G-AKA, qui est utilisé dans les réseaux de téléphonie mobile. Pour chacun de ces protocoles, nous montrons des attaques existentes ou nouvelles, proposons des versions corrigées de ces protocoles, et prouvons que celles-ci sont sécurisées. Finalement, nous étudions le problème de l'automatisation de la recherche de preuves dans le modèle Bana-Comon. Pour cela, nous prouvons la décidabilité d'un ensemble de règles d'inférences qui est une axiomatisation correcte, bien que incomplète, de l'indistingabilité calculatoire, lorsque l'on utilise un schéma de chiffrement IND-CCA2. Du point de vue d'un cryptographe, cela peut être interprété comme la décidabilité d'un ensemble de transformations de jeux. / Our society extensively relies on communications systems. Because such systems are used to exchange sensitive information and are pervasive, they need to be secured. Cryptographic protocols are what allow us to have secure communications. It is crucial that such protocols do not fail in providing the security properties they claim, as failures have dire consequences. Unfortunately, designing cryptographic protocols is notoriously hard, and major protocols are regularly and successfully attacked. We argue that formal verification is the best way to get a strong confidence in a protocol security. Basically, the goal is to mathematically prove that a protocol satisfies some security property.Our objective is to develop techniques to formally verify equivalence properties of cryptographic protocols, using a method that provides strong security guarantees while being amenable to automated deduction techniques. In this thesis, we argue that the Bana-Comon model for equivalence properties meets these goals. We support our claim through three different contributions.First, we design axioms for the usual functions used in security protocols, and for several cryptographic hypothesis. Second, we illustrate the usefulness of these axioms and of the model by completing case studies of concrete protocols: we study two RFID protocols, KCL et LAK, as well as the 5G-AKA authentication protocol used in mobile communication systems. For each of these protocols, we show existing or new attacks against current versions, propose fixes, and prove that the fixed versions are secure. Finally, we study the problem of proof automation in the Bana-Comon model, by showing the decidability of a set of inference rules which is a sound, though incomplete, axiomatization of computational indistinguishability when using an IND-CCA2 encryption scheme. From a cryptographer's point of view, this can be seen as the decidability of a fixed set of cryptographic game transformations.