Cette these concerne la verification formelle et la composition de protocoles de securite, motivees en particulier par l'analyse des protocoles de vote electronique. Les chapitres 3 a 5 ont comme sujet la verification de protocoles de securite et le Chapitre 6 vise la composition.Nous montrons dans le Chapitre 3 comment reduire certains problemes d'une algebre quotient des termes a l'algebre libre des termes en utilisant des ensembles fortement complets de variants. Nous montrons que, si l'algebre quotient est donnee par un systeme de reecriture de termes convergent et optimalement reducteur (optimally reducing), alors des ensembles fortement complets de variants existent et sont finis et calculables.Dans le Chapitre 4, nous montrons que l'equivalence statique pour (des classes) de theories equationnelles, dont les theories sous-terme convergentes, la theorie de l'engagement a trappe (trapdoor commitment) et la theorie de signature en aveugle (blind signatures), est decidable en temps polynomial. Nous avons implemente de maniere efficace cette procedure.Dans le Chapitre 5, nous etendons la procedure de decision precedente a l'equivalence de traces. Nous utilisons des ensembles fortement complets de variants du Chapitre 3 pour reduire le probleme a l'algebre libre. Nous modelisons chaque trace du protocole comme une theorie de Horn et nous utilisons un raffinement de la resolution pour resoudre cette theorie. Meme si nous n'avons pas reussi a prouver que la procedure de resolution termine toujours, nous l'avons implementee et utilisee pour donner la premiere preuve automatique de l'anonymat dans le protocole de vote electronique FOO.Dans le Chapitre 6, nous etudions la composition de protocoles. Nous montrons que la composition de deux protocoles qui utilisent des primitives cryptographiques disjointes est sure s'ils ne revelent et ne reutilisent pas les secrets partages. Nous montrons qu'une forme d'etiquettage de protocoles est suffisante pour assurer la disjonction pour un ensemble fixe de primitives cryptographiques. / This thesis is about the formal verification and composition of security protocols, motivated by applications to electronic voting protocols. Chapters 3 to 5 concern the verification of security protocols while Chapter 6 concerns composition.We show in Chapter 3 how to reduce certain problems from a quotient term algebra to the free term algebra via the use of strongly complete sets of variants. We show that, when the quotient algebra is given by a convergent optimally reducing rewrite system, finite strongly complete sets of variants exist and are effectively computable.In Chapter 4, we show that static equivalence for (classes of) equational theories including subterm convergent equational theories, trapdoor commitment and blind signatures is decidable in polynomial time. We also provide an efficient implementation.In Chapter 5 we extend the previous decision procedure to handle trace equivalence. We use finite strongly complete sets of variants introduced in Chapter 3 to get rid of the equational theory and we model each protocol trace as a Horn theory which we solve using a refinement of resolution. Although we have not been able to prove that this procedure always terminates, we have implemented it and used it to provide the first automated proof of vote privacy of the FOO electronic voting protocol.In Chapter 6, we study composition of protocols. We show that two protocols that use arbitrary disjoint cryptographic primitives compose securely if they do not reveal or reuse any shared secret. We also show that a form of tagging is sufficient to provide disjointness in the case of a fixed set of cryptographic primitives.

Ce travail de recherche porte sur l’adoption de l’innovation et la lutte contre la fraude dans le paiement électronique du secteur bancaire tunisien, plus spécifiquement il vise l’exploration de la relation entre les composantes du marketing relationnel et les variables liées ; à l’individu, à la banque et au site marchand et leur impact sur l’intention d’utilisation des moyens de paiement électroniques dans les banques tunisiennes. L’objectif principal de ce travail étant la construction d’un modèle intégrateur qui illustre la relation entre le comportement du client et les facteurs influant l’adoption des moyens de paiement électroniques et la lutte contre la fraude. Sur le plan théorique, notre recherche a pour intérêt la contribution à l’amélioration des fondations sécuritaires pour les différents intervenants ainsi que le développement des moyens de paiement électronique. Sur le plan pratique l’intérêt de cette recherche est double, il s’agit de contribuer à la recherche sur les innovations dans le domaine d’e paiement d’une part et d’apprécier la relation entre les variables du MKG relationnel, l’adoption de l’innovation et la lutte contre la fraude monétique dans le domaine bancaire d’autre part. Notre stratégie de recherche adoptée suit une démarche quantitative selon un mode de raisonnement hypothético-déductif. La démarche est effectuée en trois itérations de terrain : une première à visée exploratoire, une deuxième confirmatoire et enfin une troisième dite complémentaire. Notre analyse des différentes itérations montre que l’engagement a un impact significatif sur l’intention d’utilisation des moyens de paiement et ce à l’image des recherches et des études antérieures. Ainsi, la perception de la qualité de service électronique (netqual) et la confiance ont un impact significatif sur l’engagement du consommateur à l’égard de l’utilisation des moyens électroniques en ligne. En renouvelant la lecture autour du concept de marketing relationnel par la mise en exergue du rôle de la satisfaction, la confiance et l’engagement comme variables clés dans la qualité de la relation, les principales contributions de cette recherche se présentent donc dans la proposition d’un modèle intégrateur combinant des variables qui autrefois ont fait l’objet des études séparées. / This research work explores innovative methods to fight fraudulent activity in electronic payment in the Tunisian banking sector, more specifically it aims to investigate the interrelation between the strategy of relationship marketing and the various involved parties: the individual, the bank and the merchant and their impact on the intention of employing electronic means of payment in Tunisian banks. The main objective of this work is to construct an integrative model, which illustrates the relationship between the customer's behavior and the factors, which lead to the adoption of electronic payment methods and fight against fraud. On the theoretical level, our research hopes to contribute to the improvement of the security foundations for the various stakeholders as well as the development of electronic payment methods. On the practical level, the aim of this study is twofold: (1) it contributes to the research on the innovations in the field of e-Payment (2) It values the link between the variables of the relational MKG, the adoption of innovative method and the fight against electronic fraudulent activities in the banking sector. Our adopted research strategy follows a quantitative approach based on the hypo-deductive reasoning method. The approach is carried out in three stages: an exploration stage, a confirmation stage and finally a complementary stage. Our analysis of the different stages demonstrates that commitment has a significant impact on the intention to employ the means of payment, as it has been already suggested by previous research studies. The research, however, suggests an integrative model which combines variables that have previously studied separately. Thus, the perception of the quality of electronic service (Netqual) and trust have a significant impact on the consumer's commitment to the use of electronic means online. Hence, a successful revamping of the strategy of relationship marketing should underscore the role of satisfaction, trust, and commitment as key variables in the quality of interactions.

Plusieurs accidents nucléaires majeurs ont montré la dangerosité de l’industrie nucléaire civile. En droit, les efforts de l’AIEA ont consisté depuis l’origine à développer la sûreté nucléaire. L’objectif est d’assurer le fonctionnement des installations dans de bonnes conditions. La sécurité qui vise à protéger les installations contre des actes malveillants est plus récente. La police et les forces de sécurité en général, sont en charge de la protection des installations contre les menaces criminelles. Si les installations fixes constituent la partie la mieux identifiée du problème, la circulation des sources radioactives dans le monde est le point faible du dispositif industriel. Les règlementations de plus en plus complexes doivent être appréciées en fonction d’une réalité simple : les forces de police ne sont pas mieux protégées que le reste de la population en cas d’accident majeur. Ce constat oblige à déployer des moyens importants dans le domaine de la prévention et de la planification. Les effets massifs d’une urgence radiologique ne reconnaissent pas les frontières des États. La dimension internationale de cette menace est incontestable. Les forces de police préparent les plans d’évacuation des populations. Mais les rayonnements invisibles mortels constituent des défis pour leur mise en œuvre. En réalité, les évacuations pratiquées ces dernières années ont toutes présentées des différences sensibles par rapport aux prévisions. Il ne s’agit pas d’une réflexion théorique sur le droit et les faits. Dans la perspective future d’une attaque terroriste sur une centrale, les moyens de la réponse sécuritaire sont devenus essentiels à la survie des sociétés modernes. / Several major nuclear accidents have shown the dangerousness of the civilian nuclear industry. In law, the IAEA's efforts have been, since the beginning, to develop nuclear safety. The objective is to ensure the operation of the facilities in good conditions. Security which aims to protect facilities against malicious acts is more recent. Police and security forces in general are in charge of protecting the facilities against criminal threats. If fixed installations are the best identified part of the problem, the circulation of radioactive sources in the world is the weak point of the industrial device. Increasingly complex regulations must be assessed according to a simple reality: police forces are not better protected than the rest of the population in the event of a major accident. This observation requires to deploy significant resources in the area of prevention and planning. The massive effects of a radiological emergency do not recognize the borders of states. The international dimension of this threat is indisputable. Police forces prepare evacuation plans for the population. But deadly invisible radiation constitutes a challenge for their implementation. In fact, the evacuations carried out in recent years have all presented significant differences compared to the forecasts. It is not a theoretical reflection on the law and the facts. In the future prospect of a terrorist attack on a power station, the safety response means have become essential to the survival of modern societies.

No description available.

Les noyaux de systèmes d'exploitation manipulent des données fournies par les programmes utilisateur via les appels système. Si elles sont manipulées sans prendre une attention particulière, une faille de sécurité connue sous le nom de Confused Deputy Problem peut amener à des fuites de données confidentielles ou l'élévation de privilèges d'un attaquant. Le but de cette thèse est d'utiliser des techniques de typage statique afin de détecter les manipulations dangereuses de pointeurs contrôlés par l'espace utilisateur. La plupart des systèmes d'exploitation sont écrits dans le langage C. On commence par en isoler un sous-langage sûr nommé Safespeak. Sa sémantique opérationnelle et un premier système de types sont décrits, et les propriétés classiques de sûreté du typage sont établies. La manipulation des états mémoire est formalisée sous la forme de lentilles bidirectionnelles, qui permettent d'encoder les mises à jour partielles des états et variables. Un première analyse sur ce langage est décrite, permettant de distinguer les entiers utilisés comme bitmasks, qui sont une source de bugs dans les programmes C. / Operating system kernels need to manipulate data that comes from user programs through system calls. If it is done in an incautious manner, a security vulnerability known as the Confused Deputy Problem can lead to information disclosure or privilege escalation. The goal of this thesis is to use static typing to detect the dangerous uses of pointers that are controlled by userspace. Most operating systems are written in the C language. We start by isolating Safespeak, a safe subset of it. Its operational semantics as well as a type system are described, and the classic properties of type safety are established. Memory states are manipulated using bidirectional lenses, which can encode partial updates to states and variables. A first analysis is described, that identifies integers used as bitmasks, which are a common source of bugs in C programs. Then, we add to Safespeak the notion of pointers coming from userspace. This breaks type safety, but it is possible to get it back by assigning a different type to the pointers that are controlled by userspace. This distinction forces their dereferencing to be done in a controlled fashion. This technique makes it possible to detect two bugs in the Linux kernel: the first one is in a video driver for an AMD video card, and the second one in the ptrace system call for the Blackfin architecture.

À mesure que le nombre d’objets capables de communiquer croît, le besoin de sécuriser leurs interactions également. La conception des protocoles cryptographiques nécessaires pour cela est une tâche notoirement complexe et fréquemment sujette aux erreurs humaines. La vérification formelle de protocoles entend offrir des méthodes automatiques et exactes pour s’assurer de leur sécurité. Nous nous intéressons en particulier aux méthodes de vérification automatique des propriétés d’équivalence pour de tels protocoles dans le modèle symbolique et pour un nombre non borné de sessions. Les propriétés d’équivalences ont naturellement employées pour s’assurer, par exemple, de l’anonymat du vote électronique ou de la non-traçabilité des passeports électroniques. Parce que la vérification de propriétés d’équivalence est un problème complexe, nous proposons dans un premier temps deux méthodes pour en simplifier la vérification : tout d’abord une méthode pour supprimer l’utilisation des nonces dans un protocole tout en préservant la correction de la vérification automatique; puis nous démontrons un résultat de typage qui permet de restreindre l’espace de recherche d’attaques sans pour autant affecter le pouvoir de l’attaquant. Dans un second temps nous exposons trois classes de protocoles pour lesquelles la vérification de l’équivalence dans le modèle symbolique est décidable. Ces classes bénéficient des méthodes de simplification présentées plus tôt et permettent d’étudier automatiquement des protocoles taggués, avec ou sans nonces, ou encore des protocoles ping-pong. / As the number of devices able to communicate grows, so does the need to secure their interactions. The design of cryptographic protocols is a difficult task and prone to human errors. Formal verification of such protocols offers a way to automatically and exactly prove their security. In particular, we focus on automated verification methods to prove the equivalence of cryptographic protocols for a un-bounded number of sessions. This kind of property naturally arises when dealing with the anonymity of electronic votingor the untracability of electronic passports. Because the verification of equivalence properties is a complex issue, we first propose two methods to simplify it: first we design a transformation on protocols to delete any nonce while maintaining the soundness of equivalence checking; then we prove a typing result which decreases the search space for attacks without affecting the power of the attacker. Finally, we describe three classes of protocols for which equivalence is decidable in the symbolic model. These classes benefit from the simplification results stated earlier and enable us to automatically analyze tagged protocols with or without nonces, as well as ping-pong protocols.

Autant les applications Android ont réussi à positionner Android parmi les systèmes d'exploitation les plus utilisés, autant elles ont facilité aux créateurs de maliciels de s'introduire et de compromettre ses appareils. Une longue liste de menaces causées par les applications téléchargées vise l'intégrité du système et la vie privée de ses utilisateurs. Malgré l'évolution incessante du système Android pour améliorer son mécanisme de sécurité, le niveau de sophistication des logiciels malveillants a augmenté et s'adapte continuellement avec les nouvelles mesures. L'une des principales faiblesses menaçant la sécurité de ce système est le manque abyssal d'outils et d'environnements permettant la spécification et la vérification formelle des comportements des applications avant que les dommages ne soient causés. À cet égard, les méthodes formelles semblent être le moyen le plus naturel et le plus sûr pour une spécification et une vérification rigoureuses et non ambiguës de telles applications. Notre objectif principal est de développer un cadre formel pour le renforcement de politiques de sécurité dans les applications Android. L'idée est d'établir une synergie entre le paradigme orienté aspect et les méthodes formelles. L'approche consiste à réécrire le programme de l'application en ajoutant des tests de sécurité à certains points soigneusement sélectionnés pour garantir le respect de la politique de sécurité. La version réécrite du programme préserve tous les bons comportements de la version originale qui sont conformes à la politique de sécurité et agit contre les mauvais. / As much as they have positioned Android among the most widely used operating systems, Android applications have helped malware creators to break in and infect its devices. A long list of threats caused by downloaded applications targets the integrity of the system and the privacy of its users. While the Android system is constantly evolving to improve its security mechanism, the malware's sophistication level is skyrocketing and continuously adapting with the new measures. One of the main weaknesses threatening smartphone security is the abysmal lack of tools and environments that allow formal specification and verification of application behaviors before damage is done. In this regard, formal methods seem to be the most natural and secure way for rigorous and unambiguous specification and verification of such applications. Our ultimate goal is to formally enforce security policies on Android applications. The main idea is to establish a synergy between the aspect-oriented paradigm and formal methods such as the program rewriting technique. The approach consists of rewriting the application program by adding security tests at certain carefully selected points to ensure that the security policy is respected. The rewritten version of the program preserves all the good behaviors of the original one that comply with the security policy and acts against the bad ones.

Thèse diffusée initialement dans le cadre d'un projet pilote des Presses de l'Université de Montréal/Centre d'édition numérique UdeM (1997-2008) avec l'autorisation de l'auteur. / Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal. / Notre thèse poursuit trois grands objectifs. Premièrement, elle vise à ana­lyser le processus et les formes de désengagement du gouvernement canadien dans le domaine de la sécurité du revenu entre 1975 et 1995. Deuxièmement, elle vise à comparer les approches et stratégies que le gouvernement fédéral a poursuivies au cours de cette période de façon à se désengager de certaines obligations financières envers les citoyens, telles qu'assurées par quatre grands programmes de sécurité du revenu, en relation avec les obstacles politiques au désengagement pour chaque programme. Troisièmement, enfin, elle vise à éta­blir les principales distinctions entre le processus politique de l'expansion de l'État providence canadien (1950 à 1974) et celui du désengagement (depuis 1975). Nous avons adapté le modèle théorique élaboré par Paul Pierson dans J'ouvrage Dismant/ing the Welfare State? en tenant compte de la spécificité du cas canadien. Nous soutenons trois grandes propositions. Premièrement, la ca.: pacité des dirigeants de poursuivre des stratégies efficaces de longue haleine pour contourner les obstacles au désengagement et minimiser la réprimande électorale apparaît plus importante que celle qu'on leur reconnaît dans la littéra­ture. Nous soutenons qu'à longue échéance, les stratégies poursuivies font en sorte que tous les programmes sont vulnérables au désengagement et sujets à une redéfinition significative des droits. Deuxièmement, les dirigeants poursuivent des stratégies et modifient leur approche vis-à-vis de la sécurité du revenu sur plusieurs années, si bien que l'efficacité des formes de rétroaction des politiques, qui apparaissent centrales au début du processus pour ralentir ou résister aux initiatives de désengagement, ne garantissent pas nécessairement l'intégrité du programme à longue échéance. Nous soutenons que /es dirigeants poursuivent avec succès des stratégies de longue haleine, adaptées à la nature du terrain politique de chaque programme, pour contourner les obstacles au désengage­ment et minimiser les coûts politiques de ce dernier. Troisièmement, nous soute­nons qu'au Canada, comme en Grande-Bretagne et aux États-Unis, /a dynami­que du processus de désengagement, ne correspond pas simplement à celle, renversée, de l'expansion. Notamment, le rôle des provinces, des élites adminis­tratives et des groupes d'intérêt s'est métamorphosé. Notre thèse s'appuie principalement sur des sources secondaires. Elle ne vise pas à produire de nouvelles données empiriques mais elle avance une inter­prétation originale et systématique des données disponibles. Pour opérationna­liser le concept du désengagement comme variable dépendante, nous avons re­cours à l'analyse de la composition et de l'évolution des dépenses, jouxtée à l'analyse des dispositions budgétaires et législatives. Nous tenons compte de la régression passée ou imminente de la sécurité du revenu. Les résultats de notre étude du cas canadien ont des implications pour l'étude de la politique canadienne de la sécurité du revenu, pour la littérature comparée sur l'État providence, ainsi que des implications méthodologiques pour l'étude du processus actuel. D'abord, au Canada, il est indéniable que, histori­quement, le fédéralisme et les objectifs d'intégration nationale ont laissé une em­preinte forte sur les programmes de sécurité du revenu. Toutefois, pendant le processus de désengagement, la "spécificité canadienne" est beaucoup moins caractérisée par ces deux facteurs. De plus, on ne peut pas affirmer qu'elle se caractérise toujours par le rôle effacé des groupes de la société. Ensuite, pour la littérature comparée sur l'État providence, le cas canadien fournit un exemple où les stratégies politiques de désengagement poursuivies pendant plusieurs an­nées ont fonctionné et où les programmes ont été réorientés fondamentalement. Il suggère l'hypothèse que les travaux de Pierson ont attribué une importance indue au processus de rétroaction des politiques comme facteur de résistance au désengagement en même temps qu'ils sous-estimaient le succès potentiel, à longue échéance, des stratégies politiques. Enfin, nos résultats ont une implica­tion méthodologique significative. Nous croyons que le succès des stratégies po­litiques de désengagement, au Canada, n'est pas attribuable principalement à la singularité de l'expérience canadienne (par rapport à la Grande-Bretagne et aux États-Unis). Elle s'explique plutôt par une opérationnalisation inadéquate de la va­riable dépendante, dans les premiers travaux sur le retrait de l'État providence, et par une période d'observation restreinte et un déficit d'attention portée aux réfor­mes progressives chez Pierson.

« Thèse présentée à l'École des gradués de l'Université Laval pour l'obtention du grade de maître ès arts (M.A.) »

Ce mémoire étudie la relation entre les concepts de régionalisme et de convergence des politiques. L'hypothèse avancée est que le régionalisme constitue un moteur à la convergence des politiques entre les États membres d'un même bloc régional. Le cas étudié est l'Amérique du Nord, plus particulièrement l'intégration entre le Canada et les États-Unis de 1980 à 2005, et nous examinons les politiques liées au contrôle frontalier. Nous examinons donc les impacts qu'ont eus l'ALÉ et l'ALÉNA principalement sur les politiques canadiennes et américaines de sécurité à leur frontière commune. Nos résultats confirment partiellement notre hypothèse étant donné que plusieurs politiques similaires ont été adoptées après l'entrée en vigueur de l'ALÉNA en 1994. Toutefois, l'accélération du processus de convergence après le 11 septembre 2001 ne semble pas avoir été causée spécifiquement par le régionalisme. C'est plutôt les attentats terroristes qui expliquent le rapprochement institutionnel entre le Canada et les États-Unis jusqu'en 2005. Malgré tout, le régionalisme a joué un rôle de 2001 à 2005, mais celui-ci s'est plutôt avéré indirect.