A Novel Symbolic Approach to Verifying Epistemic Properties of Programs

1 Introduction

Epistemic logics capture rich properties such as unlinkability, diagnosability and anonymity [Fagin et al., 1995], and have been applied to complex systems. Several verifiers for temporal-epistemic properties have been developed [Lomuscio et al., 2015; Gammie and van der Meyden, 2004; Kacprzak et al., 2008], and used on a number of applications, ranging from security protocols [Boureanu et al., 2009] and cache-coherence protocols [Baukus and van der Meyden, 2004] to under-water vehicles [Ezekiel et al., 2011].

Typically, verification of epistemic properties in such systems is done by translating the specifications into the input language of a model checker (e.g., [Boureanu et al., 2009]). Thus it is not possible, in general, to verify epistemic properties directly on program code. Also, it is hard to capture richer (e.g., first-order) state specifications, because the base logic of most temporal-epistemic verifiers is propositional.

This is in contrast to program verification. Therein, the full power of temporal logic is foregone (properties only constrain final states, all or some), but programs are expressed in concrete languages, and base logics are very expressive (dealing with integers, reals, arrays, strings etc). In this context, predicate transformers (e.g., strongest postconditions [Dijkstra,

∗Raimondi was supported by EPSRC grant EP/K033921/1; Boureanu was funded by the Marie Skłodowska-Curie grant 661362.

Ioana Boureanu

Department of Computer Science University of Surrey, Guilford, UK i.boureanu@surrey.ac.uk

1976]) are used to reduce verification to first-order queries fed to SMT solvers (e.g., Z3 [De Moura and Bjørner, 2008]).

Inspired by program verification, we propose a methodology for verifying epistemic properties of programs. We focus on S5-like epistemic properties about program states (e.g., "I know that variable x is equal to y + 5"). As in interpreted systems [Fagin et al., 1995], agents can observe certain program variables. Also, the program (its transition relation) is assumed to be known by all agents, similarly to most existing model checkers. We summarise our contributions below.

A New Methodology. We propose a framework whereby a program-epistemic logic of agents can be defined, given userchosen parameters. These parameters include (i) a base logic over program variables; (ii) the programming language; and, (iii) the set of observable program variables for each agent.

Reducing to First-Order. We show that if the strongest postcondition operator is computable for the chosen base logic/programming language, then validity of programepistemic specifications is reducible to validity in first-order fragments (such as QBF and Presburger arithmetic).

Over-approximation. When the strongest postcondition can only be over-approximated (such as in programming languages with unbounded loops), we show that the validity of positive epistemic specifications still reduces to that of firstorder fragments, in a sound but incomplete way.

Case Studies. We instantiate this framework on two case studies: the dining cryptographers problem [Chaum, 1988] and the ThreeBallot protocol [Rivest and Smith, 2007]. We then show how the behaviour of the two systems can be specified using epistemic properties employing propositional logic, and linear integer arithmetic, respectively.

Evaluation. We use off-the-shelf SMT solvers to verify epistemic properties via our reduction to first-order fragments. We experimentally assess the performance of the obtained verifiers, and compare with temporal-epistemic model checkers. We find that our method yields verifiers which can be implemented with minimal effort, whilst remaining competitive for properties in our language with state-of-the-art tools.

Paper Structure. Sec. 2 introduces the syntax and semantics of the proposed framework. Sec. 3 presents the reduction of epistemic to first-order validity. Our case studies and experimental results are detailed in Sec. 4. Finally, we discuss related work in Sec. 5 and conclude in Sec. 6.

2 An Epistemic Logic of Programs

We start from a user-specified base language and build on top of it, up to more expressive logics that specify epistemic properties of programs. We introduce these languages below.

Notation. We denote vectors (x1, . . . , xn) by x and their length by |x| = n. We extend quantifiers over vectors of variables: ∀x. φ means ∀x1. ∀x2. . . . ∀xn. φ. We treat vectors as sets: x ⊆ y means that every element of x appears in y. We write FV (P) for the set of free variables of a formula P .

2.1 Logical Languages: Syntax

Agents & Program Variables. Let A be a finite set of agents. Formulas are over a countable set of variables V. To this end, we fix the following finite sets of variables:

• p ⊆ V is a non-empty set of program variables;
• oA ⊆ p are the variables the agent A ∈ A can observe;
• nA = p\oA are variables agent A ∈ A cannot observe.

Syntax. Let the base language, LQF, be a quantifier-free, first-order language. We leave LQF under-specified to allow various instantiations; we denote formulas of LQF with π.

We now define three languages on top of LQF.

The first-order language, LFO, is the extension of LQF with quantifiers. Its definition is standard,

where x ∈ V and π ∈ LQF. We use the Greek letters φ, ψ to denote formulas given in this first-order language.

The epistemic language language, LK, is the extension of LQF with epistemic modalities KA. The modality KA expresses the knowledge of agent A. Its syntax is as follows:

where π is a base-language formula and A ∈ A is an agent. We use the Greek letter α to denote formulas in LK.

We fix a (possibly infinite) set of commands 1 , C. The program specification language, L□K, extends LK with every formula β = □Cα, meaning "at all final states of C, α holds", where α ∈ LK and C ∈ C is a command.

Finally, we fix L+K as the ¬,⇒-free fragment of LK (note that ¬ and ⇒ over base-language formulas π are allowed, while the dual operator of K, ¬K¬ is not allowed).

2.2 Logic Languages: Semantics

Let D be a set, used as the domain for interpreting variables and quantifiers. A valuation is a total function s : V →D. We lift valuations to tuples of variables and terms (pointwise). Such a valuation is a state. Let U be the set of all states.

We use s[x ↦→ c] to denote the state s′ which agrees with s on all variables except for x, and which also has the property that s′ (x) = c. We extend this notation to vectors of variables/values, i.e., s[x ↦→ c] = s[x1 ↦→ c1] · · · [xn ↦→ cn].

First-order Semantics. Let I be an interpretation of constants, functions and predicates in LQF over the domain D.

1 NB: we use the terms command and program interchangeably, as a program can always be seen as a compound command.

Then, the standard first-order semantics is as follows.

where ◦ is ∧, ∨ or ⇒.

The interpretation JφK of a first-order formula φ is the set of states satisfying it, i.e., JφK = {s ∈ U | s |= φ}.

Epistemic and Program Semantics. For each command C ∈ C, let RC ⊆ U × U be a binary relation over U, representing the transition relation of C. We overload RC as a function from states to sets of states, as well as a function from sets of states to sets of states, as standard.

Definition 2.1. The strongest postcondition operator is a partial function SP(-, -) : LFO × C ⇀ LFO defined as follows.

(here ψ is assumed to be in some canonical form).

Definition 2.2. A function f : LFO × C → LFO is wellbehaved if it is total and computable, and, FV(φ) ⊆ p implies FV (f(φ, C)) ⊆ p for all φ ∈ LFO and C ∈ C.

A function f : LFO × C → LFO over-approximates the strongest postcondition iff it is well-behaved, and, Jf(φ, C)K ⊇ RC(JφK) for all φ ∈ LFO and C ∈ C.

Definition 2.3. Let X ⊆ V. The indistinguishability relation ∼X is a binary relation over U, defined as follows:

Clearly ∼X is an equivalence relation over U, for any X. We now define the interpretation of a program specification β, by defining a ternary satisfaction relation W, s ⊩ β, where W is a set of states and s is a state in W, as follows:

where ◦ is ∧, ∨, or ⇒, and C ∈ C is a command. Intuitively, in a judgement W, s ⊩ β, the set W designates the reachable, or epistemically relevant states, of which s must be a member. Definition 2.4 (Validity of program specifications.). Let φ ∈ LFO and β be a program specification. We write φ ⊩ β to mean that for all s ∈ JφK, we have that JφK, s ⊩ β. We will also, sometimes, write W ⊩ β, where W is a set of states.

Defn. 2.4 sets out the format of our program-epistemic specifications. For instance, φ ⊩ KAπ means that in all states satisfying φ, agent A knows π. Alternatively, φ ⊩ □C¬KAπ means: if command C starts at a state satisfying φ, then in all states where the execution finishes, agent A does not know π.

Lemma 2.5. For any first-order formula φ and epistemic formula α, φ ⊩ □Cα iff RC(JφK) ⊩ α.

Lemma 2.6. Let φ ∈ LFO, s, s′ ∈ U and X, Y ⊆ V. Then,

1. If X ⊆ Y and s ∼Y s′ then s ∼X s′ .
2. If s ∼X s′ and s ∼Y s′ then s ∼X∪Y s′ .
3. If FV(φ) ⊆X and s ∼X s′ , then s |= φ iff s′ |= φ.

3 Reducing to First-Order Validity

In this section, we show that the validity/satisfaction of a formula in L□K reduces to that of a first-order formula. More concretely, the main results of this section (Theorems 3.3 and 3.5) can be understood in the following way: the validity of certain first-order formulas is equivalent to, or implies, the validity of a program specification in the format given by Defn. 2.4. Underpinning this reduction is a translation of epistemic formulas into the first-order language.

Definition 3.1. We define the function τ : LK → LFO by recursion on the structure of epistemic formulas as follows.

The first parameter of τ is a first-order formula representing the set of reachable, or epistemically relevant, states. The translation maps epistemic formulas to (guarded) quantified first-order formulas, exploiting the definition of the indistinguishability relation in terms of state variables.

We first show that satisfaction of α at a state coincides with first-order satisfaction of τ(-, α) at the same state.

Lemma 3.2. For any φ ∈ LFO, state s ∈ JφK and α ∈ LK such that FV (φ) ∪ FV (α) ⊆ p, JφK, s ⊩ α iff s |= τ (φ, α).

Proof. By structural induction on α. The inductive hypothesis is that for all subformulas of α, the result holds.

Cases for π, ¬, ∧, ∨, ⇒: Immediate by the definitions of τ and of the first-order satisfaction relation.

Case for KAα: We need to show JφK, s ⊩ KAα iff s |= ∀nA. (φ ⇒ τ (φ, α)).

Direction ⇒: Suppose s ̸|= ∀nA. (φ⇒ τ(φ, α)). Thus, there exists c ∈ D|nA| such that s[nA ↦→ c] |= φ ∧ ¬τ(φ, α). Expanding s[-], there is a state s′ such that for all x ∈ V\nA, s(x) = s′ (x), and s′ |= φ ∧ ¬τ(φ, α). By Defn. 2.3, we first obtain that s ∼V\nA s′ , which then implies s ∼oA s′ by item (1) of Lem. 2.6. Also, s′ |= φ and s′ ̸|= τ(φ, α), which means that JφK, s′ ̸⊩ α, by the inductive hypothesis. Therefore, there exists a state s′ |= φ such that s ∼oA s′ and s′ ̸|= τ(φ, α). Thus, JφK, s ̸⊩ KAα, completing the proof.

Direction ⇐: Assume s |= ∀nA. (φ ⇒ τ(φ, α)) but JφK, s ̸⊩ KAα. The former implies that: for all value tuples c ∈ D|nA| , we have s[nA ↦→ c] |= φ ⇒ τ(φ, α). Expanding s[-], we get that if for all x ∈ V \nA, s(x) = s′ (x), then s′ |= φ ⇒ τ(φ, α). Using Defn. 2.3, we conclude that for all states s′ , if s ∼V\nA s′ then s′ |= φ⇒ τ(φ, α).

The second assumption implies that there exists a state s0 ∈ JφK such that s ∼oA s0 and JφK, s0 ̸⊩ α. By the inductive hypothesis, this means s0 ̸|= τ(φ, α). So, s ∼oA s0 and s0 |= φ ∧ ¬τ(φ, α). Define a new state s1 = s[p ↦→ s0(p)]. But, if FV(φ) ∪FV(α) ⊆ p, then FV(τ(φ, α)) ⊆ p (by simple induction). Thus, since s1 ∼p s0 by construction, item (3) of Lem. 2.6 gives us that s1 |= φ ∧ ¬τ(φ, α).

Also, since oA ⊆ p and s1 ∼p s0, it follows from item (1) of Lem. 2.6 that s1 ∼oA s0. By the transitivity of ∼oA and the fact that s ∼oA s0 we have that s ∼oA s1. Also, by construction, s ∼V\p s1, and given that (V \ p) ∪ oA = V \ nA, we obtain s ∼V\nA s1 by item (2) of Lem. 2.6. This, along with the fact that s1 |= φ ∧ ¬τ (φ, α), directly contradicts that for all states s′ , if s ∼V\nA s′ then s′ |= φ⇒ τ(φ, α).

We can now state the first main result: when SP(-,-) is well-behaved, validity of program specifications coincides with that of first-order formulas produced by the τ function.

Theorem 3.3. Let φ ∈ LFO and α ∈ LK be formulas such that FV (φ) ∪ FV (α) ⊆ p. If SP is well-behaved, then

Proof. Assume the left-hand side. By Lem. 2.5 this is equivalent to RC(JφK) ⊩ α. By the semantics and Defn. 2.1, this is equivalent to claiming that for all s, if s |= SP(φ,C), then SP(φ,C), s ⊩ α. By Lem. 3.2, for all s, if s |= SP(φ,C), then s |= τ(SP(φ, C), α), completing the proof.

The strongest postcondition operator is often not wellbehaved, e.g., when the transition relation R is generated by programs containing unbounded loops over infinite domains. Our second main result states that when positive epistemic formulas are involved (L+K ), and it is possible to compute an over-approximation of SP(-,-), then validity of the translated formulas implies validity of the program specification. This mirrors the situation in program analysis, where undecidability often leads to sound but incomplete analyses.

We start with a technical lemma and lift it up to validity.

Lemma 3.4. Let φ ∈ LFO and α ∈ L+K be formulas such that FV (φ) ∪ FV (α) ⊆ p. Then, for any set of states W ⊆ JφK and any state s ∈ W, if JφK, s ⊩ α then W, s ⊩ α.

Proof. By structural induction on α. The only interesting case is the epistemic one, that is, if JφK, s ⊩ KAα then W, s ⊩ KAα. Suppose the former. Then, for any state s′ ∈ JφK such that s ∼oA s′ , it is the case that JφK, s′ ⊩ α. But, since W ⊆ JφK, we can restrict attention to states in W, i.e., for any state s′ ∈ W such that s ∼oA s′ , it is the case that JφK, s′ ⊩ α. Now we can apply the inductive hypothesis on s′ and obtain that for any state s′ ∈ W such that s ∼oA s′ , W, s′ ⊩ α holds, which completes the proof.

Theorem 3.5. Suppose f : LFO × C → LFO overapproximates the strongest postcondition. If φ ∈ LFO and α ∈ L+K are formulas such that FV (φ) ∪ FV (α) ⊆ p, then

Proof. Assume f(φ,C) |= τ(f(φ,C), α). By Lem. 3.2, this means that f(φ,C) ⊩ α, or (Defn. 2.4), that for all states s |= f(φ, C), it is the case that Jf(φ, C)K, s ⊩ α. By assumption, RC(JφK) ⊆ Jf(φ,C)K. Therefore we can soundly restrict the relevant set of states, obtaining that for all states s ∈ RC(JφK), it is the case that Jf(φ,C)K, s ⊩ α. By Lem. 3.4, for all s, if s ∈ RC(JφK), then RC(JφK), s ⊩ α. This is equivalent to φ ⊩ □Cα, thus completing the proof.

Remark 3.6. Without fixing the various framework parameters, it is hard to determine the decidability and complexity of program specifications. Some observations are possible:

First, the length of τ(φ, α) is linear in ‖φ‖ + ‖α‖, where ‖φ‖ is the number of symbols in φ, defined as usual.

Second, the number of quantifier alternations in τ(φ, α) (in negation-normal form) is bounded by the quantifier alternations in φ plus the number of alternations of ¬ and K in α.

3.1 A Simple Programming Language

We informally present a simple, loop-free imperative programming language, and how it can be used to interpret execution modalities □C and SP(-,-). In the (infinite) set of commands C we include assignments, conditionals and sequencing. We omit unbounded loops in order to guarantee that the strongest postcondition is well-behaved. We do not fix the types of variables, to allow different user choices for domains. In Sections 4.1 and 4.2 we show how we can use this language with Booleans and integers. Below we show the syntax of commands and the rules for computing SP(-, -).

Above, x is a program variable and y is a fresh logical variable. The transition relations RC are defined as usual.

Remark 3.7. The SP(-,-) operator for the above programming language is well-behaved (cf. Defn. 2.2) for any choice of other framework parameters (domain, program variables, base language etc). In addition, we can make the following observations that we use in Sections 4.1 and 4.2:

• SP(-, -) may only introduce existential quantifiers.
• If x /∈ FV (φ), then SP(φ, x := e) = (φ ∧ x = e). That is, if x is unrestricted, no quantifiers are introduced.
• For a fixed C, the size of SP(φ, C) is polynomial in ‖φ‖.

4 Evaluation

We now present two case studies, where we instantiate the framework presented in Sec. 2, mechanise the verification of relevant epistemic properties by using appropriate tools such as SMT solvers, and assess verification performance.

All the experiments 2 have been performed on a 4-core 2.4 GHz Intel Core i7 MacBook Pro with 16 GB of RAM running OS X 10.11.6. The version of MCMAS is 1.2.2 and Z3 is 4.5.1; both tools have been compiled from source on the target machine.

4.1 Dining Cryptographers

Problem description. This is a scenario where n agents (cryptographers) dine at a round table [Chaum, 1988]. The dinner may have been paid by their employer (the NSA), or by one of the agents. They execute a protocol to reveal whether one of the agents paid, but without revealing which one. The protocol supplies each pair of adjacent agents with a random coin, which can be observed only by that pair. Each agent announces the result of XORing three Booleans: the two coins observable by her and the status of whether she paid for the dinner. The XOR of all announcements is proven to be equal to the disjunction of whether any agent paid.

This protocol has been used as an evaluation case study for several methods of verifying epistemic properties of programs [Kacprzak et al., 2006; 2008; Lomuscio et al., 2015].

2 Our code is released open-source at goo.gl/so8bQc.

Framework Instantiation. The domain is D = {⊤,⊥}. The base language LQF is propositional logic. The set of agents is A = {0, . . . , n - 1}. The program variables are p = {x} ∪ {pi, ci | 0 ≤ i < n}; x is the XOR of announcements; pi encodes whether agent i has paid; and, ci encodes the coin shared between agents i - 1 and i. Observable variables for agent i ∈ A are oi = {x, pi, ci, ci+1 mod n}, and ni = p \ oi. We model the protocol by an assignment C:

The language LFO is that of QBFs. As seen in Sec. 3.1, SP(φ, C) is well-behaved. Validity of program specifications is in ΣPj or ΠPj [Stockmeyer, 1977], where j is the sum of quantifier alternations in φ and alternations of ¬ and K in α.

The initial states, I, are those where at most one agent paid. Thus, we can compute the strongest postcondition:

Experiments. We list the specifications we verify. Formula α1 = ¬p0 ⇒ ((K0 ∧n-1 i=0 ¬pi) ∨ (∧n-1 i=1 ¬K0pi)) states that if agent 0 has not paid then she knows that no agent paid, or (in case an agent paid) she does not know which one. Formula α2 = K0 (x ⇔ ∨n-1 i=0 pi) states that agent 0 knows that x is true iff one of the agents paid. Formula α3 = K0p1 states that agent 0 knows that agent 1 has paid; this is false, but we include this to assess performance on negative instances too.

To verify I ⊩ □Cα1, I ⊩ □Cα2 and I ̸⊩ □Cα3 we construct the QBF formula SP(I,C) ∧ ¬τ(SP(I,C), αi), feed it to Z3, and test for unsatisfiability, as per Theorem 3.3.

Experimental results for the verification of these formulae are reported in Fig. 1. As computing the reachable-states space is a dominant factor for MCMAS, its performance does not vary significantly across specifications α1, α2, α3. Thus, for clarity of exposition, we omit the MCMAS curves on specifications α2, α3. We observe that (i) MCMAS is faster, or equally fast, for n ≤ 7, but slower for all n > 7; (ii) there are cases where our method is faster than MCMAS by a factor of ≥ 100 (e.g., when n = 32) when checking α1 (which is the computationally most expensive in our case), whilst when verifying α3 our speed-up is several orders of magnitudes higher.

4.2 ThreeBallot Voting Protocol

Problem description. In the ThreeBallot voting protocol [Rivest and Smith, 2007], a voter is given a multi-ballot formed of three atomic ballots. All atomic ballots are identical and show all candidates in the same fixed order. To vote for a candidate, a voter ticks the name of the candidate on exactly two atomic ballots. To vote against a candidate, a voter ticks the name of the candidate on exactly one atomic ballot. The voting system posts all the atomic ballots cast, randomly ordered, on a public bulletin board. The number of votes for the j-th candidate is the number of atomic ballots with the j-th position marked minus the total number of voters. Several voting requirements exist: (universal) verifiability, coercion-resistance, vote-privacy, etc. Vote-privacy broadly means that no observer in a voting protocol can know how some voter (other than themselves) voted. Here we only consider vote-privacy, and only in the absence of active adversaries. As such, the presentation above and our modelling are restricted to aspects of the ThreeBallot protocol relevant to this task, leaving aside several sub-parts of the system (e.g., scanning machines, identifiers on atomic bulletins, etc). We also leave out properties that are not yet expressible in our formalism, such as common-knowledge properties.

Framework Instantiation. We assume m ≥ 2 candidates and n ≥ 2 voters. The domain is D = N. The base language LQF is linear integer arithmetic. The set of agents is A = {1, . . . , n, P}, where P is a 'public observer' agent (surveying all public aspects). The program variables are p = ⋃mj=1 {cj} ∪ ⋃ni=1 ⋃mj=1 ⋃3k=1 {bijk}. Variable cj stores the total number of atomic-ballot ticks for candidate j. Variable bijk (with values in {0, 1}) represents whether or not voter i ticked next to candidate j on the k-th atomic ballot.

For an agent i ∈ A \ {P}, the observable variables are oi = ⋃mj=1 {cj} ∪ ⋃mj=1 ⋃3k=1 {bijk}, i.e., voter i can observe the totals for each candidate, as well as her own vote. For agent P, the observable variables are oP = ⋃mj=1 {cj}. That is, P only observes the totals for each candidate. For every agent i ∈ A, the non-observable variables are ni = p \ oi.

To model vote-counting, we first introduce the macro Si,j ≡ ∑3k=1 bijk, denoting the number of ticks voter i has entered for candidate j. Then, the programC is:

The language LFO is Presburger arithmetic. For any φ ∈ LFO, SP(φ,C) is well-behaved (Sec. 3.1). Program specification validity is in ΣEXP ℓ or ΠEXP ℓ (classes of the weak exponential hierarchy [Haase, 2014]), where ℓ + 1 is the sum of quantifier alternations in φ and alternations of ¬ and K in α.

Fig. 2b depicts a number of macros which we use in composing the program specifications verified. Macro B bounds the possible values of the entries on atomic ballots to 0 or 1,

• (b) Macros used in the Three-Ballot system.

Figure 2: Experimental evaluation of case studies.

i.e., no tick or a tick. Macro Vi,j (resp. ¯ Vi,j) states that voter i voted for (resp. against) candidate j, i.e., two ticks vs one tick. Macro CV ≥0 i states that voter i voted for at least one candidate and CV ≤1 i states that voter i voted for at most one candidate. Macro CV states that all voters voted correctly. Macro NU states that the vote is not unanimous, as every candidate received at least one vote; we will require non-unanimity to avoid trivial vote-privacy breaches. Macro NUmod i is a variation on NU, and states that every candidate received at least one vote from voters other than a designated voter i; we will require this non-unanimity condition for asserting voterprivacy relative to a voter agent. Accordingly, Fig. 2b shows the two possible initial conditions, I and Imod i.

Experiments. The formula α1 = ¬KPV1,1 states that the public observer does not know that voter 1 voted for candidate 1. The formula α2 = ¬K1V2,1 states that voter 1 does not know that voter 2 voted for candidate 1. We verify the following scenarios: (a) I ⊩ □Cα1; (b) Imod 1 ⊩ □Cα2; and, (c) I ̸⊩ □Cα2. We construct the relevant Presburger formulas obtained by Theorem 3.3, and issue the queries to Z3.

We make the following observations. With a timeout of roughly 1h, for m = 2 candidates, we can verify all formulas for up to n = 22 voters. For m = 3, we can check the specifications up to n = 15. For m = 5, we stop at n = 11. Runtime is evidently exponential in both n and m. Increasing m rather than n has a more pronounced impact on verification runtime; this is apparent on the graphs, as different formulas for the same m value cluster together. Finally, disproof (i.e., α3) seems to be more tractable when m = 2.

5 RelatedWork

Several model checkers exist for model verification against properties expressed in temporal-epistemic logics [Lomuscio et al., 2015; Gammie and van der Meyden, 2004; Kacprzak et al., 2008]. Their underlying techniques include binary decision diagrams, automata, and bounded model checking using SAT solvers. Abstraction and parametrisation have also been introduced in some of these tools, to tackle infinitestate systems [Belardinelli et al., 2016; Kouvaros and Lomuscio, 2016]. A fix-point technique for verifying bounds on resources in multi-agent systems using SMT solvers is described in [Zbrzezny et al., 2016]. As per Section 4, we generally outperform significantly MCMAS [Lomuscio et al., 2015], a state-of-the-art tool in this domain.

Verification of epistemic properties in (possibly) infinite state systems is also addressed in [Cimatti et al., 2016]. The authors employ a counter-example guided abstraction refinement loop to translate a class of temporal-epistemic properties to LTL properties, and to generate a satisfiability problem for an infinite-state model checker. Beside the core technique, the key differences between [Cimatti et al., 2016] and our approach are three-fold. (1) Our input is a program in a general-purpose language rather than the model of a system. (2) We can handle nested epistemic operators (but our temporal expressivity is limited to the final states of programs). (3) Our approach performs better on the epistemic properties of the dining cryptographers that can be expressed both by our framework and by [Cimatti et al., 2016]: for the formula p0 ⇒ K0(¬ ∨n-1 i=1 pi), the authors report running times of 287, 598 and 765 seconds for 280, 360 and 400 cryptographers, respectively; in all cases, this formula is checked in less than 1 second in our framework.

Verification of programs against properties expressed in (temporal-)epistemic logics is a less explored area of research compared to model-based verification. Going back some decades, the verification of epistemic properties for a LISP-like language called REX was investigated in [Rosenschein and Kaelbling, 1986]; the authors employed a variant of LTL+K and presented a calculus to prove logical consequences of a REX program. On a slightly different path, [Gelfond, 1994; Zhang, 2006] addressed the theoretical problem of extending (declarative) programming languages with epistemic operators. More recently, the approach described in [Balliu et al., 2012] verifies whether Java programs respect non-interference properties (modulo declassification), given as epistemic formulae. The authors employ a version of the model checker JPF [P˘as˘areanu and Rungta, 2010] to generate the state space of a Java program and then either MCMAS or Z3 to verify a symbolic representation of the reachable state-space. The key differences between [Balliu et al., 2012] and our approach stem from their focus on non-interference properties and the need of a concolic execution engine. Finally, dynamic epistemic logic [Plaza, 2007] lends itself to the expression of epistemic properties of programs; preliminary work on a verification tool in this space is described in [Wang, 2016].

6 Conclusions

In this paper, we proposed a new approach to verifying epistemic properties of programs. We showed how this method can be applied to arbitrary logics and programming languages. We use program-epistemic specifications, expressing the requirement that the given epistemic properties hold on all final states of the program. We showed how programepistemic specifications can be reduced to appropriate queries to tools such as SMT solvers. We instantiated our approach in two case studies, the Dining Cryptographers problem and the ThreeBallot voting protocol, and experimentally evaluated verification performance.

For any given instantiation of our framework, the translation of program-epistemic properties into first-order sentences can be automated with great ease. In addition, we expect that advances in SMT technology will directly translate into performance gains for tools based on our methodology.

Our approach is not, of course, without limitations. We traded off temporal expressivity, to deal with arbitrary programming languages. Thus we cannot directly encode properties utilising, e.g., until operators or other complex temporal properties. This is a research direction we plan to pursue, drawing inspiration from attempts to lift infinite-state program verification to the verification of true temporal properties [Cook et al., 2012].

Common-knowledge properties are outside the current reach of our approach. We plan to investigate an extension of our framework that can deal with common knowledge, possibly by viewing it as a fixpoint and using cyclic proof to discharge its instances [Brotherston et al., 2012].

Another limitation is the restriction to positive epistemic properties (L+K ) when the strongest postcondition is not wellbehaved (cf. Theorem 3.5). To lift this limitation, we believe that static analysis methods such as abstract interpretation [Cousot and Cousot, 1977] can be fruitfully employed here, especially when over- and under-approximating analyses are combined. We plan to follow this thread in future work.

Another avenue of future work is a twofold extension of the work in [Armando et al., 2014] which, one, focused on SAT solvers and, two, analysed only trace-based properties of systems. To this end, we will look into embedding different security semantics into our methodology and thus move towards the verification of privacy and anonymity properties of programs with a security bearing (e.g., reference implementations of cryptographically rich e-voting protocols).