This paper describes four tools for verification security protocols Athena, Casper, Isabelle and Murphi. Each tool is briefly characterized and implementation of protocol Needham Schroeder. One part of this paper is comparing of selected tools. The second part of this paper describes in detail a tool Athena and mentions examples of verified protocols. By each protocol is stated a specifications of communication, a detected attack and results of own verification. At the end compares this paper verification results with already publicated attacks.

Sensor networks are innovative wireless networks consisting of a large number of low-cost, resource-constrained sensor nodes that collect, process, and transmit data in a distributed and collaborative way. There are numerous applications for wireless sensor networks, and security is vital for many of them. However, sensor nodes suffer from many constraints, including low computation capability, small memory, limited energy resources, susceptibility to physical capture, and the lack of infrastructure, all of which impose formidable security challenges and call for innovative approaches. In this thesis, we present our research results on three important aspects of securing sensor networks: lightweight entity authentication, distributed node clone detection, and secure data aggregation. As the technical core of our lightweight authentication proposals, a special type of circulant matrix named circulant-P2 matrix is introduced. We prove the linear independence of matrix vectors, present efficient algorithms on matrix operations, and explore other important properties. By combining circulant-P2 matrix with the learning parity with noise problem, we develop two one-way authentication protocols: the innovative LCMQ protocol, which is provably secure against all probabilistic polynomial-time attacks and provides remarkable performance on almost all metrics except one mild requirement for the verifier's computational capacity, and the HB$^C$ protocol, which utilizes the conventional HB-like authentication structure to preserve the bit-operation only computation requirement for both participants and consumes less key storage than previous HB-like protocols without sacrificing other performance. Moreover, two enhancement mechanisms are provided to protect the HB-like protocols from known attacks and to improve performance. For both protocols, practical parameters for different security levels are recommended. In addition, we build a framework to extend enhanced HB-like protocols to mutual authentication in a communication-efficient fashion. Node clone attack, that is, the attempt by adversaries to add one or more nodes to the network by cloning captured nodes, imposes a severe threat to wireless sensor networks. To cope with it, we propose two distributed detection protocols with difference tradeoffs on network conditions and performance. The first one is based on distributed hash table, by which a fully decentralized, key-based caching and checking system is constructed to deterministically catch cloned nodes in general sensor networks. The protocol performance of efficient storage consumption and high security level is theoretically deducted through a probability model, and the resulting equations, with necessary adjustments for real application, are supported by the simulations. The other is the randomly directed exploration protocol, which presents notable communication performance and minimal storage consumption by an elegant probabilistic directed forwarding technique along with random initial direction and border determination. The extensive experimental results uphold the protocol design and show its efficiency on communication overhead and satisfactory detection probability. Data aggregation is an inherent requirement for many sensor network applications, but designing secure mechanisms for data aggregation is very challenging because the aggregation nature that requires intermediate nodes to process and change messages, and the security objective to prevent malicious manipulation, conflict with each other to a great extent. To fulfill different challenges of secure data aggregation, we present two types of approaches. The first is to provide cryptographic integrity mechanisms for general data aggregation. Based on recent developments of homomorphic primitives, we propose three integrity schemes: a concrete homomorphic MAC construction, homomorphic hash plus aggregate MAC, and homomorphic hash with identity-based aggregate signature, which provide different tradeoffs on security assumption, communication payload, and computation cost. The other is a substantial data aggregation scheme that is suitable for a specific and popular class of aggregation applications, embedded with built-in security techniques that effectively defeat outside and inside attacks. Its foundation is a new data structure---secure Bloom filter, which combines HMAC with Bloom filter. The secure Bloom filter is naturally compatible with aggregation and has reliable security properties. We systematically analyze the scheme's performance and run extensive simulations on different network scenarios for evaluation. The simulation results demonstrate that the scheme presents good performance on security, communication cost, and balance.

Sensor networks are innovative wireless networks consisting of a large number of low-cost, resource-constrained sensor nodes that collect, process, and transmit data in a distributed and collaborative way. There are numerous applications for wireless sensor networks, and security is vital for many of them. However, sensor nodes suffer from many constraints, including low computation capability, small memory, limited energy resources, susceptibility to physical capture, and the lack of infrastructure, all of which impose formidable security challenges and call for innovative approaches. In this thesis, we present our research results on three important aspects of securing sensor networks: lightweight entity authentication, distributed node clone detection, and secure data aggregation. As the technical core of our lightweight authentication proposals, a special type of circulant matrix named circulant-P2 matrix is introduced. We prove the linear independence of matrix vectors, present efficient algorithms on matrix operations, and explore other important properties. By combining circulant-P2 matrix with the learning parity with noise problem, we develop two one-way authentication protocols: the innovative LCMQ protocol, which is provably secure against all probabilistic polynomial-time attacks and provides remarkable performance on almost all metrics except one mild requirement for the verifier's computational capacity, and the HB$^C$ protocol, which utilizes the conventional HB-like authentication structure to preserve the bit-operation only computation requirement for both participants and consumes less key storage than previous HB-like protocols without sacrificing other performance. Moreover, two enhancement mechanisms are provided to protect the HB-like protocols from known attacks and to improve performance. For both protocols, practical parameters for different security levels are recommended. In addition, we build a framework to extend enhanced HB-like protocols to mutual authentication in a communication-efficient fashion. Node clone attack, that is, the attempt by adversaries to add one or more nodes to the network by cloning captured nodes, imposes a severe threat to wireless sensor networks. To cope with it, we propose two distributed detection protocols with difference tradeoffs on network conditions and performance. The first one is based on distributed hash table, by which a fully decentralized, key-based caching and checking system is constructed to deterministically catch cloned nodes in general sensor networks. The protocol performance of efficient storage consumption and high security level is theoretically deducted through a probability model, and the resulting equations, with necessary adjustments for real application, are supported by the simulations. The other is the randomly directed exploration protocol, which presents notable communication performance and minimal storage consumption by an elegant probabilistic directed forwarding technique along with random initial direction and border determination. The extensive experimental results uphold the protocol design and show its efficiency on communication overhead and satisfactory detection probability. Data aggregation is an inherent requirement for many sensor network applications, but designing secure mechanisms for data aggregation is very challenging because the aggregation nature that requires intermediate nodes to process and change messages, and the security objective to prevent malicious manipulation, conflict with each other to a great extent. To fulfill different challenges of secure data aggregation, we present two types of approaches. The first is to provide cryptographic integrity mechanisms for general data aggregation. Based on recent developments of homomorphic primitives, we propose three integrity schemes: a concrete homomorphic MAC construction, homomorphic hash plus aggregate MAC, and homomorphic hash with identity-based aggregate signature, which provide different tradeoffs on security assumption, communication payload, and computation cost. The other is a substantial data aggregation scheme that is suitable for a specific and popular class of aggregation applications, embedded with built-in security techniques that effectively defeat outside and inside attacks. Its foundation is a new data structure---secure Bloom filter, which combines HMAC with Bloom filter. The secure Bloom filter is naturally compatible with aggregation and has reliable security properties. We systematically analyze the scheme's performance and run extensive simulations on different network scenarios for evaluation. The simulation results demonstrate that the scheme presents good performance on security, communication cost, and balance.

This paper analyses some existing approaches in security and payment protocol design. It describes protocol design using simple BAN logic and using derivation system. Special attention is paid to composition method, which is based on the design of complicated protocols from small parts called primitives and it is demonstrated on design of purchase procedure of SET protocol. This method was automated and implemented in C++ language, which allows designer to generate set of candidate protocols according to his needs and this set can be further used for next phase of protocol design process.

An understanding of cryptographic protocols requires that we examine the knowledge of protocol participants and adversaries: When a participant receives a message, does she know who sent it? Does she know that the message is fresh, and not merely a replay of some old message? Does a network spy know who is talking to whom? This thesis studies logics of knowledge and cryptography. Specifically, the thesis addresses the problem of how to make the concept of knowledge reflect feasible computability within a Kripke-style semantics. The main contributions are as follows. 1. A generalized Kripke semantics for first-order epistemic logic and cryptography, where the later is modeled using private constants and arbitrary cryptographic operations, as in the Applied Pi-calculus. 2. An axiomatization of first-order epistemic logic which is sound and complete relative to an underlying theory of cryptographic terms, and to an omega-rule for quantifiers. Besides standard axioms and rules from first-order epistemic logic, the axiomatization includes some novel axioms for the interaction between knowledge and cryptography. 3. Epistemic characterizations of static equivalence and Dolev-Yao message deduction. 4. A generalization of Kripke semantics for propositional epistemic logic and symmetric cryptography. 5. Decidability, soundness and completeness for propositional BAN-like logics with respect to message passing systems. Completeness and decidability are generalised to logics induced from an arbitrary base of protocol specific assumptions. 6. An epistemic definition of message deduction. The definition lies between weaker and stronger versions of Dolev-Yao deduction, and coincides with weaker Dolev-Yao regarding all atomic messages. For composite messages, the definition withstands a well-known counterexample to Dolev-Yao deduction. 7. Protocol examples using mixes, a Crowds style protocol, and electronic payments. / QC 20100524

Les solucions proposades en els articles científics sobre els intercanvis electrònics entre dues parts sovint involucren terceres parts (TTPs) per resoldre i simplificar el problema, però els usuaris hi han de dipositar una certa confiança. Ara bé, la confiança no és garantia ferma del compliment dels requisits de seguretat. Per això, molts usuaris són reticents a dipositar confiança en entitats remotes, fet que en dificulta l'ús. Aquí mostram com, a partir d'un determinat protocol de seguretat, podem aconseguir que la TTP involucrada sigui verificable. Construïm un entorn de confiança dins del protocol per mitjà del subministrament d'evidències sobre cada una de les operacions de la TTP (definim i introduïm la verificabilitat on-line de la TTP). Aconseguim això gràcies a la detecció, l'anàlisi i la classificació de cada una de les accions de la TTP. Aportam unes orientacions de disseny que faciliten la introducció de TTPs verificables dins dels protocols.

Made available in DSpace on 2016-08-17T18:39:39Z (GMT). No. of bitstreams: 1 3802.pdf: 4112819 bytes, checksum: e42717f19397f311cb6978ed3341685c (MD5) Previous issue date: 2010-10-29 / For centuries, infectious agents have been used as weapons in armed conflicts. In 1972 the Biological Weapons Convention prohibited the creation and stockpiling of biological weapons. However, some countries continued to research and develop these weapons. Proof of this fact was the crash in 1979 in a military factory in the USSR, where Bacillus anthracis were dispersed. Biotechnology in a globalizing world facilitates and contributes not only to the development of weapons programs of regular armies, but also to terrorist groups. Examples of such this are the contamination by the bacterium Salmonella typhimurium by a religious fanatic group that in 1984 poisoned 751 people in the U.S., and the bacterium Bacillus anthracis spores mailed in the U.S. to several people during 2001 and 2002, immediately after the attacks of September 11th. A biological weapon is of extreme difficult detection by security equipment. Most infectious agents are present in almost every continent, making it easier to obtain. The production is cheap and it is easy to carry, being a small amount enough to reach very large area and thousands of people. It is an invisible weapon, odorless and causes symptoms unknown to most physicians. So, given this background, in this master thesis we attempt to demonstrate the reality of the threat of a biological weapon based on Anthrax as the biological agent used as a weapon of mass destruction. Based on this study, we show the fragility of the state system for dealing with such incidents, and we propose security protocols in order to regulate what should be done in time of crisis, defining its management and streamline the decision-making. Finally, using the technique of molecular docking, we also studied the lethal factor of anthrax, and proposed the compound 1-Phenylsulfonyl-2-propanone (DARXOJ, C9H10O3S) as a good candidate to inhibit its effects. / Há séculos agentes infecciosos são utilizados como armas em conflitos bélicos. Em 1972 a Convenção sobre Armas Biológicas proibiu a criação e armazenamento de armas biológicas. No entanto alguns países continuaram a pesquisa e o desenvolvimento dessas armas. Prova desse fato foi o acidente em 1979 em uma fábrica militar na URSS, onde foram dispersos esporos de Bacillus anthracis. A Biotecnologia no mundo globalizado facilita e contribui não apenas aos programas de desenvolvimento de armas dos exércitos regulares, mas também aos grupos terroristas. Exemplos disso são a intoxicação pela bactéria Salmonella typhimurium por um grupo fanático religioso que em 1984, nos EUA, intoxicou 751 pessoas, e os esporos da bactéria Bacillus anthracis enviados pelo correio para várias pessoas em 2001 e 2002, imediatamente após os atentados de 11 de setembro nos EUA. Uma arma biológica é muito difícil de ser detectada por equipamento de segurança. A maioria dos agentes infecciosos está presente em quase todos os continentes, o que facilita a sua obtenção. A produção é barata e simples de transportar, podendo atingir com pequena quantidade área muito grande e milhares de pessoas. É uma arma invisível, inodora e que provoca sintomas desconhecidos pela maioria dos médicos. Em face desse panorama, neste trabalho procuramos demonstrar a realidade da ameaça de uma arma biológica e elegemos o Antraz como agente biológico utilizado como arma de destruição em massa. Neste estudo, mostramos a fragilidade do sistema estatal para lidar com este tipo de incidente, e propomos protocolos de segurança com o objetivo de regular os procedimentos no momento de crise, definindo o gerenciamento para melhorar e otimizar as tomadas de decisões. Finalmente, por meio do uso da técnica de docking molecular, também estudamos o fator letal do Antraz, e propusemos o composto 1-Fenilsulfonil-2-propanona (DARXOJ, C9H10O3S) como um bom candidato a inibir os seus efeitos.

Original protocols, which were created during early development of computer networks, no longer provide sufficient security. This is the reason why new protocols are developed and implemented. The important component of this process is formal verification, which is used to analyze the developed protocols and check whether a successful attack is possible or not. This thesis presents selected security protocols and tools for their formal verification. Further, the selected protocols are specified in LySa calculus and results of their analysis using LySatool are presented and discussed.

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.

Made available in DSpace on 2016-04-04T18:31:27Z (GMT). No. of bitstreams: 1 Manoel Peluso de Carvalho Filho.pdf: 1548469 bytes, checksum: 813f063c4ea17788aa795465c9e6e6f5 (MD5) Previous issue date: 2008-11-24 / Nowadays, the use of the wireless network technology has grown mainly motivated by the price of equipments, ease of installation, network maintenance and expansion of technical safety. The more you use the wireless network resource, the better should be the treatment related to its safety aspect. As the security level increases, the amount of information transmitted between the equipment decreases. This thesis aims to analyze the performance of WLAN network with the implementation of WEP and WPA / TKIP security protocols in an environment that uses applications whose characteristic is to generate small packets on the network. The LanTraffic TM software is used to generate traffic and also to capture the transmission rate in Kbps that flows through the stations. Three scenarios are simulated varying in the distance between the equipments. For each scenario, a comparative study was made and the WLAN behavior without the security resource analyzed, then it was analyzed with the WEP fitted and finally with the WPA/TKIP configured. To develop the experiments it was used a WLAN network in a controlled environment in the Laboratory Research on Radio System in PUC Campinas. Therefore, there is not external interference in the signal transmitted by equipments. / A utiliza??o da tecnologia de rede sem fio tem crescido ultimamente motivado principalmente pelo pre?o dos equipamentos, facilidade de instala??o, manuten??o da rede e amplia??o das t?cnicas de seguran?a. Quanto mais se utiliza o recurso de rede sem fio maior tem de ser o tratamento em rela??o ao aspecto de seguran?a. A medida que aumenta o n?vel de seguran?a, decresce a quantidade de informa??o transmitida entre os equipamentos. Esse trabalho visa analisar o desempenho de rede WLAN(Wireless Local ?rea Network) com a implementa??o dos protocolos de seguran?a WEP(Wired Equivalent Privacy) e WPA/TKIP(WI-FI Protected Access / Temporal Key Integrity Protocol). ? utilizado o software LanTrafficTM para gerar tr?fego na rede e tamb?m para capturar a taxa de transmiss?o em Kbps trafegados entre as STAs. S?o emulados tr?s cen?rios variando a dist?ncia entre os equipamentos. Para cada cen?rio foi confeccionado um comparativo e analisado o comportamento da WLAN configurado sem seguran?a, com o WEP habilitado e finalmente com o WPA/TKIP configurado. Para executar os experimentos utilizou-se uma rede WLAN no laborat?rio de pesquisa em sistema de r?dio (LP-SiRa) da PUC Campinas em um ambiente controlado. Com isso n?o h? interfer?ncias na transmiss?o dos sinais emitidos pelos equipamentos Ou seja, sem interfer?ncia externa no sinal transmitido entre os equipamentos.