From qualitative to quantitative proofs of security properties using first-order conditional logic
Joseph Yehuda Halpern · Journal of Computer Security · 2016
A first-order conditional logic is considered, with semantics given by a variant of ϵ-semantics where [Formula: see text] means that [Formula: see text] 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.