On the computational soundness of formal analysis of cryptographic protocols

Protocols can be specified and analyzed using the simpler symbolic method in such a way that the security results obtained this way have a meaningful computational interpretation.; We start with a comprehensive study of the Abadi-Rogaway logic where we address the following issues. (1) First we give a natural counterexample that shows that the original logic is not complete. (2) Then we investigate under which conditions the Abadi-Rogaway logic becomes complete and discover that if the encryption scheme that is used satisfies a standard, well-studied security condition, namely that it is authenticated, then the logic becomes complete. (3) Finally, we investigate several refinements of the logic; in the most interesting extension that we provide, we show how to eliminate the impractical requirement that encryption hides the length of the plaintext.; Next, we provide a computational analysis of the well-known Needham-Schroder-Lowe protocol. We prove that (1) the protocol may be insecure, even if encryption satisfies the standard security notion of indistinguishability under chosen-plaintext attack and (2) the protocol is secure if encryption satisfies in-distinguishability under chosen-ciphertext attack. Essentially we show that formal analysis is not sound even if encryption satisfies a strong, standard security requirement (IND-CPA) but the question of soundness is open for the case of a stronger security notion (IND-CCA).; The main result of this dissertation is a framework in which security protocols can be analyzed using (simple, automated) symbolic execution models and yet the results that are proved have a natural computational interpretation. Specifically, we provide a simple language for specifying protocols in which parties exchange messages formed by combining parties identities, randomly generated nonces using public-key encryption and pairing. We then give a symbolic and a computational model for executing such protocols in the presence of attackers that actively interfere with their execution. Our main theorem is about the soundness of the symbolic analysis with respect to the concrete model: we prove that for specific security notions for protocols (which we show how to define generically), if the encryption scheme used to implement the protocol in the computational setting is IND-CCA secure, then proving security in the symbolic model implies security with respect to the computational model. (Abstract shortened by UMI.)...