We prcscnt a general framework for constructing and analyzing authentication protocols in realistic models of communication networks.This framework provides a sound formalization for the authentication problem and suggests simple and attractive design principles for general authentication and key exchange protocols.The key element in our appronch io a modular treatment of the authentication problem in cryptographic protocols; thii applies to the definition of accurity, to the design of the protocols, and to their analysis.In particulnr, following this modular approach, we show how to systematically transform solutions that work in a model of idaalizcd authenticated communications into solutions that are secure in the realistic setting of communication channels controlled by an active adversary.Using these principles we construct and prove the security of simple and practical authentication and key-exchange protocols.In particular, we provide a security analysis of aomo well-known key exchange protocols (e.g.authenticated Dlfllc-Hcllman key exchange), and of some of the techniques underlying the design of several authentication protocols that are currently being deployed on a large scale for the Intornot Protocol and other applications.
We prcscnt a general framework for constructing and analyzing authentication protocols in realistic models of communication networks.This framework provides a sound formalization for the authentication problem and suggests simple and attractive design principles for general authentication and key exchange protocols.The key element in our appronch io a modular treatment of the authentication problem in cryptographic protocols; thii applies to the definition of accurity, to the design of the protocols, and to their analysis.In particulnr, following this modular approach, we show how to systematically transform solutions that work in a model of idaalizcd authenticated communications into solutions that are secure in the realistic setting of communication channels controlled by an active adversary.Using these principles we construct and prove the security of simple and practical authentication and key-exchange protocols.In particular, we provide a security analysis of aomo well-known key exchange protocols (e.g.authenticated Dlfllc-Hcllman key exchange), and of some of the techniques underlying the design of several authentication protocols that are currently being deployed on a large scale for the Intornot Protocol and other applications.
We present a general framework for constructing and analyzing authentication protocols in realistic models of communication networks. This framework provides a sound formalization for the authentication problem and suggests simple and attractive design principles for general authentication and key exchange protocols. The key element in our approach is a modular treatment of the authentication problem in cryptographic protocols; this applies to the definition of security, to the design of the protocols, and to their analysis. In particular, following this modular approach, we show how to systematically transform solutions that work in a model of idealized authenticated communications into solutions that are secure in the realistic setting of communication channels controlled by an active adversary. Using these principles we construct and prove the security of simple and practical authentication and key-exchange protocols. In particular, we provide a security analysis of some well-known key exchange protocols (e.g. authenticated Diffie-Hellman key exchange), and of some of the techniques underlying the design of several authentication protocols that are currently being
We consider the problem of authenticated group key exchange among n parties communicating over an insecure public network. A number of solutions to this problem have been proposed; however, all prior provably-secure solutions do not scale well and, in particular, require O (n) rounds. Our main contribution is the first scalable protocol for this problem along with a rigorous proof of security in the standard model under the DDH assumption; our protocol uses a constant number of rounds and requires only O (1) \full modular exponentiations per user. Toward this goal (and adapting work of Bellare, Canetti, and Krawczyk), we first present an efficient compiler that transforms any ngroup key-exchange protocol secure against a passive eavesdropper to an authenticated protocol which is secure against an active adversary who controls all communication in the network. This compiler adds only one round and O (1) communication (per user) to the original scheme. We then prove secure | against a passive adversary | a variant of the two-round group key-exchange protocol of Burmester and Desmedt. Applying our compiler to this protocol results in a provably-secure three-round protocol for authenticated group key exchange which also achieves forward secrecy.
This thesis is concerned with two security mechanisms: authenticated key transport and rational exchange protocols. These mechanisms are potential building blocks in the security architecture of a range of different services. Authenticated key transport protocols are used to build secure channels between entities, which protect their communications against eaves-dropping and alteration by an outside attacker. In contrast, rational exchange protocols can be used to protect the entities involved in an exchange transaction from each other. This is important, because often the entities do not trust each other, and both fear that the other will gain an advantage by misbehaving. Rational exchange protocols alleviate this problem by ensuring that a misbehaving party cannot gain any advantages. This means that misbehavior becomes uninteresting and it should happen only rarely. The thesis is focused on the construction of formal models for authenticated key transport and rational exchange protocols. In the first part of the thesis, we propose a formal model for key transport protocols, which is based on a logic of belief. Building on this model, we also propose an original systematic protocol construction approach. The main idea is that we reverse some implications that can be derived from the axioms of the logic, and turn them into synthesis rules. The synthesis rules can be used to construct a protocol and to derive a set of assumptions starting from a set of goals. The main advantage is that the resulting protocol is guaranteed to be correct in the sense that all the specified goals can be derived from the protocol and the assumptions using the underlying logic. Another important advantage is that all the assumptions upon which the correctness of the protocol depends are made explicit. The protocol obtained in the synthesis process is an abstract protocol, in which idealized messages that contain logical formulae are sent on channels with various access properties. The abstract protocol can then be implemented in several ways by replacing the idealized messages and the channels with appropriate bit strings and cryptographic primitives, respectively. We illustrate the usage of the logic and the synthesis rules through an example: We analyze an authenticated key transport protocol proposed in the literature, identify several weaknesses, show how these can be exploited by various attacks, and finally, we redesign the protocol using the proposed systematic approach. We obtain a protocol that resists against the presented attacks, and in addition, it is simpler than the original one. In the second part of the thesis, we propose an original formal model for exchange protocols, which is based on game theory. In this model, an exchange protocol is represented as a set of strategies in a game played by the protocol parties and the network that they use to communicate with each other. We give formal definitions for various properties of exchange protocols in this model, including rationality and fairness. Most importantly, rationality is defined in terms of a Nash equilibrium in the protocol game. The model and the formal definitions allow us to rigorously study the relationship between rational exchange and fair exchange, and to prove that fairness implies rationality (given that the protocol satisfies some further usual properties), but the reverse is not true in general. We illustrate how the formal model can be used for rigorous verification of existing protocols by analyzing two exchange protocols, and formally proving that they satisfy the definition of rational exchange. We also present an original application of rational exchange: We show how the concept of rationality can be used to improve a family of micropayment schemes with respect to fairness without substantial loss in efficiency. Finally, in the third part of the thesis, we extend the concept of rational exchange, and describe how similar ideas can be used to stimulate the nodes of a self-organizing ad hoc network for cooperation. More precisely, we propose an original approach to stimulate the nodes for packet forwarding. Like in rational exchange protocols, our design does not guarantee that a node cannot deny packet forwarding, but it ensures that it cannot gain any advantages by doing so. We analyze the proposed solution analytically and by means of simulation.
Key exchange protocols, first introduced by Diffie and Hellman in 1976, are one of the most widely-deployed cryptographic protocols. They allow two parties, that have never interacted before, to establish shared secrets. These shared cryptographic keys may subsequently be used to establish a secure communication channel. Use cases include the classic client-server setting that is for example at play when browsing the internet, but also chats via end-to-end-encrypted instant messaging applications. Security-wise, we generally demand of key exchange protocols to achieve key secrecy and authentication. While, informally, authentication ensures that the communicating parties have confidence in the identity of their peers, key secrecy ensures that any shared cryptographic key that is established via the key exchange protocol is only known to the participants in the protocol and can be used securely in cryptographic protocols, i.e., is sufficiently random. In 1993, Bellare and Rogaway gave a first formalization of key exchange protocol security that captures these properties with respect to powerful adversaries with full control over the network. Their model constitutes the basis of the many subsequent treatments of authenticated key exchange security, including the models presented in this thesis. The common methodological approach underlying all of these formalizations is the provable security paradigm, which has become a standard tool in assessing the security of cryptographic protocols and primitives. So-called security models specify the expected security guarantees of the scheme in question with regards to a well-defined class of adversaries. Proofs that validate these security claims do so by reducing the security of the overall scheme to the security of the underlying cryptographic primitives and hardness assumptions. However, advances in computational power and more sophisticated cryptanalytic capabilities often render exactly these components insecure. Especially the advent of quantum computers will have a devastating effect on much of today's public key cryptography. This is especially true for key exchange protocols since they rely crucially on public-key algorithms. In this thesis, our focus in future-proofing key exchange protocols is two-fold. First, we focus on extending security models for key exchange protocols to capture the (un)expected break of cryptographic primitives and hardness assumptions. The aim is to gain assurances with respect to future adversaries and to investigate the effects of primitive failures on key exchange protocols. More specifically, we explore how key exchange protocols can be safely transitioned to new, post-quantum secure algorithms with hybrid techniques. Hybrids combine classical and post-quantum algorithms such that the overall key agreement scheme remains secure as long as one of the two base schemes remains secure. For this, we introduce security notions for key encapsulation mechanisms that account for adversaries with varying levels of quantum capabilities and present three new constructions for hybrid key encapsulation mechanisms. Our hybrid designs are practice-inspired and for example capture draft proposals for hybrid modes in the Transport Layer Security (TLS) protocol, which is one of the most widely-deployed cryptographic protocols that enables key agreement. Furthermore, our notion of breakdown resilience for key exchange protocols allows to gauge the security of past session keys in the event of a failure of a cryptographic component in the key exchange. We exercise our model on variants of the post-quantum secure key exchange protocol NewHope by Alkim et al. Thereby, we confirm the intuition that, in order to guard against adversaries that only have access to quantum computing power in the (more distant) future, it is sufficient to use classically-secure authentication mechanisms alongside post-quantum key agreement to achieve authenticated key exchange. As with any mathematical statement, theorems in the provable security paradigm are only as valid as the underlying assumptions. A careful consideration of any newly made assumption is thus essential to ensure the meaningfulness of the statement itself and make the assumption a viable tool for future analyses. Thus, secondly, we systematically classify the PRF-ODH assumption, a complexity-theoretic hardness assumption that has been used in key exchange security analyses of such prominent protocols as TLS, Signal, and Wireguard. In particular, we give a unified, parametrized definition of the assumption encompassing different variants that are present in the literature. We relate the resulting parametrized notions in terms of their strength and show where these assumptions fit in the collection of well-understood related hardness assumptions. We finally sketch our result on the impossibility of instantiating this assumption in the standard model, thereby disposing of the uncertainty in the community whether PRF-ODH is in fact a standard model assumption, i.e., removes the usage of some idealized assumptions in key exchange protocol proofs.
In this work we construct an alternative model for Authenticated Key Exchange, intended to build a theoretic security framework for protocols whose characteristics may not always concur with the specifics of already existing models for authenticated exchanges. This model is constructed in a modular way, from the notion of commitment schemes and employing ephemeral information, therefore avoiding the exchange of long-term cryptographic material. From this model, we propose a number of Commitment-based protocols to establish a shared secret between two parties, and study their resistance over unauthenticated channels. This means analyzing the security of the protocol itself, and its robustness against Man-in-the-Middle attacks, by formalizing their security under this model. The protocols are constructed from Key Agreement (KA) and Key Encapsulation (KEM) primitives, to show that this model can be applied to both established and new paradigms. We highlight the differences that arise naturally, due to the nature of KEM constructions, in terms of the protocol itself and the types of attacks that they are subject to. We provide practical go-to protocols instances to migrate to, both for KEM-based and KA-based cryptographic primitives.
Security protocols, such as TLS, SSH, IEEE~802.11, and DNSSEC, have become crucial tools in modern society to protect people, data, and infrastructure. They are used throughout virtually all electronic devices to achieve a wide range of different security goals, such as confidentiality, authentication, and integrity. As the long history of attacks on security protocols illustrates, it is indispensable to perform a formal security analysis of such protocols. A central tool in cryptography for taming the complexity of the design and the analysis of modern protocols is modularity, provided by security models for universal composability. Such models allow for designing and analyzing small parts of a protocol in isolation and then reusing these security results in the context of the overall protocol. This is not just easier than analyzing the whole protocol as a monolithic block but also reduces the overall effort required in building and analyzing multiple different protocols based on the same underlying components, such as cryptographic primitives. Ideally, a model for universal composability should support a protocol designer in easily creating full, precise, and detailed specifications as well as sound security proofs of various protocols for various types of adversarial models, instead of being an additional obstacle one has to overcome during a security analysis. In particular, such a model should be sound, flexible/expressive, and easy to use. Unfortunately, despite the wide spread use of models for universal composability, existing models and frameworks are still unsatisfying in these respects as none combines all of these requirements simultaneously. In this thesis we therefore develop a model for universal composability, called the iUC framework, which combines soundness, usability, and flexibility in a so far unmatched way, and hence constitutes a solid framework for designing and analyzing essentially any protocol and application in a modular, universally composable, and sound manner. We use our model in a case study to analyze multiple different key exchange protocols precisely as they are deployed in practice. This illustrates the combination of both flexibility and usability of our model. This case study is also an important independent contribution as this is the first faithful security analysis of these unmodified protocols in a universal composability setting.