Symbolic protocol analysis based on the Dolev-Yao model [DY84] and complexity-theoretic based analysis (starting from work by Goldwasser-Micali on encryption [GM84]) have emerged as two largely independent research areas over the last two decades. The connection between these two models has remained unclear. The symbolic model operates under the perfect cryptography assumption (e.g., in order to decrypt a ciphertext it is essential to possess the key). The attacker is allowed to perform only a fixed set of actions (e.g., decryption with known key). This idealization has paved the way for formal analysis techniques and tools which have been successfully applied to practical protocols. On the other hand, the complexity-theoretic model allows more fine-grained specification of protocol properties (e.g., secrecy of a message is defined as not possessing any partial information about the message). The attacker model is much more powerful: she can carry out any probabilistic polytime computation in order to execute an attack. However, protocol correctness proofs are long, detailed, done by hand, and require explicit reasoning about probability and complexity.
In this work, our goal is to get the best of both worlds by (i) using a symbolic logic for specifying and proving protocol properties; while (ii) using the complexity-theoretic model for interpreting these properties and defining the execution model, in particular, the adversary capabilities. Our result is a logic called Computational Protocol Composition Logic (CPCL) which is developed along these lines. The soundness theorem for CPCL's proof system ensures that our axiomatic proofs (which do not explicitly mention probability or complexity) carry the same meaning as hand-proofs done by cryptographers. The logic has been applied to prove security properties of several industrial protocols including various versions of Kerberos and IKEv2.