L'utilisabilité et la sécurité sont des éléments cruciaux dans le processus d'authentification des utilisateurs. L'un des défis majeurs auquel font face les organisations aujourd'hui est d'offrir des systèmes d'accès aux ressources logiques (par exemple, une application informatique) et physiques (par exemple, un bâtiment) qui soient à la fois sécurisées et utilisables. Afin d'atteindre ces objectifs, il faut d'abord mettre en œuvre les trois composantes indispensables que sont l'identification (c.-à-d., définir l'identité d'un utilisateur), l'authentification (c.-à-d., vérifier l'identité d'un utilisateur) et l'autorisation (c.-à-d., accorder des droits d'accès à un utilisateur). Plus particulièrement, la recherche en authentification de l'utilisateur est essentielle. Sans authentification, par exemple, des systèmes informatiques ne sont pas capables de vérifier si un utilisateur demandant l'accès à une ressource possède les droits de le faire. Bien que plusieurs travaux de recherche aient porté sur divers mécanismes de sécurité, très peu de recherches jusqu'à présent ont porté sur l'utilisabilité et la sécurité des méthodes d'authentification des utilisateurs. Pour cette raison, il nous paraît nécessaire de développer un protocole d'utilisabilité et de sécurité pour concevoir les méthodes d'authentification des utilisateurs. La thèse centrale de ce travail de recherche soutient qu'il y a un conflit intrinsèque entre la création de systèmes qui soient sécurisés et celle de systèmes qui soient facile d'utilisation. Cependant, l'utilisabilité et la sécurité peuvent être construites de manière synergique en utilisant des outils d'analyse et de conception qui incluent des principes d'utilisabilité et de sécurité dès l'étape d'Analyse et de Conception de la méthode d'authentification. Dans certaines situations il est possible d'améliorer simultanément l'utilisabilité et la sécurité en revisitant les décisions de conception prises dans le passé. Dans d'autres cas, il est plus avantageux d'aligner l'utilisabilité et la sécurité en changeant l'environnement régulateur dans lequel les ordinateurs opèrent. Pour cette raison, cette thèse a comme objectif principal non pas d'adresser l'utilisabilité et la sécurité postérieurement à la fabrication du produit final, mais de faire de la sécurité un résultat naturel de l'étape d'Analyse et de Conception du cycle de vie de la méthode d'authentification. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : authentification de l'utilisateur, utilisabilité, sécurité informatique, contrôle d'accès.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

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.

De nombreux mécanismes de sécurité ont été proposés pour les réseaux fixes et mobiles. Bien que ces mécanismes aient pu répondre à un ensemble d'exigences de sécurité, ils demeurent uniquement efficaces dans un contexte spécifique lié aux hypothèses et aux exigences restrictives qui ont été émises lors de la conception. Dans un premier temps, nous définissons une liste d'exigences en sécurité qui permet d'analyser les solutions de sécurité les plus déployées. Dans un second temps, nous proposons d'étendre le protocole SSL/TLS avec de nouveaux services. SSL/TLS est une solution de sécurité générique et transparente aux applications. Ainsi, il ne couvre pas les besoins spécifiques à certaines classes d'application telles que les applications de paiement sur Internet. Notre propositions d'intégrer le protocole d'échange des clés ISAKMP avec SSL/TLS permet de fournir, entre autres, la protection d'identité des utilisateurs et l'unification des associations de sécurité. Afin d'étendre l'utilisation de SSL/TLS vers les systèmes de paiement sur Internet, nous intégrons un module générique pour la génération d'une preuve de non répudiation dans le protocole SSL/TLS. Par ailleurs, toutes ces propositions restent, cernées par le problème d'interopérabilité avec les anciennes versions de chaque protocole. Ce qui rend la satisfaction de tous les besoins à travers un des protocoles existants irréalisables. Pour cela, nous proposons finalement de concevoir et de valider un nouveau protocole de sécurité qui intègre nativement l'évolution des protocoles de sécurité des échanges et des réseaux d'une manière performante. Nous avons appelé ce protocole SEP (Secure and Extensible Protocol)

Description de mes activités de recherche réalisées depuis plus de 20 ans.

La présente recherche propose un modèle de traduction automatique français-arabe contrôlée appliquée aux domaines à sécurité critique. C’est une recherche transverse qui traite à la fois des langues contrôlées et de la traduction automatique français-arabe, deux concepts intimement liés. Dans une situation de crise où la communication doit jouer pleinement son rôle, et dans une mondialisation croissante où plusieurs langues cohabitent, notre recherche montre que l’association de ces deux concepts est plus que nécessaire. Nul ne peut contester aujourd’hui la place prépondérante qu’occupe la sécurité dans le quotidien des personnes et les enjeux qu’elle représente au sein des sociétés modernes. Ces sociétés davantage complexes et interconnectées manifestent une vulnérabilité flagrante qui les oblige à repenser leurs moyens d’organisation et de protection dont les systèmes de communication. La communication langagière à l’aide de systèmes informatisés est l’une des formes de communication la plus souvent utilisée pour le transfert des connaissances nécessaires à l’accomplissement des tâches et le déroulement des diverses actions. Toutefois, et contrairement à une idée bien ancrée qui tend à associer les risques d’une mauvaise communication à l’oral uniquement, l’usage de la langue écrite peut lui aussi comporter des risques. En effet des messages mal écrits peuvent conduire à de réelles catastrophes et à des conséquences irréversibles notamment dans des domaines jugés sensibles tels que les domaines à sécurité critique. C’est dans ce contexte que s’inscrit notre recherche. Cette thèse est une approche novatrice dans les domaines des langues contrôlées et de la traduction automatique. Elle définit avec précision, en s’appuyant sur une analyse microsystémique de la langue et un travail en intension sur le corpus, des normes pour la rédaction de protocoles de sécurité et d’alertes ainsi que leur traduction automatique vers l’arabe. Elle apporte en effet des notions nouvelles à travers plusieurs procédés normatifs intervenant non seulement dans le processus de contrôle mais également dans le processus de traduction. Le système de traduction automatique français-arabe TACCT (Traduction Automatique Contrôlée Centre Tesnière) mis au point dans cette thèse est un système à base de règles linguistiques qui repose sur un modèle syntaxico-sémantique isomorphique issu des analyses intra- et interlangues entre le français et l’arabe. Il introduit de nouveaux concepts notamment celui des macrostructures miroir contrôlées, où la syntaxe et la sémantique des langues source et cible sont représentées au même niveau. / The result of our research is a proposal for a controlled French to Arabic machine translation model, applied to security critical domains. This cross-disciplinary research study covers controlled languages and French to Arabic machine translation, two intimately related concepts. In a situation of crisis where communication must play its full role, and in the context of increasing globalisation where many languages coexist, our research findings show that the combination of these two concepts is sorely needed. No one can deny today the predominant role played by security in people’s daily life and the significant challenges it presents in modern societies. These more and more complex and interconnected societies present evident vulnerabilities that force them to rethink their means of protection and in particular that of their communication systems. Language communication with computerised systems is one of the most widely used forms of communication for the transfer of knowledge required in carrying out and completing tasks and in the good conduct of various activities. However, and contrary to an entrenched idea that tends to associate the risk of poor communication only with oral transmission, the use of written language can also be subject to risk. Indeed, a protocol or an alert which is badly formulated can provoke serious accidents due to misunderstanding, in particular during a crisis and under stress. It is in this context that our research has been undertaken. Our thesis proposes an innovative approach in the fields of controlled language and machine translation in which, relying on a microsystemic analysis of the language and a study of the corpus in intension, precise standards are defined for writing and translating protocols and security alerts written in French automatically into Arabic. Indeed, new concepts are introduced by means of several normative methods involved not only in the controlling process but also in the machine translation process. The French to Arabic machine translation system TACCT (Traduction Automatique Contrôlée Centre Tesnière) developed during our research is a rule-based system based on an isomorphic syntactic and semantic model stemming from intra- and interlanguage analysis between French and Arabic. It introduces new concepts including controlled mirror macrostructures, where the syntax and semantics of the source and target languages are represented at the same level.