Author: Arnab Roy

Publisher:

Published: 2009

Total Pages:

ISBN-13:

Present-day internet users and networked enterprises rely on key management and related protocols that use cryptographic primitives. In spite of the staggering financial value of, say, the total number of credit card numbers transmitted by SSL/TLS in a day, we do not have correctness proofs that respect cryptographic notions of security for many of these relatively simple distributed programs. In light of this challenge, there have been many efforts to develop and use methods for proving security properties of network protocols. Computational Protocol Composition Logic (CPCL), developed by our group at Stanford, is a symbolic logic whose semantics is defined with respect to the complexity-theoretic model of cryptography. The axiomatic proofs in CPCL do not involve probability and complexity and are amenable to automation. Furthermore, the soundness theorem guarantees that they provide comparable mathematical guarantees as traditional hand-proofs done by cryptographers. Protocol authentication properties are generally trace-based, meaning that authentication holds for the protocol if authentication holds for individual traces (runs of the protocol and adversary). Computational secrecy conditions, on the other hand, often are not trace based: the ability to computationally distinguish a system that transmits a secret from one that does not, is measured by overall success on the \textit{set} of all traces of each system. Non-trace-based properties present a challenge for inductive or compositional methods: induction is a natural way of reasoning about traces of a system, but it does not appear directly applicable to non-trace properties. We therefore investigate the semantic connection between trace properties that could be established by induction and non-trace-based security requirements. In this dissertation, we present foundations for inductive analysis of computational security properties by proving connections between selected trace properties of protocol executions and non-trace complexity theoretic properties standard in the literature. Specifically, we prove that a certain trace property implies computational secrecy and authentication properties, assuming the encryption scheme provides chosen ciphertext security and ciphertext integrity. We formalize the aforesaid inductive properties in a set of new axioms and inference rules that are added to CPCL and prove soundness of the system over a standard cryptographic model with a probabilistic polynomial time adversary. We illustrate the system by giving a modular, formal proof of computational authentication and secrecy properties of Kerberos V5. We also present axioms and inference rules for reasoning about Diffie-Hellman-based key exchange protocols and use these rules to prove authentication and secrecy properties of two important protocol standards, the Diffie-Hellman variant of Kerberos, and IKEv2, the revised standard key management protocol for IPSEC. The proof system extended with the new axioms and rules is sound for an accepted semantics used in cryptographic studies. In the process of applying our system, we uncover a deficiency in Diffie-Hellman Kerberos that is easily repaired.