From qualitative to quantitative proofs of security properties using first-order conditional logic¹

Article type: Research Article

Authors: Halpern, Joseph Y.

Affiliations: Department of Computer Science, Cornell University, Ithaca, NY 14853, USA. E-mail: halpern@cs.cornell.edu. URL: http://www.cs.cornell.edu/home/halpern

Note: [1] A preliminary version of this paper appeared in AAAI-08 (Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence), 2008. This version uses a somewhat different axiomatization than the conference version, and includes proofs not contained in the conference version, as well as more detailed discussion.

Abstract: A first-order conditional logic is considered, with semantics given by a variant of ϵ-semantics where φ→ψ means that Pr(ψ|φ) approaches 1 super-polynomially – faster than any inverse polynomial. This type of convergence is needed for reasoning about security protocols. A complete axiomatization is provided for this semantics, and it is shown how a qualitative proof of the correctness of a security protocol can be automatically converted to a quantitative proof appropriate for reasoning about concrete security.

Keywords: Qualitative security, quantitative security, conditional logic, epsilon semantics

DOI: 10.3233/JCS-15774

Journal: Journal of Computer Security, vol. 25, no. 1, pp. 1-19, 2017