From Qualitative to Quantitative Proofs of Security Properties Using First-Order Conditional Logic

Security protocols, such as key-exchange and key management protocols, are short, but notoriously difficult to prove correct. Flaws have been found in numerous protocols, ranging from the the 802.11 Wired Equivalent Privacy (WEP) protocol used to protect link-layer communications from eavesdropping and other attacks to standards and proposed standards for Secure Socket Layer to Kerberos. Not surprisingly, a great deal of effort has been devoted to proving the correctness of such protocols. There are two largely disjoint approaches. The first essentially ignores the details of cryptography by assuming perfect cryptography and an adversary that controls the network. The second approach applies the tools of modern cryptography to proving correctness, using more quantitative arguments.