We develop a compositional method for proving cryptographically sound security properties of key exchange protocols, based on a symbolic logic that is interpreted over conventional runs of a protocol against a probabilistic polynomial-time attacker. Since reasoning about an unbounded number of runs of a protocol involves induction-like arguments about properties preserved by each run, we formulate a specification of secure key exchange that, unlike conventional key indistinguishability, is closed under general composition with steps that use the key.
We develop a compositional method for proving cryptographically sound security properties of key exchange protocols, based on a symbolic logic that is interpreted over conventional runs of a protocol against a probabilistic polynomial-time attacker. Since reasoning about an unbounded number of runs of a protocol involves induction-like arguments about properties preserved by each run, we formulate a specification of secure key exchange that, unlike conventional key indistinguishability, is closed under general composition with steps that use the key.
Recently, Canetti and Krawczyk (Eurocrypt'2001) formu- lated a notion of security for key-exchange (ke) protocols, called SK- security, and showed that this notion suffices for constructing secure channels. However, their model and proofs do not suffice for proving more general composability properties of SK-secure ke protocols. We show that while the notion of SK-security is strictly weaker than a fully-idealized notion of key exchange security, it is sufficiently robust for providing secure composition with arbitrary protocols. In particular, SK-security guarantees the security of the key for any application that desires to set-up secret keys between pairs of parties. We also provide new definitions of secure-channels protocols with similarly strong com- posability properties, and show that SK-security suffices for obtaining these definitions. To obtain these results we use the recently proposed framework of uni- versally composable (UC) security. We also use a new tool, called non- information oracles, which will probably find applications beyond the present case. These tools allow us to bridge between seemingly limited indistinguishability-based definitions such as SK-security and more pow- erful, simulation-based definitions, such as UC security, where general composition theorems can be proven. Furthermore, based on such compo- sition theorems we reduce the analysis of a full-fledged multi-session key- exchange protocol to the (simpler) analysis of individual, stand-alone, key-exchange sessions.
We propose a novel paradigm for defining security of cryptographic protocols, called universally composable security. The salient property of universally composable definitions of security is that they guarantee security even when a secure protocol is composed of an arbitrary set of protocols, or more generally when the protocol is used as a component of an arbitrary system. This is an essential property for maintaining security of cryptographic protocols in complex and unpredictable environments such as the Internet. In particular, universally composable definitions guarantee security even when an unbounded number of protocol instances are executed concurrently in an adversarially controlled manner, they guarantee non-malleability with respect to arbitrary protocols, and more. We show how to formulate universally composable definitions of security for practically any cryptographic task. Furthermore, we demonstrate that practically any such definition can be realized using known techniques, as long as only a minority of the participants are corrupted. We then proceed to formulate universally composable definitions of a wide array of cryptographic tasks, including authenticated and secure communication, key-exchange, public-key encryption, signature, commitment, oblivious transfer, zero knowledge and more. We also make initial steps towards studying the realizability of the proposed definitions in various settings.
What does it mean for a cryptographic protocol to be "secure"? Capturing the security requirements of cryptographic tasks in a meaningful way is a slippery business: On the one hand, we want security criteria that prevent "all potential attacks" against a protocol; on the other hand, we want our criteria not to be overly restrictive and accept "reasonable protocols". One of the main reasons for flaws is the often unexpected interactions among different protocol instances that run alongside each other in a composite system.This tutorial studies a general methodology for defining security of cryptographic protocols. The methodology, often dubbed the "trusted party paradigm", allows for defining the security requirements of a large variety of cryptographic tasks in a unified and natural way. We first review more basic formulations that capture security in isolation from other protocol instances. Next we address the security problems associated with protocol composition, and review formulations that guarantee security even in composite systems.
In general, it is difficult to verify security of cryptographic protocols.Indeed, flaws of designs and security proofs of some protocols were found after they had been presented.In deductive verification using formal methods, protocols and security properties are described in formal languages, and correctness of designs and security proofs are deduced by inference rules.While a number of formal frameworks and verification tools have been developed and applied to classical protocols, few formal methods have been applied to security proofs of quantum protocols.The contributions of this thesis consist of the following three results.First, we developed a software tool to verify bisimilarity of configurations (pairs of processes and quantum states) of qCCS, a quantum process calculus presented by Feng et al.Bisimilar configurations behave indistinguishably from the outside.We designed a formal framework for the verifier, which we call nondeterministic qCCS, on the basis of qCCS by Feng et al.While the transition system of qCCS is both nondeterministic and probabilistic, we presented a nondeterministic and non-probabilistic transition system for configurations, extending the definition of them.This allows the verifier to verify bisimilarity efficiently.Next, we designed the verifier to handle security parameters and quantum states symbolically.A purpose is to apply it to quantum cryptographic protocols, where the dimensions of quantum states depend on security parameters.When the verifier checks bisimulation relation of configurations, it uses user-defined equations on the symbolic representations to check the quantum states that the outsider can access are always equal.Besides, the verifier is sound with respect to qCCS, that is, when it runs with two configurations as input and returns true, a symbol representing success of the verification, the configurations are in bisimulation relation in the qCCS's definition.Second, we defined a notion of approximate bisimulation relation on configurations of nondeterministic qCCS, and extended the verifier to check the approximate bisimilarity.Approximately bisimilar configurations reveal quantum states with close trace distance to the outsider after transitions.This property is useful in security proofs of quantum key distribution protocols.We then proved the approximate bisimulation relation is closed under application of evaluation contexts of processes.Third, we formally verified Shor and Preskill's security proof of BB84 quantum key distribution protocol.They first considered another protocol (the EDP-based protocol) and proved the security of BB84 and the EDP-based protocol is equivalent.They next proved the latter is secure.For the first step of their proof, we formalized the two protocols as configurations and formally verified that they are bisimilar.For the second step, we defined a completely secure protocol (EDPideal) and formally verified that the configurations of it and the EDP-based protocol are approximately bisimilar.This is the first work where a security proof of a quantum cryptographic protocol is mechanically verified using a software tool.
Authenticated key exchange protocols are ubiquitous in modern-day life. They are used to secure numerous types of data exchange, ranging from online banking to instant messaging conversations. In this thesis, we extend the state of the art for authenticated key exchange security, following the three themes of realistic, strong and provable. First, we tackle the theme of provable security. We develop generic techniques, applicable to a wide range of security models, to assist in proofs of security of cryptographic schemes. Specifically, a "game hopping" proof is a powerful technique to prove strong statements about the security of a protocol. However, the proof technique often involves esoteric and repetitive steps. We demystify the methodology and prove generic theorems to reduce the length and complexity of a wide class of game hopping proofs. Next, we use this new framework to analyse strong and previously unstudied formal security guarantees of authenticated key exchange protocols. These protocols are able to achieve strong security guarantees because they share and update state across sessions. Using our framework, we are able to push the state of the art by defying the folklore of what was previously thought provable of authenticated key exchange protocols. Specifically, it was previously thought that no protocol can achieve a security guarantee about communication with a peer if the peer was already fully compromised. We show that this is not true by formally defining a new concept, which we name post-compromise security. We capture an intuitive "self-healing" property of protocols. We then construct and formally prove protocols can achieve this strong security notion. Finally, we leverage all of this work to analyse realistic protocols. Signal, which is used to encrypt messages in WhatsApp, Facebook Messenger and Google Allo amongst others, is one such protocol we consider. Despite being used by billions of people, Signal was completely unstudied in the academic literature prior to this work. Two reasons for this were that Signal had no documentation at the time and it did not fit into existing models: it shares state across sessions and has over ten different types of key, most of which continually update. Despite its complexity, we are able to use the other work in this thesis to give the first ever analysis and proof of security of Signal. Overall, this thesis aims to bridge the gap between theory and practice in the current state of the art of authenticated key exchange protocols.
This work presents a general framework for describing cryptographic protocols and analyzing their security. The framework allows specifying the security requirements of practically any cryptographic task in a unified and systematic way. Furthermore, in this framework the security of protocols is preserved under a general composition operation, called universal composition. The proposed framework with its security-preserving composition operation allows for modular design and analysis of complex cryptographic protocols from simpler building blocks. Moreover, within this framework, protocols are guaranteed to maintain their security in any context, even in the presence of an unbounded number of arbitrary protocol sessions that run concurrently in an adversarially controlled manner. This is a useful guarantee, which allows arguing about the security of cryptographic protocols in complex and unpredictable environments such as modern communication networks.