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

Abstract

A first-order conditional logic is considered, with semantics given by a variant of ϵ-semantics where $φ \to ψ$ 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

1. Introduction

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 802.11 Wired Equivalent Privacy (WEP) protocol used to protect link-layer communications from eavesdropping and other attacks [10] to standards and proposed standards for Secure Socket Layer [24,26] to Kerberos [7]. 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 (i.e., nothing encrypted can ever be decrypted without the encryption key) and an adversary that controls the network. By ignoring the cryptography, it is possible to give a more qualitative proof of correctness, using logics designed for reasoning about security protocols. Indeed, this approach has enabled axiomatic proofs of correctness and model checking of proofs (see, for example, [23,25]). The second approach applies the tools of modern cryptography to proving correctness, using more quantitative arguments. Typically it is shown that, given some security parameter k (where k may be, for example, the length of the key used) an adversary whose running time is polynomial in k has a negligible probability of breaking the security, where “negligible” means “less than any inverse polynomial function of k” (see, for example, [8,19]). There has been recent work on bridging the gap between these two approaches, with the goal of constructing a logic that can allow reasoning about quantitative aspects of security protocols while still being amenable to mechanization. This line of research started with the work of Abadi and Rogaway [1]. More recently, Datta et al. [13] showed that by giving a somewhat nonstandard semantics to their first-order Protocol Composition Logic [12], it was possible to reason about many features of the computational model. In this logic, an “implication” of the form $φ \supset B$ is interpreted as, roughly speaking, the probability of B given φ is high. For example, a statement like secret encrypted ⊃ adversary does not decrypt the secret says “with high probability, if the secret is encrypted, the adversary does not decrypt it”. While the need for such statements should be clear, the probabilistic interpretation used is somewhat unnatural, and no axiomatization is provided by Datta et al. [13] for the ⊃ operator (although some sound axioms are given that use it).

The interpretation of ⊃ is quite reminiscent of one of the interpretations of → in conditional logic, where $φ \to ψ$ can be interpreted as “typically, if φ then ψ” [22]. Indeed, one semantics given to →, called ϵ-semantics [2,21], is very close in spirit to that used in [13]; this is particularly true for the formulation of ϵ-semantics given by Goldszmidt, Morris, and Pearl [20]. In this formulation, a formula $φ \to ψ$ is evaluated with respect to a sequence $({Pr}_{1}, {Pr}_{2}, \dots)$ of probability measures (probability sequence, for short): it is true if, roughly speaking, ${lim}_{n \to \infty} {Pr}_{n} (ψ | φ) = 1$ (where ${Pr}_{k} (ψ | φ)$ is taken to be 1 if ${Pr}_{k} (φ) = 1$ ). This formulation is not quite strong enough for some security-related purposes, where the standard is super-polynomial convergence, that is, convergence faster than any inverse polynomial. To capture such convergence, we can take $φ \to ψ$ to be true with respect to this probability sequence if, for all polynomials p, there exists $n^{*}$ such that, for all $n ⩾ n^{*}$ , ${Pr}_{n} (ψ | φ) ⩾ 1 - 1 / p (n)$ . (Note that this implies that ${lim}_{n \to \infty} {Pr}_{n} (ψ | φ) = 1$ .) In a companion paper [14], it is shown that reinterpreting → in this way gives an elegant, powerful variant of the logic considered in [13], which can be used to reason about security protocols of interest.

While it is already a pleasant surprise that conditional logic provides such a clean approach to reasoning about security, using conditional logic has two further significant advantages, which are the subject of this paper. The first is that, as I show here, the well-known complete axiomatization of conditional logic with respect to ϵ-semantics continues to be sound and complete with respect to the super-polynomial semantics for →; thus, the axioms form a basis for automated proofs. The second is that the use of conditional logic allows for a clean transition from qualitative to quantitative arguments. To explain these points, I need to briefly recall some well-known results from the literature.

As is well known, the KLM properties [22] (see Section 2) provide a sound and complete axiomatization for reasoning about → formulas with respect to ϵ-semantics [18]. More precisely, if Δ is a collection of formulas of the form $φ^{'} \to ψ^{'}$ , then Δ (ϵ-)entails $φ \to ψ$ (that is, for every probability sequence $P$ , if every formula in Δ is true in $P$ according to ϵ semantics, then so is $φ \to ψ$ ), then $φ \to ψ$ is provable from Δ using the KLM properties. This result applies only when Δ is a collection of → formulas. Δ cannot include negations or disjunctions of → formulas. Conditional logic extends the KLM framework by allowing Boolean combinations of → statements. A sound and complete axiomatization of propositional conditional logic with semantics given by what are called preferential structures was given by Burgess [11]; Friedman and Halpern [16] proved it was also sound and complete for ϵ-semantics.

Propositional conditional logic does not suffice for reasoning about security. The logic of [13] is first-order; quantification is needed to capture important properties of security protocols. A sound and complete axiomatization for the language of first-order conditional logic, denoted $L_{C}$ , with respect to ϵ-semantics is given by Friedman, Halpern, and Koller [17]. The first major result of this paper shows that a conditional logic formula φ is satisfiable in some model M with respect to ϵ-semantics iff it is satisfiable in some model $M^{'}$ with respect to the super-polynomial semantics. It follows that all the completeness results for ϵ-semantics apply without change to the super-polynomial semantics.

I then consider the language $L_{C}^{0}$ which essentially consists of universal → formulas, that is, formulas of the form $\forall x_{1} \dots \forall x_{n} (φ \to ψ)$ , where φ and ψ are first-order formulas. As in the KLM framework, there are no nested → formulas or negated → formulas. The second major result of this paper is to provide a sound and complete axiomatization that extends the KLM properties for reasoning about when a collection of formulas in $L_{C}^{0}$ entails a formula in $L_{C}^{0}$ .

It might seem strange to be interested in an axiomatization for $L_{C}^{0}$ when there is already a sound and complete axiomatization for the full language $L_{C}$ . However, $L_{C}^{0}$ has some significant advantages. In reasoning about concrete security, asymptotic complexity results do not suffice; more detailed information about security guarantees is needed. For example, we may want to prove that an SSL server that supports 1,000,000 sessions using 1024 bit keys has a probability of 0.999999 of providing the desired service without being compromised. I show how to convert a qualitative proof of security in the language $L_{C}^{0}$ , which provides only asymptotic guarantees, to a quantitative proof. Moreover, the conversion shows exactly how strong the assumptions have to be in order to get the desired 0.999999 level of security. More generally, the proof shows that, given a qualitative proof of a property and ϵ, we can compute a δ in polynomial time from the proof itself such that if the assumptions in the proof all hold with probability at least $1 - δ$ , then the conclusion holds with probability at least $1 - ϵ$ . Such a conversion is not possible with $L_{C}$ . This conversion justifies reasoning at the qualitative level. A qualitative proof can be constructed without worrying about the details of the numbers, and then automatically converted to a quantitative proof for the desired level of security.

There has been work on formal proof techniques for concrete cryptography [5,6,9]. However, it has largely focused on relational techniques where security is proved via game-based reductions, similar to traditional cryptographic proofs. The kind of transition from qualitative to quantitative reasoning that is my focus here has not been investigated. Perhaps even closer to this paper is that of Bana, Hasebe, and Okada [4]. They also have an operator → that can be viewed as attempting to capture qualitatively some probabilistic aspects of reasoning about security. I discuss their work in more detail in Section 4.

In the next section, I review the syntax and semantics of conditional logic, with an emphasis on ϵ-semantics, and show how it can be modified to deal with the super-polynomial convergence that is more appropriate for reasoning about security. In Section 3, I provide axioms and inference rules for both qualitative and quantitative reasoning. I conclude in Section 4 with some discussion of the usefulness of this logic for reasoning about security.

2. First-order conditional logic

I review the syntax and semantics of first-order conditional logic here. It is straightforward to specialize all the definitions and results to the propositional case, so I do not discuss the propositional case further.

The syntax of first-order conditional logic is straightforward. Fix a finite first-order vocabulary $T$ consisting, as usual, of function symbols, predicate symbols, and constants. Starting with atomic formulas (i.e., closed quantifier-free first-order formulas) over the vocabulary $T$ , more complicated formulas are formed by closing off under the standard truth-functional connectives (i.e., ∧ ,∨, ¬, and ⇒), first-order quantification, and the binary modal operator →. Thus, a typical formula is $\forall x (P (x) \to \exists y (Q (x, y) \to R (y)))$ . Let $L_{C} (T)$ be the resulting language. Let $L^{fo} (T)$ be the pure first-order fragment of $L_{C} (T)$ , consisting of →-free formulas. Let $L_{C}^{0} (T)$ consist of all formulas in $L_{C} (T)$ of the form $\forall x_{1} \dots \forall x_{n} (φ \to ψ)$ , where φ and ψ are in $L^{fo}$ . (I henceforth omit the $T$ unless it is necessary for clarity.) Note that $L_{C}^{0}$ does not include negations of → formulas or conjunctions of → formulas. While not having conjunctions does not really impair the expressive power of $L_{C}^{0}$ (since we will be interested in sets of $L_{C}^{0}$ formulas, where a set can be identified with the conjunction of the formulas in the set), the lack of negation does.

I give two semantics to formulas in $L_{C} (T)$ . In both semantics, the truth of formulas is defined with respect to PS structures. A PS structure is a tuple $M = (D, W, π, P)$ , where D is a domain, W is a set of worlds, π is an interpretation, which associates with each predicate symbol (resp., function symbol, constant) in $T$ and world $w \in W$ a predicate (resp., function, domain element) of the right arity, and $P = ({Pr}_{1}, {Pr}_{2}, \dots)$ is a probability sequence, where each probability measure ${Pr}_{n}$ in the sequence is a probability measure on W. I assume for ease of exposition that all subsets of W are measurable with respect to each probability measure ${Pr}_{n}$ in the sequence. (I discuss below how this assumption can be weakened considerably.) As usual, a valuation V associates with each variable x an element $V (x) \in D$ .

Given a valuation V and structure $M = (D, W, π, P)$ , the semantics of ∧, ¬, ⇒, and ∀ is completely standard. In particular, the truth of a first-order formula in $L^{fo}$ in a world $w \in W$ , written $(M, V, w) ⊧ φ$ , is determined as usual. For $φ \in L_{C}$ , let ${⟦ φ ⟧}_{M, V} = {w \in W : (M, V, w) ⊧ φ}$ . If φ is a closed formula, so that its truth does not depend on the valuation, I occasionally write ${⟦ φ ⟧}_{M}$ rather than ${⟦ φ ⟧}_{M, V}$ . I write $(M, V) ⊧ φ$ if $(M, V, w) ⊧ φ$ for all worlds w. The truth of an → formula does not depend on the world, but only on the structure M and valuation V. Define $\begin{array}{rcl} {(M, V, w) ⊧ φ \to ψ if lim_{n \to \infty} {Pr}_{n} {(⟦ ψ ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) = 1, \end{array}$ where ${{Pr}_{n} {(⟦ ψ ⟧}_{M, V} | ⟦ φ ⟧}_{M, V})$ is taken to be 1 if ${Pr}_{n} {(⟦ φ ⟧}_{M, V}) = 0$ . (I could have written $(M, V) ⊧ φ \to ψ$ , since the truth of $φ \to ψ$ is independent of the world w; I occasionally do this below.)

If W is infinite, the assumption that every subset of W is measurable is a very strong one. Suppose instead that there is a fixed σ-algebra $F$ of measurable sets that is the domain of all the probability measures ${Pr}_{n}$ in the sequence. All that is needed in the semantics above is that ${⟦ φ ⟧}_{M, V}$ is measurable (i.e., ${⟦ φ ⟧}_{M, V} \in F$ ) for every formula φ and valuation V. I now give a condition sufficient to guarantee this.

As usual, the set of terms over the vocabulary $T$ is defined inductively. A variable x is a term, a constant $c \in T$ is a term, and if $f \in T$ is a k-ary function symbol and $t_{1}, \dots, t_{k}$ are terms, then $f (t_{1}, \dots, t_{k})$ is a term. An atomic expression over $T$ has the form either (a) $P (t_{1}, \dots, t_{k})$ , where $P \in T$ is a k-ary predicate symbol and $t_{1}, \dots, t_{k}$ are terms over $T$ , (b) $f (t_{1}, \dots, t_{k}) = t_{k + 1}$ , where $f \in T$ is a k-ary predicate symbol and $t_{1}, \dots, t_{k + 1}$ are terms over $T$ , or (c) $t_{1} = t_{2}$ , where $t_{1}$ and $t_{2}$ are terms over $T$ . I claim that if the domain D is finite or countably infinite and for all valuations V and atomic expressions A, ${⟦ A ⟧}_{M, V}$ is measurable, then ${⟦ φ ⟧}_{M, V}$ is measurable for all formulas φ in the language and valuations V. The claim follows by a straightforward induction on the structure of formulas. For a formula φ of the form $\forall x φ^{'}$ , observe that ${{⟦ \forall x φ^{'} ⟧}_{M, V} = ⋂_{d \in D} ⟦ φ^{'} ⟧}_{M, V_{d}}$ , where $V_{d}$ is the valuation that agrees with V except that $V_{d} (x) = d$ . Since D is countable and $F$ is closed under countable intersection, it follows that ${⟦ \forall x φ^{'} ⟧}_{M, V} \in F$ . If φ has the form $φ^{'} \to ψ$ , note that ${⟦ φ^{'} \to ψ ⟧}_{M, V}$ is either ∅ or W, since it is independent of the world, so $⟦ φ^{'} \to ψ ⟧$ must be measurable. All other cases in the induction argument are straightforward.

I also consider an alternative semantics that gives super-polynomial convergence. $\begin{matrix} \begin{matrix} (M, V, w) ⊧^{sp} φ \to ψ if, for all k, there exists some n^{*} ⩾ 0 such that, for all n ⩾ n^{*}, \\ {{Pr}_{n} {(⟦ ψ ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) ⩾ 1 - \frac{1}{n^{k}} . \end{matrix} \end{matrix}$ Note that if $(M, V, w) ⊧^{sp} φ \to ψ$ and $p (n)$ is a polynomial whose leading coefficient is positive, then ${{Pr}_{n} {(⟦ ψ ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) ⩾ 1 - \frac{1}{p (n)}$ for sufficiently large n.

As usual, I write $M ⊧ φ$ if $(M, V) ⊧ φ$ for all valuations V, and $M ⊧ φ$ if $M ⊧ φ$ for all PS structures in a set $M$ , and similarly with ⊧ replaced by $⊧^{sp}$ .

3. Axioms for qualitative and quantitative reasoning

In this section, I start by showing that qualitative reasoning for both ⊧ and $⊧^{sp}$ is characterized by the same axiom system. I then provide a complete axiomatization for $L_{C}^{0}$ . Finally, I consider quantitative conditional logic. In the axioms, it is convenient to use $N φ$ as an abbreviation for $\neg φ \to false$ . Note that if φ is a closed formula, then $M ⊧ N φ$ iff there exists $n^{*}$ such that, for all $n ⩾ n^{*}$ , ${{Pr}_{n} {(⟦ false ⟧}_{M} | ⟦ \neg φ ⟧}_{M}) ⩾ 1 / 2$ . Since ${⟦ false ⟧}_{M} = \emptyset$ , this can happen only if $Pr {(⟦ \neg φ ⟧}_{M}) = 0$ for all $n ⩾ n^{*}$ , or equivalently, ${Pr}_{n} {(⟦ φ ⟧}_{M}) = 1$ for all $n ⩾ n^{*}$ , and similarly with ⊧ replaced by $⊧^{sp}$ . Thus, $N φ$ can be read as saying “φ is almost surely eventually true”.

3.1. Qualitative reasoning

As was mentioned in the Introduction, Friedman, Halpern, and Koller [17] provide a complete axiomatization ${AX}_{C}$ for $L_{C}$ with respect to ⊧. For security applications, a generalization of their result is needed, where it is possible to restrict to models where all worlds satisfy a particular first-order theory Λ. We can think of Λ as describing first-order properties of the security protocol being analyzed. Formally, Λ is just a (possibly infinite) set of first-order formulas.

Let $⊢_{Λ}$ denote provability in first-order logic given the formulas in the theory Λ. Let ${AX}_{C}^{Λ}$ consist of the following axioms and rules:

Λ-AX.

φ, if $φ \in L^{fo}$ and $⊢_{Λ} φ$ .

C0.

All substitution instances of propositional tautologies.

C1.

$φ \to φ$ .

C2.

$((φ \to ψ_{1}) \land (φ \to ψ_{2})) \Rightarrow (φ \to (ψ_{1} \land ψ_{2}))$ .

C3.

$((φ_{1} \to ψ) \land (φ_{2} \to ψ)) \Rightarrow ((φ_{1} \lor φ_{2}) \to ψ)$ .

C4.

$((φ_{1} \to φ_{2}) \land (φ_{1} \to ψ)) \Rightarrow ((φ_{1} \land φ_{2}) \to ψ)$ .

C5.

$[(φ \to ψ) \Rightarrow N (φ \to ψ)] \land [\neg (φ \to ψ) \Rightarrow N \neg (φ \to ψ)]$ .

C6.

$\neg (true \to false)$ .

F1.

$\forall x φ \Rightarrow φ [x / t]$ , where t is substitutable for x in the sense discussed below and $φ [x / t]$ is the result of substituting t for all free occurrences of x in φ (see [15] for a formal definition).

F2.

$\forall x (φ \Rightarrow ψ) \Rightarrow (\forall x φ \Rightarrow \forall x ψ)$ .

F3.

$φ \Rightarrow \forall x φ$ if x does not occur free in φ.

F4.

$x = y \Rightarrow (φ_{1} \Rightarrow φ_{2})$ , where $φ_{1}$ is quantifier-free and $φ_{2}$ is obtained from $φ_{1}$ by replacing zero or more occurrences of x in $φ_{1}$ by y.

F5.

$x \neq y \Rightarrow N (x \neq y)$ .

MP.

From φ and $φ \Rightarrow ψ$ infer ψ.

Gen.

From φ infer $\forall x φ$ .

R1.

From $φ_{1} \Leftrightarrow φ_{2}$ infer $φ_{1} \to ψ \Leftrightarrow φ_{2} \to ψ$ .

R2.

From $ψ_{1} \Rightarrow ψ_{2}$ infer $φ \to ψ_{1} \Rightarrow φ \to ψ_{2}$ .

The axiom system ${AX}_{C}$ of [17] does not have Λ-AX (this is needed to incorporate the theory Λ) and includes an axiom $x = x$ that follows from Λ-AX; otherwise, the axiom systems are identical. As observed in [17], the “positive” version of F5, $x = y \Rightarrow N (x = y)$ , is also sound. It is not included in the axiomatization because it is provable from the other axioms.

I now briefly discuss the axioms. Λ-AX just says that any first-order formula provable in Λ is also provable in ${AX}_{C}^{Λ}$ . The notion of “substitution instance of a propositional tautology” in C0 means that we start with a propositional tautology, and then uniformly replace each instance of a propositional variable by a formula in $L_{C} (T)$ . For example, $\forall x, y (P (x) \to Q (y)) \lor \neg \forall x, y (P (x) \to Q (y))$ is a substitution instance of the propositional tautology $p \lor \neg p$ , where $\forall x, y (P (x) \to Q (y))$ is substituted for p.

C1 has been called reflexivity; it says, for example, that birds are typically birds. C2 is called the and rule; it says, for example, that if birds typically fly and birds typically have wings, then birds typically both fly and have wings. C3 is the or rule; it says, for example, that if birds typically fly and insects typically fly, that something that is either a bird or an insect typically flies. C4 is cautious monotonicity; it says that if birds typically fly and birds typically have wings, then flying birds typically have wings. Full monotonicity would say that if birds typically have wings then red birds have wings or, more generally, $(φ \to ψ) \Rightarrow ((φ \land φ^{'}) \to ψ)$ , for an arbitrary $φ^{'}$ . This is not sound (although the analogue is sound if we replace → by ⇒). R1 is left logical equivalence; it says that if we replace the left-hand side of a → formula by a provably equivalent formula, the resulting → formula is equivalent to the original formula. Again, the stronger version (that if we replace the left-hand side by a stronger formula we get a formula weaker than the original) does not hold; this is just full monotonicity. R2 is right weakening; it says that if we replace the right-hand side of a → formula by a weaker formula, the resulting → formula is weaker than the original formula. The axioms and rules C1–C4, R1, and R2 characterize the core properties of →, and will essentially reappear in system P, discussed below.

C5 encodes the fact that the truth of $φ \to ψ$ depends only on the world; if it is true at some world, it is true at all worlds (and hence holds with probability 1). This lets us handle nested occurrence of →. C6 is clearly a trivial consequence of the probabilistic semantics.

To understand the notion of “substitutable” in F1, observe that a term t with free variables that might be captured by some quantifiers in φ cannot be substituted for x; for example, while $\forall x \exists y (x \neq y)$ is true as long as the domain has at least two elements, the result of substituting y for x is $\exists y (y \neq y)$ , which is surely false. In the case of first-order logic, it suffices to define “substitutable” so as to make sure this does not happen (see [15] for details). However, in modal logics such as this one, more care must be taken. In general, terms cannot be substituted for universally quantified variables in a modal context, since terms are not in general rigid; that is, they can have different interpretations in different worlds. To understand the impact of this, consider the formula $\forall x (\neg N P (x)) \Rightarrow \neg N P (c)$ (where P is a unary predicate and c is a constant). This formula is not valid in PS structures. For example, consider a PS structure $M = (D, W, π, P)$ , where $W = {w_{1}, w_{2}}$ , $D = {d_{1}, d_{2}}$ , $P = ({Pr}_{1}, {Pr}_{2}, \dots)$ is such that ${Pr}_{n}$ gives positive probability to both $w_{1}$ and $w_{2}$ , and π is such that in world $w_{1}$ , $P (d_{1})$ holds, $P (d_{2})$ does not, and c is interpreted as $d_{1}$ , while in world $w_{2}$ , $P (d_{2})$ holds, $P (d_{1})$ does not, and c is interpreted as $d_{2}$ . Then it is easy to see that $N P (c)$ holds in both worlds, but $N P (x)$ does not hold, no matter how x is interpreted. It follows that $M ⊧ N P (c)$ and $M ⊧ \forall x (\neg N P (x))$ . Thus, if φ is a formula that has occurrences of →, then the only terms that are considered substitutable for x in φ are other variables.

The fact that variables are rigid is what makes F5 sound: if $x \neq y$ in some world given some valuation V, then $x \neq y$ in all worlds given valuation V, and hence holds with probability 1. F2, F3, F4, MP, and Gen are standard axioms and rules of first-order logic, and apply to modal logic as well.

I want to show that ${AX}_{C}^{Λ}$ is also sound and complete for the $⊧^{sp}$ semantics. The key step in doing that is to show that a formula is satisfiable with respect to the ⊧ semantics iff it is satisfiable with respect to the $⊧^{sp}$ semantics.

Theorem 3.1.
If $M = (D, W, π, P)$ is a PS structure such that D is countable, then there exists a probability sequence $P^{'}$ such that, for all valuations V, $(M, V) ⊧ φ$ iff $(M^{'}, V) ⊧^{sp} φ$ , where $M^{'} = (D, W, π, P^{'})$ .
Proof.
Suppose that $M = (D, W, π, P)$ , where $D = {d_{1}, d_{2}, \dots}$ (D may be finite), and $P = ({Pr}_{1}, {Pr}_{2}, \dots)$ . Suppose that the set of variables is ${x_{1}, x_{2}, \dots}$ . (I am implicitly assuming that the set of variables is countable, as is standard.) Define a valuation V to be constant at k if $V (x_{m}) = d_{1}$ for all $m ⩾ k$ ; a valuation V is eventually constant if V is constant at k for some k. Clearly there are only countably many eventually constant valuations. Let $L^{+}$ be an enumeration of pairs of the form $(φ \to ψ, V)$ such that V is eventually constant and $(M, V) ⊧ φ \to ψ$ ; let $L^{-} = ((φ_{1} \to ψ_{1}, V_{1}), (φ_{2} \to ψ_{2}, V_{2}), \dots)$ be an enumeration of pairs of the form $(φ \to ψ, V)$ such that V is eventually constant and $(M, V) ⊧ \neg (φ \to ψ)$ , where each pair appears in the enumeration $L^{-}$ infinitely often. There exists a function $f : N \to N$ such that for all n, if $n^{'} > f (n)$ , then ${{Pr}_{n^{'}} {(⟦ ψ ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) ⩾ 1 - 1 / n^{n}$ for all the first n pairs $(φ \to ψ, V) \in L^{+}$ . Similarly, there exists a function g that maps elements in the enumeration $L^{-}$ to $N$ such that if $(φ \to ψ, V)$ is in $L^{-}$ , then $g (φ \to ψ, V)$ is the least integer k such that, for infinitely many indices h, we have ${{Pr}_{h} {(⟦ ψ ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) < 1 - 1 / k$ . (There must be such an integer k, since ${{lim}_{h \to \infty} {Pr}_{h} {(⟦ ψ ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) \neq 1$ .)

I now construct a subsequence $P^{'} = ({Pr}_{1}^{'}, {Pr}_{2}^{'}, \dots)$ of $P$ by taking ${Pr}_{n}^{'} = {Pr}_{N}$ , where, if $(φ \to ψ, V)$ is the nth element of $L^{-}$ , then N is the least integer greater than $f (n)$ such that ${{Pr}_{N}^{'} {(⟦ ψ ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) < 1 - 1 / g (φ \to ψ, V)$ . Let $M^{'} = (D, W, π, P^{'})$ . I now prove that $(M, V) ⊧ φ$ iff $(M^{'}, V) ⊧^{sp} φ$ for all valuations V and formulas $φ \in L_{C}$ by a straightforward induction on the structure of φ. If φ is an atomic formula, this is immediate, since M and $M^{'}$ differ only in their probability sequences. All cases but the one where φ has the form $φ^{'} \to ψ^{'}$ follow immediately from the induction hypothesis. If φ has the form $φ^{'} \to ψ^{'}$ , suppose that the free variables in $φ^{'} \to ψ^{'}$ are contained in ${x_{1}, \dots, x_{k}}$ . Given V, let $V^{'}$ be an eventually constant valuation such that $V (x_{i}) = V^{'} (x_{i})$ for $i = 1, \dots, k$ . Clearly, for all distributions Pr on W, we have ${{Pr {(⟦ ψ ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) = Pr {(⟦ ψ ⟧}_{M, V^{'}} | ⟦ φ ⟧}_{M, V^{'}})$ , and similarly with M replaced by $M^{'}$ . First suppose that $(M, V) ⊧ φ^{'} \to ψ^{'}$ . Thus, we must have $(M, V^{'}) ⊧ φ^{'} \to ψ^{'}$ , so $(φ^{'} \to ψ^{'}, V^{'})$ is in $L^{+}$ . Suppose that $(φ^{'} \to ψ^{'}, V^{'})$ is the Nth pair in $L^{+}$ . The construction guarantees that for all $n ⩾ N$ , we have ${{Pr}_{n}^{'} {(⟦ ψ ⟧}_{M, V^{'}} | ⟦ φ ⟧}_{M, V^{'}}) ⩾ 1 - 1 / n^{n}$ . It follows that $(M^{'}, V^{'}) ⊧^{sp} φ^{'} \to ψ^{'}$ , and thus $(M^{'}, V) ⊧^{sp} φ^{'} \to ψ^{'}$ .

Next suppose that $(M, V) ⊧ \neg (φ^{'} \to ψ^{'})$ . Thus, $(M, V^{'}) ⊧ \neg (φ^{'} \to ψ^{'})$ , so the pair $(φ^{'} \to ψ^{'}, V^{'})$ appears infinitely often in the enumeration $L^{-}$ . For each index h such that this pair appears in position h in $L^{-}$ , by construction, we have that ${{Pr}_{h}^{'} {(⟦ ψ^{'} ⟧}_{M^{'}, V^{'}} | ⟦ φ^{'} ⟧}_{M^{'}, V^{'}}) < 1 - 1 / g (φ^{'} \to ψ^{'}, V^{'})$ . Hence, $(M^{'}, V^{'}) ⊧^{sp} \neg (φ^{'} \to ψ^{'})$ , so $(M^{'}, V) ⊧^{sp} \neg (φ^{'} \to ψ^{'})$ , as desired.2
²
Exactly the same argument shows that there exists a probability sequence $P^{'}$ such that, for all valuations V, $(M, V) ⊧ φ$ iff $(M^{'}, V) ⊧^{ex} φ$ , where $M^{'} = (D, W, π, P^{'})$ and $⊧^{ex}$ considers exponential convergence for →; that is, $(M, V, w) ⊧^{ex} φ \to ψ$ if, for all c, there exists some $n^{} ⩾ 0$ such that, for all $n ⩾ n^{}$ , ${{Pr}_{n} {(⟦ ψ ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) ⩾ 1 - \frac{1}{2^{c n}}$ . I have focused on super-polynomial rather than exponential convergence here since that is what is considered in the security literature.

□

Let $PS (Λ)$ consist of all PS structures M such that every world in M satisfies Λ.
Theorem 3.2.
${AX}_{C}^{Λ}$ is a sound and complete axiomatization for $PS (Λ)$ with respect to both ⊧ and $⊧^{sp}$ . That is, the following are equivalent for all formulas in $L_{C} (T)$ :
${AX}_{C}^{Λ} ⊢ φ$ ;

$PS (Λ) ⊧ φ$ ;

$PS (Λ) ⊧^{sp} φ$ .

Proof.
The equivalence of parts (a) and (b) for the case that $Λ = \emptyset$ is proved in Theorem 5.2 of [17]. The same proof shows that the result holds for arbitrary Λ. To show that (a) implies (c), I must show that all the axioms are valid, and that the rules of inference preserve validity. This is straightforward for all the axioms and rules other than C2, C3, C4, and C5. I consider each of these axioms in turn.

For C2, suppose that $M = (D, W, π, ({Pr}_{1}, {Pr}_{2}, \dots))$ is a PS structure such that $M ⊧^{sp} φ \to ψ_{1}$ and $M ⊧^{sp} φ \to ψ_{2}$ . Since $M ⊧^{sp} φ \to ψ_{i}$ , $i = 1, 2$ , given a positive polynomial p, there exists $n_{1}^{}, n_{2}^{} ⩾ 0$ such that, for all $n ⩾ n_{i}^{}$ , ${{Pr}_{n} {(⟦ ψ_{i} ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) ⩾ 1 - 1 / 2 p (n)$ , for $i = 1, 2$ . For all $n ⩾ max (n_{1}^{}, n_{2}^{})$ , ${{Pr}_{n} {(⟦ \neg ψ_{i} ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) ⩽ 1 / 2 p (n)$ . Thus, for $n ⩾ max (n_{1}^{}, n_{2}^{})$ , $\begin{array}{l} {{Pr}_{n} {(⟦ ψ_{1} \land ψ_{2} ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) \\ {⩾ 1 - {({Pr}_{n} {(⟦ \neg ψ_{1} ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) + {Pr}_{n} {(⟦ \neg ψ_{2} ⟧}_{M, V} | ⟦ φ ⟧}_{M, V})) \\ ⩾ 1 - \frac{1}{2 p (n)} - \frac{1}{2 p (n)} \\ = 1 - \frac{1}{p (n)} . \end{array}$

For C3, note that $\begin{array}{l} Pr (A | B_{1} \cup B_{2}) \\ = Pr ((A \cap B_{1} \cup A \cap B_{2}) | B_{1} \cup B_{2}) \\ = Pr (A \cap B_{1} | B_{1} \cup B_{2}) + Pr (A \cap B_{2} | B_{1} \cup B_{2}) - Pr (A \cap B_{1} \cap B_{2} | B_{1} \cup B_{2}) \\ = Pr (A | B_{1}) \times Pr (B_{1} | B_{1} \cup B_{2}) + Pr (A | B_{2}) \times Pr (B_{2} | B_{1} \cup B_{2}) \\ (1) & - Pr (A \cap B_{1} \cap B_{2} | B_{1} \cup B_{2}) . \end{array}$ Now suppose that $M ⊧^{sp} φ_{1} \to ψ$ and $M ⊧^{sp} φ_{2} \to ψ$ . Given a positive polynomial p, as in the case of C2, there exist $n_{1}^{}$ and $n_{2}^{}$ such that, for all $n ⩾ n_{i}^{}$ , ${{Pr}_{n} {(⟦ ψ ⟧}_{M, V} | ⟦ φ_{1} ⟧}_{M, V}) ⩾ 1 - 1 / 2 p (n)$ , for $i = 1, 2$ . It easily follows from (1) that if $n ⩾ max (n_{1}^{}, n_{2}^{})$ , then $\begin{array}{l} {{Pr}_{n} {(⟦ ψ ⟧}_{M, V} | ⟦ φ_{1} \lor φ_{2} ⟧}_{M, V}) \\ ⩾ {(1 - \frac{1}{2 p (n)}) {Pr}_{n} {(⟦ φ_{1} ⟧}_{M, V} | ⟦ φ_{1} \lor φ_{2} ⟧}_{M, V}) + {(1 - \frac{1}{2 p (n)}) {Pr}_{n} {(⟦ φ_{2} ⟧}_{M, V} | ⟦ φ_{1} \lor φ_{2} ⟧}_{M, V}) \\ {- {Pr}_{n} {(⟦ ψ \land φ_{1} \land φ_{2} ⟧}_{M, V} | ⟦ φ_{1} \lor φ_{2} ⟧}_{M, V}) \\ ⩾ {(1 - \frac{1}{2 p (n)}) {Pr}_{n} {(⟦ φ_{1} ⟧}_{M, V} | ⟦ φ_{1} \lor φ_{2} ⟧}_{M, V}) + {(1 - \frac{1}{2 p (n)}) {Pr}_{n} {(⟦ φ_{2} ⟧}_{M, V} | ⟦ φ_{1} \lor φ_{2} ⟧}_{M, V}) \\ {- {Pr}_{n} {(⟦ φ_{1} \land φ_{2} ⟧}_{M, V} | ⟦ φ_{1} \lor φ_{2} ⟧}_{M, V}) \\ {⩾ {(1 - \frac{1}{2 p (n)}) [{Pr}_{n} {(⟦ φ_{1} ⟧}_{M, V} | ⟦ φ_{1} \lor φ_{2} ⟧}_{M, V}) + {Pr}_{n} {(⟦ φ_{2} ⟧}_{M, V} | ⟦ φ_{1} \lor φ_{2} ⟧}_{M, V}) \\ {{- {Pr}_{n} {(⟦ φ_{1} \land φ_{2} ⟧}_{M, V} | ⟦ φ_{1} \lor φ_{2} ⟧}_{M, V})] - \frac{1}{2 p (n)} {Pr}_{n} {(⟦ φ_{1} \land φ_{2} ⟧}_{M, V} | ⟦ φ_{1} \lor φ_{2} ⟧}_{M, V}) \\ ⩾ (1 - \frac{1}{2 p (n)}) - \frac{1}{2 p (n)} \\ = 1 - \frac{1}{p (n)} . \end{array}$ For C4, note that $\begin{matrix} Pr (A_{1} | A_{2} \cap B) = Pr (A_{1} \cap A_{2} | B) / Pr (A_{2} | B) ⩾ Pr (A_{2} \cap A_{2} | B), \end{matrix}$ so the argument follows essentially the same lines as that for C2. Finally, the validity of C5 follows easily from the fact that the truth of a formula of the form $φ \to ψ$ or $\neg (φ \to ψ)$ is independent of the world, and depends only on the probability sequence.

Finally, I must show that (c) implies (b). Suppose not. Then there exists a formula φ such that $PS (Λ) ⊧^{sp} φ$ but $PS (Λ) ⊭ φ$ . Thus, there exists $M \in PS (Λ)$ and valuation V such that $(M, V) ⊭ φ$ . The proof in [17] shows that if a formula is satisfiable with respect to ⊧ at all, then it is satisfiable in a structure in $PS (Λ)$ with a countable domain. Thus, without loss of generality, M has a countable domain. But then it immediately follows from Theorem 3.1 that $PS (Λ) ⊭^{sp} φ$ .3
³
An easy extension of this argument shows that conditions (a), (b), and (c) of Theorem 3.2 are also equivalent to $PS (Λ) ⊧^{ex} φ$ . The argument that the axioms are sound for the $⊧^{ex}$ semantics is similar in spirit to that above showing that they are sound for the $⊧^{sp}$ semantics; this shows that ${AX}_{C}^{Λ} ⊢ φ$ implies $PS (Λ) ⊧^{ex} φ$ . The fact that $PS (Λ) ⊧^{ex} φ$ is equivalent to $PS (Λ) ⊧ φ$ follows from the observation in the previous footnote that Theorem 3.1 also holds for the $⊧^{ex}$ semantics.

□

I next completely characterize reasoning in $L_{C}^{0}$ . (Recall that $L_{C}^{0}$ consists of all formulas of the form $\forall x_{1} \dots \forall x_{n} (φ \to ψ)$ , where φ and ψ are first-order formulas.) More precisely, I characterize when one formula in $L_{C}^{0}$ can be derived from other formulas in $L_{C}^{0}$ , given a first-order theory. I first consider the fragment $L_{C}^{-}$ of $L_{C}^{0}$ consisting of all formulas of the form $φ \to ψ$ where φ and ψ are closed first-order formulas. Thus, $L_{C}^{-}$ does not allow → formulas to be universally quantified. I start by giving a sound and complete axiomatization for expressions of the form $Δ ↪ φ$ , where φ is a formula in $L_{C}^{-}$ and Δ is a set of formulas in $L_{C}^{-}$ . I allow Δ to be infinite here (this seems more consistent with the usage in [22]), but all the results hold without change if Δ is restricted to being finite. (I make comments along the way about the changes needed if Δ is restricted to being finite.) $(M, V) ⊧ Δ ↪ φ$ if $(M, V) ⊧ φ^{'}$ for every formula $φ^{'} \in Δ$ implies that $(M, V) ⊧ φ$ . If Δ is finite, then $(M, V) ⊧ Δ ↪ φ$ iff $(M, V) ⊧ (⋀_{φ^{'} \in Δ} φ^{'}) \Rightarrow φ$ . Thus, if Δ is finite, the $Δ ↪ φ$ is expressible in $L_{C}$ ; I allow the slightly greater generality of infinite sets to be able to relate the results of this paper to earlier work. I write $PS (Λ) ⊧ Δ ↪ φ$ if $(M, V) ⊧ Δ ↪ φ$ for all PS structures M and valuations V.

Consider the following axioms: LLE.
${φ_{1} \to ψ} ↪ (φ_{2} \to ψ)$ if $⊢_{Λ} φ_{1} \Leftrightarrow φ_{2}$ (left logical equivalence).
RW.
${φ \to ψ_{1}} ↪ (φ \to ψ_{2})$ if $⊢_{Λ} ψ_{1} \Rightarrow ψ_{2}$ (right weakening).
REF.
$\emptyset ↪ (φ \to φ)$ (reflexivity).
AND.
${φ \to ψ_{1}, φ \to ψ_{2}} ↪ (φ \to (ψ_{1} \land ψ_{2}))$ .
OR.
${φ_{1} \to ψ, φ_{2} \to ψ} ↪ ((φ_{1} \lor φ_{2}) \to ψ)$ .
CM.
${φ_{1} \to φ_{2}, φ_{1} \to ψ} ↪ ((φ_{1} \land φ_{2}) \to ψ)$ (cautious monotonicity).
TRIV.
$Δ ↪ φ$ if $φ \in Δ$ (trivial).
We have one rule of inference:
TRANS.
From $Δ ↪ ψ$ for all $ψ \in Δ^{'}$ and $Δ^{'} ↪ φ$ infer $Δ ↪ φ$ (transitivity).

This collection of rules has been called system $P_{Λ}$ [22] or the KLM properties.4
⁴
The standard presentation of system $P_{Λ}$ is somewhat different from that given here. For one thing, Λ is not usually mentioned explicitly; I mention it here to make the dependence on Λ clear. For another, the set Δ is typically not included as part of the rule, but is put on the left-hand side of ⊢, so what I am calling an axiom is typically viewed as an inference rule; for example, AND is usually written as “from $φ \to ψ_{1}$ and $φ \to ψ_{2}$ infer $φ \to (ψ_{1} \land ψ_{2})$ ”. Finally, the axiom TRIV and the rule TRANS are not usually given explicitly, but are built into how inference works in $P_{Λ}$ . However, it is easy to see that what I have done here is equivalent to the standard approach.

The rules are obvious analogues of axioms in ${AX}_{C}^{Λ}$ . In particular, LLE is the analogue of R1; and RW is the analogue of R2; REF, AND, and OR are just restatements of C2, C3, and C4, respectively, in this notation.

Note that even if Δ and Λ are infinite, since all the rules are in fact finitary, we have $⊢_{Λ} Δ ↪ φ$ iff there is a finite set $Λ^{'} \subseteq Λ$ and a finite set $Δ^{'} \subseteq Δ$ such that $⊢_{Λ^{'}} Δ^{'} ↪ φ$ . For the completeness result, I make an innocuous technical restriction: I assume that the vocabulary $T$ includes a countably infinite set of constants and there are (as usual) countably many variables, and for every formula $Δ ↪ φ$ , there are infinitely many constants and variables that do not appear in Δ.5
⁵
The assumption holds trivially if Δ is restricted to being a finite set, as long as the set of constants and variables is infinite. Even if Δ can be infinite, we can always add countably infinite fresh constants to $T$ and rename variables, so this restriction is innocuous. The assumption is used in the proof of Theorem 3.4 below, where at one point I need to assume that there infinitely many “fresh” constants and variables that do not appear in Δ or φ. A similar assumption arises in the proof of Theorem 3.3.

The following result is well known.
Theorem 3.3 ([22]).

If $Δ \cup {φ} \subseteq L_{C}^{-}$ , then $P_{Λ} ⊢ Δ ↪ φ$ iff $PS (Λ) ⊧ Δ ↪ φ$ .

I want to extend this result from $L_{C}^{-}$ to $L_{C}^{0}$ ; thus, I now want to allow $Δ \cup {φ} \subseteq L_{C}^{0}$ . I actually extend a little further to allow first-order formulas, so $Δ \cup {φ} \subseteq L^{fo} \cup L_{C}^{0}$ . In addition, I want the axiomatization to be sound and complete for the $⊧^{sp}$ semantics as well as the ⊧ semantics, so as to make it more applicable to reasoning about security protocols.

To get a complete axiomatization, I still need to use the axioms and rules of $P_{Λ}$ , but now I need (special cases of) a few other axioms and rules in ${AX}_{C}^{Λ}$ modified to deal with this language:

C6 ⁺ .

${true \to false} ↪ false$ .

F1 ⁺ .

${\forall x φ} ↪ φ [x / t]$ if t is substitutable for x in φ.

F4 ⁺ .

${x = y, φ_{1}} ↪ φ_{2}$ , where $φ_{1}$ is quantifier-free and $φ_{2}$ is obtained from $φ_{1}$ by replacing zero or more occurrences of x in $φ_{1}$ by y.

F5 ⁺ .

${x \neq y} ↪ N (x \neq y)$ .

IMP.

$Δ ↪ φ$ if $Δ \cup {φ} \subseteq L^{fo}$ , Δ is finite, and $⊢_{Λ} ⋀_{ψ \in Δ} ψ \Rightarrow φ$ (implication).

Gen ⁺ .

If z is a variable that does not appear free in Δ, then (a) if $φ \in L^{fo}$ , then from $Δ \cup {φ [x / z]} ↪ ψ$ infer $Δ \cup {\exists x φ} ↪ ψ$ ; (b) from $Δ ↪ φ [x / z]$ infer $Δ ↪ \forall x φ$ .

Of course, C6⁺, F4⁺ and F5⁺ are just C6, F4, and F5 restated using ↪, F1⁺ is just a special case of F1 (restated using ↪), IMP is a special case of Λ-AX, and Gen⁺ can be viewed as a special case of Gen. (It is not hard to show that it follows from Gen if Δ is finite.) Since I now allow first-order formulas, whose truth depends on the world, I take $(M, V, w) ⊧ Δ ↪ φ$ if $(M, V, w) ⊧ φ^{'}$ for all formulas $φ^{'} \in Δ$ implies $(M, V, w) ⊧ φ$ . I now write $PS (Λ) ⊧ Δ ↪ φ$ if $(M, V, w) ⊧ Δ ↪ φ$ for all PS structures M and valuations V.

Let $P_{Λ}^{+}$ be the axiom system consisting of the axioms and rules of $P_{Λ}$ together with C6⁺, F1⁺, F4⁺, F5⁺, IMP, and Gen⁺. I write $P_{Λ}^{+} ⊢ Δ ↪ φ$ if there is a derivation from $P_{Λ}^{+}$ whose last line in $Δ ↪ φ$ .

Theorem 3.4.
If $Δ \cup {φ} \subseteq L_{C}^{0} \cup L^{fo}$ , then the following are equivalent:
$P_{Λ}^{+} ⊢ Δ ↪ φ$ ;

$PS (Λ) ⊧ Δ ↪ φ$ ;

$PS (Λ) ⊧^{sp} Δ ↪ φ$ .

Proof.
The fact that (a) implies (c) follows from the proof of Theorem 3.2, since all the axioms and rules in $P_{Λ}^{+}$ are essentially (special cases of) axioms and rules in ${AX}_{C}^{Λ}$ . The fact that (c) implies (b) follows just as in the proof of Theorem 3.2, using Theorem 3.1. Thus, it remains to show that (b) implies (a). As usual, for completeness, it suffices to show that if $P_{Λ}^{+} ⊬ Δ ↪ φ$ , then there is a structure $M \in PS (Λ)$ , a valuation V, and a world w such that $(M, V, w) ⊧ Δ$ and $(M, V, w) ⊧ \neg φ$ ; roughly speaking, this says that if $Δ ↪ φ$ is not provable in $P_{Λ}^{+}$ , then its negation is satisfiable.

The proof is quite similar in spirit to the completeness proof for ${AX}_{C}^{Λ}$ given in [17], but there are some subtleties involved in dealing with the restricted language. Specifically, the proof in [17] uses a Henkin-style argument, using maximal consistent sets C of formulas. Because we work here with formulas of the form $Δ ↪ φ$ , we must redefine maximal consistent sets appropriately.

A set $Δ^{'}$ of formulas in $L^{fo} \cup L_{C}^{0}$ is $P_{Λ}^{+}$ -consistent if there is no finite subset $Δ^{″}$ of $Δ^{'}$ such that $⊢_{Λ} Δ^{″} ↪ false$ . If $T^{}$ is a vocabulary and $Y$ is a set of constants and variables, then a maximal* $P_{Λ}^{+} - (T^{} \cup Y)$ -consistent* set of formulas is a $P_{Λ}^{+}$ -consistent set $Δ^{'}$ of formulas that use only symbols in $T^{} \cup Y$ such that if ψ is a formula that uses only symbols in $T^{} \cup Y$ , then $Δ^{'} \cup {ψ}$ is not $P_{Λ}^{+}$ -consistent. $Δ^{'}$ is $T^{} - Y$ -good* if (1) $Δ^{'}$ is a maximal Λ- $(T^{} \cup Y)$ -consistent set of formulas, (2) $\exists x ψ \in Δ^{'} \cap L^{fo}$ implies $\neg ψ [x / y] \in Δ^{'}$ for some $y \in Y$ , (3) if $\forall x φ \in Δ^{'}$ then $φ [x / y] \in Δ^{'}$ for all $y \in Y$ , and (4) if $y = y^{'}$ (resp., $y \neq y^{'}$ ) is in Δ for $y, y^{'} \in Y$ , then so is $N (y = y^{'})$ (resp., $N (y \neq y^{'})$ ).6
⁶
This is an adaptation of the definition of $C$ -good given in [17], where the notion was applied to sets of formulas in $L_{C}$ and a set $C$ of constants.

Let $C$ be a countably infinite set of constants not in Δ or φ such that there are countably many constants in $T$ not in $C$ , Δ, or φ. (Our technical assumption ensures that such a sets $C$ exists.) Lemma 3.5.
If $P_{Λ}^{+} ⊬ Δ ↪ φ$ , then there exists a* $C$ -good set $Δ^{} \supseteq Δ$ such that* $P_{Λ}^{+} ⊬ Δ^{} ↪ φ^{}$ , where $φ^{} = φ$ if $φ \in L^{fo}$ and* $φ^{} = φ^{'} [x_{1} / c_{1}, \dots, x_{k} / c_{k}]$ if φ has the form* $\forall x_{1} \dots \forall x_{k} φ^{'}$ , where $φ^{'}$ is quantifier-free and $c_{1}, \dots, c_{k}$ are constants in $C$ . 7
⁷
If the set Δ is restricted to being finite in formulas of the form $Δ ↪ ψ$ , then we replace the requirement $P_{Λ}^{+} ⊬ Δ^{} ↪ φ^{}$ by $P_{Λ}^{+} ⊬ Δ^{″} ↪ φ^{}$ for all finite $Δ^{″} \subseteq Δ^{}$ . Analogous changes must be made throughout the proof.

Once Lemma 3.5 is proved, the rest of the argument follows essentially the same lines as that of [17], so I just briefly outline the argument here. For each $c \in C$ , let $[c] = {c^{'} : c = c^{'} \in Δ^{}}$ . We construct a model $M = (D, W, π, P)$ where $D = {[c] : c \in C}$ , W consists of all the $C$ -good sets $Δ^{'}$ such that $Δ^{'} \cap L_{C}^{0} = Δ^{} \cap L_{C}^{0}$ (so that worlds are $C$ -good sets), and π is such that, for all $Δ^{'} \in W$ , we have $π (c, Δ^{'}) = [c]$ and, for each atomic formula ψ, $(M, Δ^{'}) ⊧ ψ$ iff $ψ \in Δ^{'}$ . This is consistent, since all sets $Δ^{'}$ in W agree on formulas of the form $N (c = c^{'})$ and $N (c \neq c^{'})$ , and hence (since $Δ^{'}$ is $C$ -good) on formulas of the form $c = c$ and $c \neq c^{'}$ ; thus, the formula $c = c^{'}$ is in $Δ^{'}$ iff $π (c^{'}, Δ^{'}) = π (c^{'}, Δ^{'}) = [c]$ . As shown in [17], it is possible to define a sequence $P$ of probability measures such that $M ⊧ ψ$ iff $ψ \in Δ^{}$ for all quantifier-free closed formulas $ψ \in Δ^{} \cap L_{C}^{0}$ (note that if $ψ \in Δ^{} \cap L_{C}^{0}$ , then $ψ \in Δ^{'} \cap L_{C}^{0}$ for all $Δ^{'} \in W$ ), and, if φ has the form $\forall x_{1} \dots \forall x_{k} φ^{'}$ , then $(M, Δ^{}) ⊧ \neg (φ^{'} [x_{1} / c_{1}, \dots, x_{1} / c_{k}])$ . This gives us the desired model.

So, to complete the proof of Theorem 3.4, it remains to prove Lemma 3.5. To do this, I construct $Δ^{}$ in stages. Starting with Δ, at each stage I add more and more formulas until I get a set $Δ^{}$ that is $C$ -good. Let $X$ be the set of variables that appear in Δ and φ, and let $Y$ be a countably infinite set of variables not in Δ or φ such that there are countably many variables not in $Y$ , Δ, or φ. (Again, our assumptions guarantee that such a set $Y$ exists.) If $φ \in L_{C}^{0}$ , suppose that $φ = \forall x_{1} \dots \forall x_{k} φ^{'}$ . For convenience suppose that $Y$ has the form ${y_{1}, \dots, y_{k}, z_{1}, z_{2}, z_{3}, \dots}$ . (If $φ \in L^{fo}$ , then we can just take $Y = {z_{1}, z_{2}, z_{3}, \dots}$ .) Let $φ^{+} = φ$ if $φ \in L^{fo}$ and $φ [x_{1} / y_{1}, \dots, x_{k} / y_{k}]$ otherwise. Clearly $\begin{matrix} (2) & P_{Λ}^{+} ⊬ Δ ↪ φ^{+} . \end{matrix}$ This is immediate if $φ \in L^{fo}$ , since in that case $φ^{+} = φ$ . And if φ has the form $\forall x_{1} \dots \forall x_{k} φ^{'}$ and $P_{Λ}^{+} ⊢ Δ ↪ φ^{'} [x_{1} / y_{1}, \dots, x_{k} / y_{k}]$ , then it follows from Gen⁺(b) that $P_{Λ}^{+} ⊢ Δ ↪ φ$ , contradicting our assumption.

Let $σ_{1}, σ_{2}, \dots$ be an enumeration of formulas in $L^{fo} \cup L_{C}^{0}$ over the vocabulary $T$ whose only (free or bound) variables are in $Y$ . We define a sequence of set $Δ_{0}, Δ_{1}, \dots$ inductively. Let $Δ_{0} = Δ$ . Suppose that $Δ_{1}, \dots, Δ_{m}$ have been defined. Let $\exists x ψ$ be the $(m + 1) st$ existential first-order formula in the enumeration. Let $Δ_{m + 1} = Δ_{m} \cup {\exists x ψ \Rightarrow ψ [x / z_{m + 1}]}$ and let $Δ^{+} = ⋃_{m} Δ^{m}$ . I claim that $\begin{matrix} (3) & P_{Λ}^{+} ⊬ Δ^{+} ↪ φ^{+} . \end{matrix}$ If not, since $P_{Λ}^{+} ⊬ Δ ↪ φ$ , there must exist some m such that $P_{Λ}^{+} ⊬ Δ^{m} ↪ φ$ and $P_{Λ}^{+} ⊢ Δ^{m + 1} ↪ φ$ . Since $Δ^{m + 1} = Δ^{m} \cup {\exists x ψ \Rightarrow ψ [x / z_{m + 1}]}$ and, by construction, $z_{m + 1}$ does not appear in $Δ^{m}$ or φ, it follows from Gen⁺(a) that $P_{Λ}^{+} ⊬ Δ^{m} \cup {\exists x (\exists x ψ \Rightarrow ψ)} ↪ φ$ . It is easy to see that $\exists x (\exists x ψ \Rightarrow ψ)$ is a valid first-order formula. Thus, by IMP, $P_{Λ}^{+} ⊢ \emptyset ↪ \exists x (\exists x ψ \Rightarrow ψ)$ . It thus follows from TRANS that $P_{Λ}^{+} ⊢ Δ^{m} ↪ φ$ , a contradiction.

I next construct a sequence $Δ_{0}^{+}, Δ_{1}^{+}, \dots$ inductively, by taking $Δ_{0}^{+} = Δ_{0}$ , and taking $Δ_{m + 1}^{+} = Δ_{m}^{+} \cup {σ_{m + 1}}$ if $P_{Λ}^{+} ⊬ Δ_{m}^{+} \cup {σ_{m}} ↪ φ$ and $Δ_{m + 1}^{+} = Δ_{m}^{+}$ otherwise. Let $Δ^{†} = ⋃_{m} Δ_{m}^{+}$ . It is clear from the construction that $P_{Λ}^{+} ⊬ Δ_{m}^{+} ↪ φ^{+}$ for all m; thus, $\begin{matrix} (4) & P_{Λ}^{+} ⊬ Δ^{†} ↪ φ^{+} . \end{matrix}$ Several other properties of $Δ^{†}$ must be noted. First, the construction guarantees that if a first-order formula of the form $\exists x ψ$ is in $Δ^{†}$ , then $ψ [x / y] \in Δ^{†}$ for some $y \in Y$ . It easily follows from F1⁺ that if $\forall x φ \in Δ^{†}$ then $φ [x / y] \in Δ^{†}$ for all $y \in Y$ . Moreover, it follows from F5⁺ that if $y \neq y^{'} \in Δ^{†}$ for $y, y^{'} \in Y$ then $N (y \neq y^{'}) \in Δ^{†}$ . Finally, it is easy to see that if $x = y \in Δ^{†}$ , then $N (x = y) \in Δ^{†}$ . (Proof: first observe that $P_{Λ}^{+} ⊢ \emptyset ↪ (false \to false)$ by REF and $⊢_{Λ} x \neq x \Leftrightarrow false$ , so $P_{Λ}^{+} ⊢ \emptyset ↪ (x \neq x) \to false$ , by LLE. Recall that, by definition, $(x \neq x) \to false = N (x = x)$ . By F4⁺, $P_{Λ}^{+} ⊢ {N (x = x), x = y} ↪ N (x = y)$ . By TRANS, $P_{Λ}^{+} ⊢ {x = y} ↪ N (x = y)$ . It easily follows that if $x = y \in Δ^{†}$ , then $N (x = y) \in Δ^{†}$ .)

Let $Δ^{}$ be the result of replacing all occurrences of $y_{j}$ in $Δ^{†}$ by $c_{j}$ , for $j = 1, \dots, k$ and replacing all occurrences of $z_{j}$ in $Δ^{†}$ by $d_{j}$ for $j = 1, 2, 3, \dots$ ; similarly, let $φ^{}$ be the result of replacing all occurrences (if any) of $y_{j}$ in $φ^{+}$ by $c_{j}$ . It is easy to see that $Δ^{}$ is $C$ -good, and that $P_{Λ}^{+} ⊬ Δ^{} ↪ φ^{*}$ (if this is not the case, then it is immediate that (4) does not hold either). This completes the proof of Lemma 3.5 and, with it, the proof of Theorem 3.4. □

3.2. Quantitative reasoning

The super-polynomial semantics just talks about asymptotic complexity. It says that for all k, the conclusion will hold with probability greater than $1 - 1 / n^{k}$ for sufficiently large n, provided that the assumptions hold with sufficiently high probability, where n can be, for example, the security parameter. While this asymptotic complexity certainly gives insight into the security of a protocol, in practice, a system designer wants to achieve a certain level of security, and needs to know, for example, how large to take the keys in order to achieve this. In this section, I provide a more quantitative semantics appropriate for such reasoning, and relate it to the more qualitative “asymptotic” semantics.

The syntax of the quantitative language, which is denoted $L_{C, q}$ , is just like that of the qualitative language, except that, instead of formulas of the form $φ \to ψ$ , there are formulas of the form $φ \to^{r} ψ$ , where r is a real number in $[0, 1]$ . The semantics of such a formula is straightforward: $\begin{array}{l} (M, V) ⊧ φ \to^{r} ψ if there exists some n^{*} ⩾ 0 such that for all n ⩾ n^{*}, \\ {{Pr}_{n} {(⟦ ψ ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) ⩾ 1 - r . \end{array}$ Let $L_{C, q}^{0}$ be the obvious analogue of $L_{C}^{0}$ , consisting of all formulas of the form $\forall x_{1} \dots \forall x_{n} (φ \to^{r} ψ)$ , where φ and ψ are first-order formulas.

Because $L_{C, q}^{0}$ does not really consider limiting probability, it would be straightforward to give it semantics using a single probability measure Pr. That is, if a model M involves just a single distribution Pr rather than a sequence $({Pr}_{1}, {Pr}_{2}, \dots)$ , then we could take $(M, V) ⊧ φ \to^{r} ψ$ if ${Pr {(⟦ ψ ⟧}_{M, V} | ⟦ φ ⟧}_{M, V}) ⩾ 1 - r$ . Indeed, that is essentially the semantics used in [14], where the focus is on quantitative security. I continue to use a sequence of probability measures here, since my goal is to relate quantitative proofs to qualitative proofs.

That said, it is not hard to show that the same formulas are valid for the language $L_{C, q}^{0}$ whether we consider a single probability measure or a sequence of probability measures in the semantics. This makes $L_{C, q}^{0}$ closer to other approaches that have used probability and classical implication. A recent example is the work of Atserias and Balcázar [3]. They consider formulas of the form $X \to Y$ , where X and Y are sets of attributes, and can be identified with conjunctions of primitive propositions. Changing the notation of Atserias and Balcázar to be compatible with that of this paper, $Pr ⊧_{γ} X \to Y$ if $Pr (Y | X) ⩾ γ$ . Given a set Δ of such formulas, $Pr ⊧_{γ} Δ ↪ (X \to Y)$ if $Pr (Y^{'} | X^{'}) ⩾ γ$ for all $X^{'} \to Y^{'} \in Δ$ implies $Pr (Y | X) ⩾ γ$ . Atserias and Balcázar provide algorithms for checking when such entailments hold, using linear programming. Note that in Atserias and Balcàzar’s work, the same γ is used for the hypothesis and the conclusion in the entailment; it will be crucial for my main result that it is possible to use different parameters (the framework used here allows us to write the parameter explicitly in the formula).

I now explain how qualitative reasoning in $L_{C}^{0}$ and quantitative reasoning in $L_{C, q}^{0}$ can be related. First note that for each of the axioms and rules in system $P_{Λ}^{+}$ , there is a corresponding sound axiom or rule in $L_{C, q}^{0}$ . Consider the following axioms:

LLE ^q .

${φ_{1} \to^{r} ψ} ↪ (φ_{2} \to^{r} ψ)$ if $⊢_{Λ} φ_{1} \Leftrightarrow φ_{2}$ .

RW ^q .

${φ \to^{r} ψ_{1}} ↪ (φ \to^{r} ψ_{2})$ if $⊢_{Λ} ψ_{1} \Rightarrow ψ_{2}$ .

REF ^q .

$\emptyset ↪ (φ \to^{0} φ)$ .

AND ^q .

${φ \to^{r_{1}} ψ_{1}, φ \to^{r_{2}} ψ_{2}} ↪ (φ \to^{r_{3}} (ψ_{1} \land ψ_{2}))$ , where $r_{3} = min (r_{1} + r_{2}, 1)$ .

OR ^q .

${φ_{1} \to^{r_{1}} ψ, φ_{2} \to^{r_{2}} ψ} ↪ ((φ_{1} \lor φ_{2}) \to^{r_{3}} ψ)$ , where $r_{3} = min (max (2 r_{1}, 2 r_{2}), 1)$ .

CM ^q .

${φ_{1} \to^{r_{1}} φ_{2}, φ_{1} \to^{r_{2}} ψ} ↪ ((φ_{1} \land φ_{2}) \to^{r_{3}} ψ)$ , where $r_{3} = min (r_{1} + r_{2}, 1)$ .

C6 ^q .

${true \to^{r} false} ↪ false$ for all $r \in [0, 1)$ .

F5 ^q .

${x \neq y} ↪ N^{0} (x \neq y)$ , where $N^{0} φ$ is an abbreviation for $\neg φ \to^{0} false$ .

Let $P_{Λ}^{+, q}$ consist of the rules above, together with TRIV, F1⁺, F4⁺, IMP, Gen⁺, and TRANS (all of which hold with no change in the quantitative setting), and

INC.

${φ \to^{r_{1}} ψ} ↪ (φ \to^{r_{2}} ψ)$ if $r_{1} ⩽ r_{2}$ (increasing superscript).

Theorem 3.6.
The rules in $P_{Λ}^{+, q}$ are all sound.
Proof.
The soundness of the quantitative analogues of the rules in $P_{Λ}$ is immediate from the proof of Theorem 3.2. The soundness of remaining rules holds as it did before (since they are unchanged). □

I do not believe that $P_{Λ}^{+, q}$ is complete, nor do I have a candidate complete axiomatization for the quantitative language. Nevertheless, as the proofs in [14] show, $P_{Λ}^{+, q}$ (when combined with axioms for reasoning about actions and partial correctness) suffices for proving many results of interest in security. Moreover, as I now show, there is a deep relationship between $P_{Λ}^{+}$ and $P_{Λ}^{+, q}$ . To make it precise, given a set of formulas $Δ \subseteq L^{fo} \cup L_{C}^{0}$ , say that $Δ^{'} \subseteq L^{fo} \cup L_{C, q}^{0}$ is a quantitative instantiation of Δ if there is a bijection f from Δ to $Δ^{'}$ such that, for every formula $φ \to ψ \in Δ$ , there is a real number $r \in [0, 1]$ such that $f (φ) = φ^{r}$ , where $φ^{r} = φ$ if $φ \in L^{fo}$ , and ${(\forall x_{1} \dots \forall x_{k} (φ^{'} \to ψ))}^{r} = \forall x_{1} \dots \forall x_{k} (φ^{'} \to^{r} ψ)$ . That is, $Δ^{'}$ is a quantitative instantiation of Δ if each qualitative formula in Δ has a quantitative analogue in $Δ^{'}$ .

Although the proof of the following theorem is straightforward, it shows the power of using of $P_{Λ}^{+}$ . Specifically, it shows that if $Δ ↪ φ$ is derivable in $P_{Λ}^{+}$ then, for all $r \in [0, 1]$ , there exists a quantitative instantiation $Δ^{'}$ of Δ such that $Δ^{'} ↪ φ^{r}$ is derivable in $P_{Λ}^{+, q}$ . Thus, if the system designer wants security at level r (that is, she wants to know that a desired security property holds with probability at least $1 - r$ ), then if she has a qualitative proof of the result, she can compute the strength with which her assumptions must hold in order for the desired conclusion to hold. For example, she can compute how to set the security parameters in order to get the desired level of security. This result can be viewed as justifying qualitative reasoning. Roughly speaking, it says that it is safe to avoid thinking about the quantitative details, since they can always be derived later. Note that this result would not hold if the language allowed negation. For example, even if $\neg (φ \to ψ)$ could be proved given some assumptions (using the axiom system ${AX}_{C}^{Λ}$ ), it would not necessarily follow that $\neg (φ \to^{q} ψ)$ holds, even if the probability of the assumptions was taken arbitrarily close to one.
Theorem 3.7.
If $P_{Λ}^{+} ⊢ Δ ↪ φ$ , then for all $r \in [0, 1]$ , there exists a quantitative instantiation $Δ^{'}$ of a finite subset $Δ^{″}$ of Δ such that $P_{Λ}^{+, q} ⊢ Δ^{'} ↪ φ^{r}$ . Moreover, $Δ^{'}$ can be found in polynomial time, given the derivation of $Δ ↪ φ$ .
Proof.
Intuitively, $Δ^{″}$ consists of the formulas in Δ needed for the proof of $Δ ↪ φ$ . The existence of $Δ^{'}$ follows by a straightforward induction on the length of the derivation. If it has length 1, then the proof must be an instance of an axiom. In this case, the argument proceeds by considering each axiom in turn. The arguments are all straightforward. I consider a few representative cases here. If the axiom TRIV was applied, then it must be the case that $φ \in Δ$ , so we can take $Δ^{″} = {φ}$ and $Δ^{'} = {φ^{r}}$ . If REF was applied, the φ has the form $φ^{'} \to φ^{'}$ . In this case, take $Δ^{″} = \emptyset$ . By REF^q, $\emptyset ↪ (φ^{'} \to^{0} φ^{'})$ . The conclusion now follows from INC. If AND was applied, then φ must have the form $φ^{'} \to ψ_{1} \land ψ_{2}$ , where $φ^{'} \to ψ_{1}, φ^{'} \to ψ_{2} \in Δ$ . Let $Δ^{″} = {φ^{'} \to ψ_{1}, φ^{'} \to ψ_{2}}$ . Choose $s_{1}, s_{2} \in [0, 1]$ such that $s_{1} + s_{2} = r$ .8
⁸
It suffices to take $s_{1} = s_{2} = r / 2$ , but there is an advantage to having this greater flexibility; see the discussion after the proof.

Let $Δ^{'} - {φ^{'} \to^{s_{1}} ψ_{1}, φ^{'} \to^{s_{2}} ψ_{2}}$ . By AND^q, it easily follows that $P_{Λ}^{+, q} Δ^{'} ↪ (φ \to^{r} (ψ_{1} \land ψ_{2}))$ . The argument for all the other axioms in $P_{Λ}^{+}$ is similar and left to the reader.

Now suppose that the derivation of $Δ ↪ φ$ has length $N > 1$ . If the last line of the derivation is an axiom, the argument above applies without change. Otherwise, it must be the result of applying Gen⁺(a), Gen⁺(b), or TRANS. I consider the latter two cases here; the case of Gen⁺(a) is straightforward and left to the reader. If Gen⁺(b) was applied, then φ has the form $\forall x φ^{'}$ and there is a derivation $Δ ↪ φ [x / z]$ of length less than N, where z does not appear in Δ. By the induction hypothesis, there is a subset $Δ^{″}$ of Δ and instantiation of $Δ^{'}$ of $Δ^{″}$ such that $P_{Λ}^{+, q} ⊢ Δ^{'} ↪ {(φ^{'})}^{r} [x / z]$ . Since $φ^{r} = {(\forall x φ^{'})}^{r} = \forall x ({(φ^{'})}^{r})$ , by Gen⁺(a), it follows that $P_{Λ}^{+, q} ⊢ Δ^{'} ↪ φ^{r}$ .

Finally, if the last step in the proof of $Δ ↪ φ$ is an application of TRANS, then there exists $Δ_{1} \subseteq Δ$ such that $P_{Λ}^{+} ⊢ Δ ↪ ψ$ for all $ψ \in Δ_{1}$ and $P_{Λ}^{+} ⊢ Δ_{1} ↪ φ$ . By the induction hypothesis, there exists a finite subset $Δ_{2}$ of $Δ_{1}$ and a quantitative instantiation $Δ_{2}^{'}$ of $Δ_{2}$ such that $P_{Λ}^{+, q} ⊢ Δ_{2}^{'} ⊢ φ^{r}$ . By the induction hypothesis again, for each formula $ψ^{s} \in Δ_{2}^{'}$ , there exists a finite subset $Δ_{ψ}$ of Δ and a quantitative instantiation $Δ_{ψ}^{'}$ of $Δ_{ψ}$ such that $P_{Λ}^{+, q} ⊢ Δ_{ψ}^{'} ↪ ψ^{s}$ . Let $Δ^{″} = ⋃_{ψ \in Δ_{2}} Δ_{ψ}$ and let $Δ^{'} = ⋃_{ψ \in Δ_{2}} Δ_{ψ}^{'}$ . By TRANS, we have $P_{Λ}^{+, q} Δ^{'} ↪ φ^{r}$ , as desired.

This argument also shows that finding $Δ^{'}$ from the proof of $Δ ↪ (φ \to ψ)$ just involves solving some simple linear inequalities, which can be done in polynomial time. □

The proof of Theorem 3.7 gives even more useful information to the system designer. In general, there may be a number of quantitative instantiations $Δ^{'}$ of Δ that give the desired conclusion. For example, as the proof shows, if the AND rule is used in the qualitative proof, and we want the conclusion to hold at level r, we must just choose $s_{1}$ and $s_{2}$ such that $φ \to ψ_{1}$ and $φ \to ψ_{2}$ hold at level $s_{1}$ and $s_{2}$ , respectively. If the system designer finds it easier to satisfy the first formula than the second (for example, the first may involve the length of the key, while the second may involve the degree of trustworthiness of one of the participants in the protocol), there may be an advantage in choosing $s_{1}$ relatively small and $s_{2}$ larger. As long as $s_{1} + s_{2} = r$ , the desired conclusion will hold.

Given r, we might wonder how close to optimal the q we can find in Theorem 3.7 is. While I cannot give a definitive answer here, the following comments may give some insight. For each axiom individually, the quantitative instantiation is optimal, in the sense that it is not hard to find examples where the bounds are satisfied with equality. For example, in the AND^q rule, we cannot do better in general than taking $r_{3} = min (r_{1} + r_{2}, 1)$ . However, it could well be that when putting several steps in a proof together, we end up with a significant overestimate. Different proofs of the same conclusion might lead to different estimates. That also suggests that developing new proof rules might be useful, since they might result in better estimates.
4. Discussion

I have shown how the intuition behind the ⊃ operator used by Datta et al. [13] can be captured using the well-studied conditional implication operator →, where $φ \to ψ$ is interpreted as “the probability of ψ conditional on φ converges to 1” (or converges to 1 super-polynomially). Using → with this interpretation has a significant advantage: it allows us to relate quantitative and qualitative reasoning. Specifically, for a rich fragment $L_{C}^{0}$ of full first-order conditional logic, I have shown that if φ is provable from a collection Δ of formulas in $L_{C}^{0} \cup L^{fo}$ , then, for all r, there exists a quantitative instantiation $Δ^{'}$ of a finite subset of Δ, computable in time polynomial in the length of the proof of $Δ ↪ φ$ , such that $φ^{r}$ is provable from $Δ^{'}$ . That mean that once we have a qualitative proof of a fact of interest from some assumptions, we can compute the strength of the assumptions needed to reach that conclusion.

I have suggested that this result is applicable to reasoning about quantitative security. This statement must be interpreted carefully. While $L_{C}^{0}$ is a rich fragment of $L_{C}$ , it clearly does not suffice for stating and proving interesting facts about security programs. To do that, we need more operators than just those for reasoning about (conditional) probability. For example, the logic used in [14] includes Hoare-like assertions of the form $φ [program] ψ$ and included axioms about the predictability of nonces and the unforgeability of signatures. Even if we had a completeness theorem for the fragment of the logic that does not involve the → operator (which we do not), there may be interactions between the → operator and the other operators. So while the axioms of this paper are still sound, it is unlikely that they will be enough for completeness (even when they are added to complete axiomatizations for the other operators). The fact that (as shown by Theorem 3.1) that the language cannot distinguish super-polynomial convergence from non-super-polynomial convergence is further evidence that the logic cannot capture all that is needed for proving correctness of security protocols.

Nevertheless, that does not render the results of this paper irrelevant for security. Even in a richer logic, Theorem 3.7 still holds. More precisely, if there is a qualitative proof of a fact of the form $Δ ↪ φ$ using only the axioms and rules of $P_{Λ}^{+}$ for reasoning about → (or, more generally, using only axioms and rules that have quantitative analogues (as the axioms and rules of $P_{Λ}^{+}$ do)), then, for all r, we can find a quantitative instantiation $Δ^{'}$ of a finite subset of Δ such that $Δ^{'} ↪ φ^{r}$ is provable. In [14], nontrivial quantitative properties of a challenge-response protocol are proved using the axioms of $P_{Λ}^{+, q}$ and axioms involving $\to^{q}$ that talk about properties of nonces and the likelihood that a signature can be forged. Interestingly, the superscript q used in the proof (and in the axioms that talk about the properties of nonces and unforgeability) is not a constant, but a function of the security parameter (and other parameters); this does not affect the arguments about $\to^{q}$ at all (all the axioms of this paper still hold), but again, makes it more applicable to security. It is easy to transform the quantitative proof given in [14] to a qualitative proof of a conclusion of the form $Δ ↪ φ$ where the only axioms used for reasoning about → are those in $P_{Λ}^{+}$ . We simply erase the superscript on →, and put (qualitative versions of) the axioms for nonces and unforgeability into Δ. Now Theorem 3.7 can be used, for example, to deduce the strength of security parameter needed to get the conclusion to hold with a given strength. Put another way, we can think of the proof in [14] as going in the “forward” direction: given assumptions about the security parameter and unforgeability, we prove that a conclusion about the security protocol holds with a certain probability. Theorem 3.7 lets us go in the “backward” direction: after proving a result qualitatively, we can deduce the strength that the assumptions need to hold with to be able to get the conclusion to hold with a given strength. It seems to me that both directions are of practical interest.

It is perhaps also worth noting that one of the features of the logic considered here is that it allows us to make statements about conditional probability; the formula $φ \to ψ$ is making a statement about the probability of φ conditional on ψ. Most of the security analyses in the literature have focused on unconditional probability; this amounts to considering formulas of the form $true \to ψ$ . (This is the case for the analyses done by Datta et al. [14], for example.) One reason for the focus on unconditional probability may be that the guarantees provided by cryptographic schemes are typically unconditional guarantees (or, at least, their formalizations avoid the use of unconditional probabilities). For example, when we say that a signature scheme has only a negligible probability of being broken, we take this probability to be unconditional (i.e., relative to the whole space). A signature scheme is considered secure even if someone broadcasts all the secret keys, as long as this is done with exponentially small probability. Of course, conditional on getting the secret keys, the system is highly insecure. But we don’t tend to worry about that in our proofs; it is a negligible event.

As shown by the analysis of Datta et al. [14], the logic considered here is of interest even in the unconditional case (i.e., if we restrict to formulas of the form $true \to ψ$ or $true \to^{r} φ$ ). Moreover, although current analyses seem to focus on the unconditional case, it seems to me that a more refined security analysis might want to take into account some conditional probabilities: we might be interested, for example, in how secure a system would be if one of the agents in the system chose a somewhat weak key or inadvertently changed some security settings in a system. Note that once we allow nontrivial formulas φ in the antecedent of →, it becomes critical that → is nonmonotonic. While a conclusion of the form $true \to ψ$ may be sound, a conclusion of the form $φ \to ψ$ may not be, if φ is an unlikely event (like an agent inadvertently changing some security setting).

Finally, it is worth considering in a little more detail the relationship between this work and that of Bana, Hasebe, and Okada [4]. As I mentioned in the introduction, they also use a → operator. They give semantics to their → operator relative to a sequence $P$ of probability measures, just as I do, but the technical details of their semantics are quite different from the semantics I use.9

⁹

In more detail, for Bana et al., each probability measure ${Pr}_{n}$ is a measure on a possibly different domain $W_{n}$ . They also consider sequences $S = (S_{1}, S_{2}, \dots)$ , where $S_{n} \subseteq W_{n}$ , in giving the semantics of formulas. Very roughly speaking, $(P, S) ⊧ φ \to ψ$ if $(P, S) ⊧ □ (p \Rightarrow q)$ , where $□ φ$ holds if φ holds for all non-negligible subsets $S^{'}$ of S, and $S^{'} = (S_{1}^{'}, S_{2}^{'}, \dots)$ is a non-negligible subset of S if $S_{n}^{'} \subseteq S_{n}$ for all n and ${Pr}_{n} (S_{n}^{'})$ is non-negligible as a function of n, that is, ${Pr}_{n} (Ω_{n} - S_{n})$ does not grow super-polynomially.

There are clearly significant differences between the two semantics for →. In the semantics for → that I have used, there is no analogue to the sequence S of events. Moreover, my focus is on events whose probability increases (super-polynomially) to 1, rather than non-negligible events. As an anonymous reviewer pointed out, we could make the two approaches somewhat closer by viewing the measures ${Pr}_{n}$ used by Bana et al. as all being defined on a single space $Ω = W_{1} \times W_{2} \times \dots$ (i.e., the crossproduct of the domain of ${Pr}_{n}$ ’s), where the measurable subsets of Ω are those of the form $A_{1} \times A_{2} \times \dots$ and $A_{n}$ is a measurable subset of $W_{n}$ , defining ${Pr}_{n} (A_{1} \times A_{2} \times \dots) = {Pr}_{n} (A_{n})$ , and identifying a sequence $S^{'} = (S_{1}^{'}, S_{2}^{'}, \dots)$ where $S_{n}^{'} \subseteq W_{n}$ with the subset $S_{1}^{'} \times S_{2} \times \dots$ of Ω. But even with these identifications, the other differences pointed out above still remain.

Bana et al. work purely at the qualitative level; they have no “concrete” analogue

\to^{r}

to their → operator. Thus, they make no attempt to relate their quatitative semantics to a more quantitative semantics. That said, they are very interested in relating qualitative work on what they call symbolic adversaries to more quantitative work on verification that works directly on models that involve probability. So, their goals are the same as mine. More experience is needed to determine which logic is better suited to reasoning about such programs. However it is done, as I hope the results of this paper have made clear, a logic with conditional statements can be an extremely useful addition to a security analyst’s toolkit.

Footnotes

Acknowledgments

Work supported in part by NSF under grants IIS-0812045, IIS-0911036, and CCF-1214844 ITR-0325453 and IIS-0534064, and by AFOSR under grant FA9550-05-1-0055.

I thank Anupam Datta, John Mitchell, Riccardo Pucella, Arnab Roy, and Shayak Sen for many useful discussions on applying conditional logic to security protocols. The anonymous reviewers of the paper provided many helpful suggestions as well.

References

Abadi and

Rogaway, Reconciling two views of cryptography (the computational soundness of formal encryption), in: Proc. IFIP International Conference on Theoretical Computer Science (TCS’00), Lecture Notes in Computer Science, Vol. 1872, Springer-Verlag, 2000, pp. 3–22.

Adams, The Logic of Conditionals. Reidel, Dordrecht, Netherlands, 1975. doi:10.1007/978-94-015-7622-2.

Atserias and

J.L.

Balcázar, Entailment among probabilistic relations, in: Proc. 30th IEEE Symposium on Logic in Computer Science, 2015, pp. 621–632.

Bana,

Hasebe and

Okada, Computationally complete symbolic attacker and key exchange, in: Proc. 13th ACM SIGSAC Conference on Computer and Communications Security (CCS ’13), 2013, pp. 1231–1246.

Barthe,

Grégoire,

Heraud and

Zanella-Béguelin, Computer-aided security proofs for the working cryptographer, in: Advances in Cryptology (CRYPTO 2011),

Rogaway, ed., Lecture Notes in Computer Science, Vol. 6841, 2011, pp. 71–90. doi:10.1007/978-3-642-22792-9_5.

Barthe,

Grégoire and

Zanella-Béguelin, Formal certification of code-based cryptographic proofs, SIGPLAN Notices 44(1) (2009), 90–101. doi:10.1145/1594834.1480894.

Bella and

L.C.

Paulson, Kerberos version IV: Inductive analysis of the secrecy goals, in: Proc. 5th European Symposium on Research in Computer Security,

J.-J.

Quisquater, ed., LNCS, Vol. 1485, Springer-Verlag, 1998, pp. 361–375.

Bellare,

Canetti and

Krawczyk, A modular approach to the design and analysis of authentication and key exchange protocols, in: Proc. 30th Annual Symposium on the Theory of Computing, 1998, pp. 419–428.

Blanchet, A computationally sound mechanized prover for security protocols, in: IEEE Symposium on Security and Privacy, 2006, pp. 140–154.

10.

Borisov,

Goldberg and

Wagner, Intercepting mobile communications: The insecurity of 802.11, in: Proc. 7th Annual International Conference on Mobile Computing and Networking, 2001, pp. 180–189.

11.

Burgess, Quick completeness proofs for some logics of conditionals, Notre Dame Journal of Formal Logic 22 (1981), 76–84. doi:10.1305/ndjfl/1093883341.

12.

Datta,

Derek,

J.C.

Mitchell and

Roy, Protocol composition logic (PCL), Electronic Notes Theoretical Computer Science 172 (2007), 311–358. doi:10.1016/j.entcs.2007.02.012.

13.

Datta,

Derek,

J.C.

Mitchell,

Shmatikov and

Turuani, Probabilistic polynomial-time semantics for a protocol security logic, in: 32nd International Colloquium on Automata, Languages, and Programming (ICALP), 2005, pp. 16–29. doi:10.1007/11523468_2.

14.

Datta,

J.Y.

Halpern,

J.C.

Mitchell,

Roy and

Sen, A symbolic logic with concrete bounds for cryptographic protocols, 2015, Available at: http://arxiv.org/abs/1511.07536.

15.

H.B.

Enderton, A Mathematical Introduction to Logic, Academic Press, New York, 1972.

16.

Friedman and

J.Y.

Halpern, Plausibility measures and default reasoning, Journal of the ACM 48(4) (2001), 648–685. doi:10.1145/502090.502092.

17.

Friedman,

J.Y.

Halpern and

Koller, First-order conditional logic for default reasoning revisited, ACM Trans. on Computational Logic 1(2) (2000), 175–207. doi:10.1145/359496.359500.

18.

Geffner, High probabilities, model preference and default arguments, Mind and Machines 2 (1992), 51–70.

19.

Goldreich, Foundations of Cryptography, Vol. 1, Cambridge University Press, 2001.

20.

Goldszmidt,

Morris and

Pearl, A maximum entropy approach to nonmonotonic reasoning, IEEE Transactions of Pattern Analysis and Machine Intelligence 15(3) (1993), 220–232. doi:10.1109/34.204904.

21.

Goldszmidt and

Pearl, Rank-based systems: A simple approach to belief revision, belief update and reasoning about evidence and actions, in: Principles of Knowledge Representation and Reasoning: Proc. Third International Conference (KR ’92), 1992, pp. 661–672.

22.

Kraus,

Lehmann and

Magidor, Nonmonotonic reasoning, preferential models and cumulative logics, Artificial Intelligence 44 (1990), 167–207. doi:10.1016/0004-3702(90)90101-5.

23.

Mitchell,

Mitchell and

Stern, Automated analysis of cryptographic protocols using Murφ, in: Proc. 1997 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1997, pp. 141–151. doi:10.1109/SECPRI.1997.601329.

24.

J.C.

Mitchell,

Shmatikov and

Stern, Finite-state analysis of SSL 3.0, in: Proc. Seventh USENIX Security Symposium, 1998, pp. 201–216.

25.

L.C.

Paulson, Isabelle, a Generic Theorem Prover, Lecture Notes in Computer Science, Vol. 828, Springer-Verlag, 1994.

26.

Wagner and

Schneier, Analysis of the SSL 3.0 protocol, in: Proc. 2nd USENIX Workshop on Electronic Commerce, 1996, pp. 29–40.