In his habilitation theses Steve Kremer presents some selected research results in the area of formal analysis of security protocols. His contributions include application of formal methods to electronic voting protocols and security APIs, automated methods for verifying equivalence properties, compositional reasoning for security protocols and computational soundness results.

Many security protocols are built as the composition of an application-layer protocol and a secure transport protocol, such as TLS. There are many approaches to proving the correctness of such protocols. One popular approach is verification by abstraction, in which the correctness of the application-layer protocol is proven under the assumption that the transport layer satisfies certain properties, such as confidentiality. Following this approach, we adapt the strand spaces model in order to analyse application-layer protocols that depend on an underlying secure transport layer, including unilaterally authenticating secure transport protocols, such as unilateral TLS. Further, we develop proof rules that enable us to prove the correctness of application-layer protocols that use either unilateral or bilateral secure transport protocols. We then illustrate these rules by proving the correctness of WebAuth, a single-sign-on protocol that makes extensive use of unilateral TLS. In this thesis we also present a full proof of the model's soundness. In particular, we prove that, subject to a suitable independence assumption, if there is an attack against the application-layer protocol when layered on top of a particular secure transport protocol, then there is an attack against the abstracted model of the application-layer protocol. In contrast to existing work in this area, the independence assumption consists of eight statically-checkable conditions, meaning that it can be checked statically, rather than having to consider all possible runs of the protocol. Lastly, we extend the model to allow protocols that consist of an arbitrary number of layers to be proven correct. In this case, we prove the correctness of the intermediate layers using the high-level strand spaces model, by abstracting away from the underlying transport-layers. Further, we extend the above soundness results in order to prove that the multi-layer approach is sound. We illustrate the effectiveness of our technique by proving the correctness of a couple of simple multi-layer protocols.

Les protocoles d'échange d'informations représentent un des grands domaines actuels de recherche en sécurité informatique, et sont entre autres à la base des mécanismes de commerce électronique. Ils sont par exemple nécessaires à la réalisation d'un achat en ligne, à la signature d'un contrat électronique et au courrier électronique recommandé. Dans ces exemples, les échanges d'informations consistent à échanger respectivement un objet électronique contre un paiement, des signatures digitales sur un même contrat, et un courrier électronique contre un accusé de réception. Informellement, un protocole mettant en oeuvre de tels types d'échanges est dit équitable si et seulement si à la fin du protocole soit l'échange d'information a eu lieu, soit aucune information (même en partie) n'a été échangée. Afin d'assurer cette propriété d'équité de manière efficace, et d'éviter ainsi des éventuels comportements malhonnêtes de la part des participants à l'échange d'informations qui chercheraient à nuire au bon déroulement du protocole, une tierce partie de confiance est utilisée. Un des buts de cette thèse est de discerner les tâches devant être assurées par une telle tierce partie de confiance et développer des méthodes permettant d'en minimiser le nombre et l'importance, afin de limiter la confiance que les entités effectuant l'échange doivent porter à cette tierce partie. Pour cela, nous identifions tout d'abord de manière générique quels sont ces types de tâches, puis nous analysons sous ce point de vue les principaux protocoles ayant été proposés dans la littérature. Cette démarche nous conduit ensuite naturellement à nous pencher sur les relations de confiance entre les participants à un protocole d'échange. Ce type de relations est particulièrement significatif pour des protocoles à plus de deux participants. Enfin, dans ce travail, nous observons à la lumière des aspects de confiance, les différentes propriétés propres aux protocoles d'échange, et nous proposons plusieurs nouveaux protocoles ayant des besoins en confiance limités.

Security protocols are important and widely used because they enable secure communication to take place over insecure networks. Over the years numerous formal methods have been developed to assist protocol designers by analysing models of these protocols to determine their security properties. Beyond the design stage however, developers rarely employ formal methods when implementing security protocols. This may result in implementation flaws often leading to security breaches. This dissertation contributes to the study of security protocol analysis by advancing the emerging field of implementation analysis. Two tools are presented which together translate between Java and the LySa process calculus. Elyjah translates Java implementations into formal models in LySa. In contrast, Hajyle generates Java implementations from LySa models. These tools and the accompanying LySa verification tool perform rapid static analysis and have been integrated into the Eclipse Development Environment. The speed of the static analysis allows these tools to be used at compile-time without disrupting a developer’s workflow. This allows us to position this work in the domain of practical software tools supporting working developers. As many of these developers may be unfamiliar with modelling security protocols a suite of tools for the LySa process calculus is also provided. These tools are designed to make LySa models easier to understand and manipulate. Additional tools are provided for performance modelling of security protocols. These allow both the designer and the implementor to predict and analyse the overall time taken for a protocol run to complete. Elyjah was among the very first tools to provide a method of translating between implementation and formal model, and the first to use either Java for the implementation language or LySa for the modelling language. To the best of our knowledge, the combination of Elyjah and Hajyle represents the first and so far only system which provides translation from both code to model and back again.

As redes de sensores sem fio (RSSF) são compostas por pequenos dispositivos distribuídos em uma região geográfica com a finalidade de monitorar ou interagir com o ambiente. Esse tipo de rede tem sido alvo de grande atenção da comunidade acadêmica e empresarial, dados os avanços das produções científicas e aplicações comerciais. Além disso, há grande potencial para esse modelo de rede, pois há diversos benefícios em se ter muitos dispositivos de baixo custo trabalhando em cooperação e que ainda podem interagir com o mundo real. As RSSFs apresentam novos desafios, até então inexistentes na maioria das redes modernas. A baixa capacidade de processamento dos dispositivos, a limitação do tamanho de um pacote, a baixa taxa de transferência de pacotes, a baixa capacidade da bateria de um dispositivo e o alcance limitado do rádio dificultam ou até inviabilizam muitas implementações de segurança. Neste sentido, há uma grande variedade de protocolos de segurança, os quais tentam fornecer o máximo de propriedades desejadas, como por exemplo autenticidade e confidencialidade de mensagens. Nesta dissertação, analisamos e comparamos dois pares de protocolos de segurança que possuem grande atenção da comunidade. Os protocolos foram analisados com base em seus mecanismos criptográficos e propriedades oferecidas. Além disso, com o uso de um simulador de RSSFs, realizamos experimentos que ajudam a entender o comportamento de dois protocolos, principalmente no que se relaciona com o consumo de energia dos dispositivos sensores. / Wireless Sensor Networks (WSNs) are formed by many tiny devices deployed for monitoring or interacting with the environment in a geografic area. This kind of network has received great attention in the academic and corporate community, given the advances of comercial applications and scientific developments. The benefits of having many low cost devices cooperating and interacting with the real world explain the great potential of such networks. The WSNs come with new challenges, so far not faced in modern networks. The low-power, low-processing devices, limited bandwidth and radio range make many security implementations difficult or even unfeasible. Within this context, there is a diversity of security protocols, intended to provide as many security properties as possible, like confidentiality and authentication of messages. In this master thesis, we compare and evaluate two pairs of security protocols that enjoy significant attention in the community. These protocols are evaluated based on their given properties and cryptographic primitives. Using a WSNs simulator, we performed experiments that help to understand the behavior of these two protocols, mainly for energy consumption purposes.

Recursive Inter-Network Architecture (RINA) networks have a shorter protocol stack than the current architecture (the Internet) and rely instead upon separation of mech- anism from policy and recursive deployment to achieve large scale networks. Due to this smaller protocol stack, fewer networking mechanisms, security or otherwise, should be needed to secure RINA networks. This thesis examines the security proto- cols included in the Internet Protocol Suite that are commonly deployed on existing networks and shows that because of the design principles of the current architecture, these protocols are forced to include many redundant non-security mechanisms and that as a consequence, RINA networks can deliver the same security services with substantially less complexity.

As redes de sensores sem fio (RSSF) são compostas por pequenos dispositivos distribuídos em uma região geográfica com a finalidade de monitorar ou interagir com o ambiente. Esse tipo de rede tem sido alvo de grande atenção da comunidade acadêmica e empresarial, dados os avanços das produções científicas e aplicações comerciais. Além disso, há grande potencial para esse modelo de rede, pois há diversos benefícios em se ter muitos dispositivos de baixo custo trabalhando em cooperação e que ainda podem interagir com o mundo real. As RSSFs apresentam novos desafios, até então inexistentes na maioria das redes modernas. A baixa capacidade de processamento dos dispositivos, a limitação do tamanho de um pacote, a baixa taxa de transferência de pacotes, a baixa capacidade da bateria de um dispositivo e o alcance limitado do rádio dificultam ou até inviabilizam muitas implementações de segurança. Neste sentido, há uma grande variedade de protocolos de segurança, os quais tentam fornecer o máximo de propriedades desejadas, como por exemplo autenticidade e confidencialidade de mensagens. Nesta dissertação, analisamos e comparamos dois pares de protocolos de segurança que possuem grande atenção da comunidade. Os protocolos foram analisados com base em seus mecanismos criptográficos e propriedades oferecidas. Além disso, com o uso de um simulador de RSSFs, realizamos experimentos que ajudam a entender o comportamento de dois protocolos, principalmente no que se relaciona com o consumo de energia dos dispositivos sensores. / Wireless Sensor Networks (WSNs) are formed by many tiny devices deployed for monitoring or interacting with the environment in a geografic area. This kind of network has received great attention in the academic and corporate community, given the advances of comercial applications and scientific developments. The benefits of having many low cost devices cooperating and interacting with the real world explain the great potential of such networks. The WSNs come with new challenges, so far not faced in modern networks. The low-power, low-processing devices, limited bandwidth and radio range make many security implementations difficult or even unfeasible. Within this context, there is a diversity of security protocols, intended to provide as many security properties as possible, like confidentiality and authentication of messages. In this master thesis, we compare and evaluate two pairs of security protocols that enjoy significant attention in the community. These protocols are evaluated based on their given properties and cryptographic primitives. Using a WSNs simulator, we performed experiments that help to understand the behavior of these two protocols, mainly for energy consumption purposes.

ITC/USA 2007 Conference Proceedings / The Forty-Third Annual International Telemetering Conference and Technical Exhibition / October 22-25, 2007 / Riviera Hotel & Convention Center, Las Vegas, Nevada / Networked based technologies (i.e. TCP/IP) have come to play an important role in the evolution of telemetry post processing services. A paramount issue when using networking to access/move telemetry data is security. In past years papers have focused on individual security technologies and how they could be used to secure telemetry data. This paper will review currently available network based security technologies, update readers on enhancements, and discuss their appropriate uses in the various phases of telemetry post-processing and analysis activities.

As the popularity of wireless networks increases, so does the need to protect them. In recent years, many researchers have studied the limitations of the security mechanisms that protect wireless networks. There has also been much research in the power consumption introduced by the network card. Technologies such as CPU and memory are increasing and so is their need for power, but battery technology is increasing at a much slower rate, forming a“battery gap". Because of this, battery capacity plays a major role in the usability of the devices. Although the effect of the network communication on a mobile device's battery has been widely researched, there has been less research on the effect of the security profile on energy usage. In this thesis, we examine a method for analyzing trade-offs between energy and security proposed by Colon Osorio et al. This research describes a method to identify the most appropriate security profile for a given application, given battery constraints. The same method can also be used to discover the minimum battery capacity to maintain a minimum security profile for a predefined amount of time. Trade-offs and optimality are analyzed using a cost-energy function, CE, and security measure, SM. CE encompasses the energy required to use countermeasure M against a specific vulnerability, Vi, as well as the energy consumed in bulk transfer. SM is a numerical representation of the effectiveness of a set of security mechanisms which utilize the set of countermeasures to defend against a set of vulnerabilities. Using CE and SM, we can compare different security profiles using a trade-off model. Having defined such a framework, we investigate different instances and examples where the use of the model is helpful in accessing trade-offs between security obtained and energy consumed to achieve such security. This was first examined through an analytical study, followed by experimentation. The major contributions of this work are an energy-security trade-off model and its empirical validation. This work extends the empirical experimentation done by other researchers such as Potlapally et al., Karri et al., and Stemm and Katz on the relationship between energy and the security of wireless communications in battery-constrained devices.

As the next evolutionary step in digital communication systems, mobile ad hoc networks (MANETs) and their specialization like wireless sensor networks (WSNs) have been attracting much interest in both research and industry communities. In MANETs, network nodes can come together and form a network without depending on any pre-existing infrastructure and human intervention. Unfortunately, the salient characteristics of MANETs, in particular the absence of infrastructure and the constrained resources of mobile devices, present enormous challenges when designing security mechanisms in this environment. Without necessary measures, wireless communications are easy to be intercepted and activities of users can be easily traced. This thesis presents our solutions for two important aspects of securing MANETs, namely efficient key management protocols and fast implementations of cryptographic primitives on constrained devices. Due to the tight cost and constrained resources of high-volume mobile devices used in MANETs, it is desirable to employ lightweight and specialized cryptographic primitives for many security applications. Motivated by the design of the well-known Enigma machine, we present a novel ultra-lightweight cryptographic algorithm, referred to as Hummingbird, for resource-constrained devices. Hummingbird can provide the designed security with small block size and is resistant to the most common attacks such as linear and differential cryptanalysis. Furthermore, we also present efficient software implementations of Hummingbird on 4-, 8- and 16-bit microcontrollers from Atmel and Texas Instruments as well as efficient hardware implementations on the low-cost field programmable gate arrays (FPGAs) from Xilinx, respectively. Our experimental results show that after a system initialization phase Hummingbird can achieve up to 147 and 4.7 times faster throughput for a size-optimized and a speed-optimized software implementation, respectively, when compared to the state-of-the-art ultra-lightweight block cipher PRESENT on the similar platforms. In addition, the speed optimized Hummingbird encryption core can achieve a throughput of 160.4 Mbps and the area optimized encryption core only occupies 253 slices on a Spartan-3 XC3S200 FPGA device. Bilinear pairings on the Jacobians of (hyper-)elliptic curves have received considerable attention as a building block for constructing cryptographic schemes in MANETs with new and novel properties. Motivated by the work of Scott, we investigate how to use efficiently computable automorphisms to speed up pairing computations on two families of non-supersingular genus 2 hyperelliptic curves over prime fields. Our findings lead to new variants of Miller's algorithm in which the length of the main loop can be up to 4 times shorter than that of the original Miller's algorithm in the best case. We also generalize Chatterjee et al.'s idea of encapsulating the computation of the line function with the group operations to genus 2 hyperelliptic curves, and derive new explicit formulae for the group operations in projective and new coordinates in the context of pairing computations. Efficient software implementation of computing the Tate pairing on both a supersingular and a non-supersingular genus 2 curve with the same embedding degree of k = 4 is investigated. Combining the new algorithm with known optimization techniques, we show that pairing computations on non-supersingular genus 2 curves over prime fields use up to 55.8% fewer field operations and run about 10% faster than supersingular genus 2 curves for the same security level. As an important part of a key management mechanism, efficient key revocation protocol, which revokes the cryptographic keys of malicious nodes and isolates them from the network, is crucial for the security and robustness of MANETs. We propose a novel self-organized key revocation scheme for MANETs based on the Dirichlet multinomial model and identity-based cryptography. Firmly rooted in statistics, our key revocation scheme provides a theoretically sound basis for nodes analyzing and predicting peers' behavior based on their own observations and other nodes' reports. Considering the difference of malicious behaviors, we proposed to classify the nodes' behavior into three categories, namely good behavior, suspicious behavior and malicious behavior. Each node in the network keeps track of three categories of behavior and updates its knowledge about other nodes' behavior with 3-dimension Dirichlet distribution. Based on its own analysis, each node is able to protect itself from malicious attacks by either revoking the keys of the nodes with malicious behavior or ceasing the communication with the nodes showing suspicious behavior for some time. The attack-resistant properties of the resulting scheme against false accusation attacks launched by independent and collusive adversaries are also analyzed through extensive simulations. In WSNs, broadcast authentication is a crucial security mechanism that allows a multitude of legitimate users to join in and disseminate messages into the networks in a dynamic and authenticated way. During the past few years, several public-key based multi-user broadcast authentication schemes have been proposed in the literature to achieve immediate authentication and to address the security vulnerability intrinsic to μTESLA-like schemes. Unfortunately, the relatively slow signature verification in signature-based broadcast authentication has also incurred a series of problems such as high energy consumption and long verification delay. We propose an efficient technique to accelerate the signature verification in WSNs through the cooperation among sensor nodes. By allowing some sensor nodes to release the intermediate computation results to their neighbors during the signature verification, a large number of sensor nodes can accelerate their signature verification process significantly. When applying our faster signature verification technique to the broadcast authentication in a 4×4 grid-based WSN, a quantitative performance analysis shows that our scheme needs 17.7%~34.5% less energy and runs about 50% faster than the traditional signature verification method.