Showing invariance compositionally for a process algebra for network protocols

Timothy Bourke^{1,2}, Robert J. van Glabbeek^{3,4}, and Peter Höfner^{3,4}

1 Inria Paris-Rocquencourt 2 Ecole normale supérieure, Paris, France 3 NICTA, Sydney, Australia 4 Computer Science and Engineering, UNSW, Sydney, Australia

Abstract. This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, such as nodes in a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). To this end, we propose a novel compositional technique for lifting global invariants stated at the level of individual nodes to networks of nodes.

1 Introduction and related work

The Algebra for Wireless Networks (AWN) is a process algebra developed for modelling and analysing protocols for Mobile Ad hoc Networks (MANETs) and Wireless Mesh Networks (WMNs) [6, §4]. This paper reports on both its mechanization in Isabelle/HOL [15] and the development of a compositional framework for showing invariant properties of models.^{1} The techniques we describe are a response to problems encountered during the mechanization of a model and proof—presented elsewhere [4]—of an RFC-standard for routing protocols. Despite the existence of extensive research on related problems [18] and several mechanized frameworks for reactive systems [5,10,14], we are not aware of other solutions that allow the compositional statement and proof of properties relating the states of different nodes in a message-passing model—at least not within the strictures imposed by an Interactive Theorem Prover (ITP).

But is there really any need for yet another process algebra and associated framework? AWN provides a unique mix of communication primitives and a treatment of data structures that are essential for studying MANET and WMN protocols with dynamic topologies and sophisticated routing logic [6, §1]. It supports communication primitives for one-to-one (unicast), one-to-many (groupcast), and one-to-all (broadcast) message passing. AWN comprises distinct layers

1 The Isabelle/HOL source files can be found in the Archive of Formal Proofs [3].

for expressing the structure of nodes and networks. We exploit this structure, but we also expect the techniques proposed in Sections 3 and 4 to apply to similar layered modelling languages. Besides this, our work differs from other mechanizations for verifying reactive systems, like UNITY [10], TLA^{+} [5], or I/O Automata [14] (from which we drew the most inspiration), in its explicit treatment of control states, in the form of process algebra terms, as distinct from data states. In this respect, our approach is close to that of Isabelle/Circus [7], but it differs in (1) the treatment of operators for composing nodes, which we model directly as functions on automata, (2) the treatment of recursive invocations, which we do not permit, and (3) our inclusion of a framework for compositional proofs. Other work in ITPs focuses on showing traditional properties of process algebras, like, for instance, the treatment of binders [1], that bisimulation equivalence is a congruence [9,11], or properties of fix-point induction [20], while we focus on what has been termed ‘proof methodology’ [8], and develop a compositional method for showing correctness properties of protocols specified in a process algebra. Alternatively, Paulson’s inductive approach [16] can be applied to show properties of protocols specified with less generic infrastructure. But we think it to be better suited to systems specified in a ‘declarative’ style as opposed to the strongly operational models we consider.

Structure and contributions. Section 2 describes the mechanization of AWN. The basic definitions are routine but the layered structure of the language and the treatment of operators on networks as functions on automata are relatively novel and essential to understanding later sections. Section 3 describes our mechanization of the theory of inductive invariants, closely following [13]. We exploit the structure of AWN to generate verification conditions corresponding to those of pen-and-paper proofs [6, §7]. Section 4 presents a compositional technique for stating and proving invariants that relate states across multiple nodes. Basically, we substitute ‘open’ Structural Operational Semantics (SOS) rules over the global state for the standard rules over local states (Section 4.1), show the property over a single sequential process (Section 4.2), ‘lift’ it successively over layers that model message queueing and network communication (Section 4.3), and, ultimately, ‘transfer’ it to the original model (Section 4.4).

2 The process algebra AWN

AWN comprises five layers [6, §4]. We treat each layer as an automaton with states of a specific form and a given set of transition rules. We describe the layers from the bottom up over the following sections.

2.1 Sequential processes

Sequential processes are used to encode protocol logic. Each is modelled by a (recursive) specification Γ of type ’p ⇒ (’s, ’p, ’l) seqp, which maps process names of type ’p to terms of type (’s, ’p, ’l) seqp, also parameterized by ’s, data states, and ’l, labels. States of sequential processes have the form (ξ, p) where ξ is a data state of type ’s and p is a control term of type (’s, ’p, ’l) seqp.

{l}[[u]] p  ’l ⇒ (’s ⇒ ’s) ⇒ (’s, ’p, ’l) seqp ⇒ (’s, ’p, ’l) seqp
{l}⟨g⟩ p  ’l ⇒ (’s ⇒ ’s set) ⇒ (’s, ’p, ’l) seqp ⇒ (’s, ’p, ’l) seqp
{l}unicast(s_{ip}, s_{msg}) . p ▷ q ’l ⇒ (’s ⇒ ip) ⇒ (’s ⇒ msg) ⇒ (’s, ’p, ’l) seqp ⇒

(’s, ’p, ’l) seqp ⇒ (’s, ’p, ’l) seqp

{l}broadcast(s_{msg}) . p  ’l ⇒ (’s ⇒ msg) ⇒ (’s, ’p, ’l) seqp ⇒ (’s, ’p, ’l) seqp
{l}groupcast(s_{ips}, s_{msg}) . p ’l ⇒ (’s ⇒ ip set) ⇒ (’s ⇒ msg) ⇒ (’s, ’p, ’l) seqp ⇒

(’s, ’p, ’l) seqp

{l}send(s_{msg}) . p  ’l ⇒ (’s ⇒ msg) ⇒ (’s, ’p, ’l) seqp ⇒ (’s, ’p, ’l) seqp
{l}receive(u_{msg}) . p  ’l ⇒ (msg ⇒ ’s ⇒ ’s) ⇒ (’s, ’p, ’l) seqp ⇒ (’s, ’p, ’l) seqp
{l}deliver(s_{data}) . p  ’l ⇒ (’s ⇒ data) ⇒ (’s, ’p, ’l) seqp ⇒ (’s, ’p, ’l) seqp
p_{1} ⊕ p_{2}  (’s, ’p, ’l) seqp ⇒ (’s, ’p, ’l) seqp ⇒ (’s, ’p, ’l) seqp
call(pn)  ’p ⇒ (’s, ’p, ’l) seqp

(a) Term constructors for (’s, ’p, ’l) seqp.

\frac{ξ’ = u ξ}{((ξ, \{l\}[[u]] p), τ, (ξ’, p)) ∈ seqp-sos Γ}  \frac{((ξ, p), a, (ξ’, p’)) ∈ seqp-sos Γ}{((ξ, p ⊕ q), a, (ξ’, p’)) ∈ seqp-sos Γ}

\frac{((ξ, Γ pn), a, (ξ’, p’)) ∈ seqp-sos Γ}{((ξ, call(pn)), a, (ξ’, p’)) ∈ seqp-sos Γ}  \frac{((ξ, q), a, (ξ’, q’)) ∈ seqp-sos Γ}{((ξ, p ⊕ q), a, (ξ’, q’)) ∈ seqp-sos Γ}
((ξ, {l}unicast(s_{ip}, s_{msg}) . p ▷ q), unicast (s_{ip} ξ) (s_{msg} ξ), (ξ, p)) ∈ seqp-sos Γ

((ξ, {l}unicast(s_{ip}, s_{msg}) . p ▷ q), ¬unicast (s_{ip} ξ), (ξ, q)) ∈ seqp-sos Γ

(b) SOS rules for sequential processes: examples from seqp-sos.

Fig. 1: Sequential processes: terms and semantics

Process terms are built from the constructors that are shown with their types^{2} in Figure 1a. The inductive set seqp-sos, shown partially in Figure 1b, contains one or two SOS rules for each constructor. It is parameterized by a specification Γ and relates triples of source states, actions, and destination states.

The ‘prefix’ constructors are each labelled with an {l}. Labels are used to strengthen invariants when a property is only true in or between certain states; they have no influence on control flow (unlike in [13]). The prefix constructors are assignment, {l}[[u]] p, which transforms the data state deterministically according to the function u and performs a τ action, as shown in Figure 1b; guard/bind, {l}⟨g⟩ p, with which we encode both guards, ⟨λξ. if g ξ then {ξ} else ∅⟩ p, and variable bindings, as in ⟨λξ. {ξ(|no := n|) | n < 5}⟩ p;^{3} network synchronizations, receive/unicast/broadcast/groupcast, of which the rules for unicast are characteristic and shown in Figure 1b—the environment decides between a successful unicast i m and an unsuccessful ¬unicast i; and, internal communications, send/receive/deliver.

The other constructors are unlabelled and serve to ‘glue’ processes together: choice, p_{1} ⊕ p_{2}, takes the union of two transition sets; and, call, call(pn), affixes a term from the specification (Γ pn). The rules for both are shown in Figure 1b.

2 Leading abstractions are omitted, for example, λl fa p. {l}[[u]] p is written {l}[[u]] p. 3 Although it strictly subsumes assignment we prefer to keep both.

We introduce the specification of a simple ‘toy’ protocol as a running example:

Γ_{Toy} PToy = labelled PToy (

receive(λmsg’ ξ. ξ (| msg := msg’ |)).  ^{{PToy-:0}}
[[λξ. ξ (|nhip := ip ξ|)]]  ^{{PToy-:1}}
( ⟨is-newpkt⟩  ^{{PToy-:2}}
[[λξ. ξ (|no := max (no ξ) (num ξ)|)]]  ^{{PToy-:3}}
broadcast(λξ. pkt(no ξ, ip ξ)). Toy()  ^{{PToy-:4,5}}
⊕ ⟨is-pkt⟩  ^{{PToy-:2}}
( ⟨λξ. if num ξ ≥ no ξ then {ξ} else {}⟩ ^{{PToy-:6}}
[[λξ. ξ (|no := num ξ|)]]  ^{{PToy-:7}}
[[λξ. ξ (|nhip := sip ξ|)]]  ^{{PToy-:8}}
broadcast(λξ. pkt(no ξ, ip ξ)). Toy() ^{{PToy-:9,10}}
⊕ ⟨λξ. if num ξ < no ξ then {ξ} else {}⟩ ^{{PToy-:6}}
Toy()))) ,  ^{{PToy-:11}}

where PToy is the process name, is-newpkt and is-pkt are guards that unpack the contents of msg, and Toy() is an abbreviation that clears some variables before a call(PToy). The function labelled associates its argument PToy paired with a number to every prefix constructor. There are two types of messages: newpkt

(data, dst), from which is-newpkt copies data to the variable num, and pkt (data,

src), from which is-pkt copies data into num and src into sip.

The corresponding sequential model is an automaton—a record^{4} of two fields: a set of initial states and a set of transitions—parameterized by an address i:

ptoy i = (|init = {(toy-init i, Γ_{Toy} PToy)}, trans = seqp-sos Γ_{Toy}|),

where toy-init i yields the initial data state (|ip = i, no = 0, nhip = i, msg = SOME x. True, num = SOME x. True, sip = SOME x. True|). The last three variables are

initialized to arbitrary values, as they are considered local—they are explicitly reinitialized before each call(PToy). This is the biggest departure from the original definition of AWN; it simplifies the treatment of call, as we show in Section 3.1, and facilitates working with automata where variable locality makes little sense.

2.2 Local parallel composition

Message sending protocols must nearly always be input-enabled, that is, nodes should always be in a state where they can receive messages. To achieve this, and to model asynchronous message transmission, the protocol process is combined with a queue model, qmsg, that continually appends received messages onto an

Fig. 2: SOS rules for parallel processes: parp-sos.

\frac{(s, a, s’) ∈ S ⋀m. a ≠ receive m}{((s, t), a, (s’, t)) ∈ parp-sos S T}  \frac{(t, a, t’) ∈ T ⋀m. a ≠ send m}{((s, t), a, (s, t’)) ∈ parp-sos S T}

\frac{(s, receive m, s’) ∈ S (t, send m, t’) ∈ T}{((s, t), τ, (s’, t’)) ∈ parp-sos S T} 4 The generic record has type (’s, ’a) automaton, where the type ’s is the domain of

states, here pairs of data records and control terms, and ’a is the domain of actions.

\frac{(s, groupcast D m, s’) ∈ S}{(s_{R}^{i}, (R ∩ D):*cast(m), s’_{R}^{i}) ∈ node-sos S}  \frac{(s, receive m, s’) ∈ S}{(s_{R}^{i}, \{i\}¬∅:arrive(m), s’_{R}^{i}) ∈ node-sos S}
(s_{R}^{i}, ∅¬{i}:arrive(m), s_{R}^{i}) ∈ node-sos S  (s_{R}^{i}, connect(i, i’), s_{R ∪ {i’}}^{i} ) ∈ node-sos S

Fig. 3: SOS rules for nodes: examples from node-sos.

internal list and offers to send the head message to the protocol process: ptoy i ⟨⟨ qmsg. The local parallel operator is a function over automata:

s ⟨⟨ t = (|init = init s × init t, trans = parp-sos (trans s) (trans t)|).

The rules for parp-sos are shown in Figure 2.

2.3 Nodes

At the node level, a local process np is wrapped in a layer that records its address i and tracks the set of neighbouring node addresses, initially R_{i}:

⟨i : np : R_{i}⟩ = (|init = {s_{R_{i}}^{i} | s ∈ init np}, trans = node-sos (trans np)|).

Node states are denoted s_{R}^{i}. Figure 3 presents rules typical of node-sos. Output network synchronizations, like groupcast, are filtered by the list of neighbours to become *cast actions. The H¬K:arrive(m) action—in Figure 3 instantiated as ∅¬{i}:arrive(m), and {i}¬∅:arrive(m)—is used to model a message m received by nodes in H and not by those in K. The connect(i, i’) adds node i’ to the set of neighbours of node i; disconnect(i, i’) works similarly.

2.4 Partial networks

Partial networks are specified as values of type net-tree, that is, as a node ⟨i; R_{i}⟩ with address i and a set of initial neighbours R_{i}, or a composition of two net-trees p_{1} ^{∥} p_{2}. The function pnet maps such a value, together with the process np i to execute at each node i, here parameterized by an address, to an automaton:

pnet np ⟨i; R_{i}⟩ = ⟨i : np i : R_{i}⟩
pnet np (p_{1} ^{∥} p_{2}) = (|init = {s_{1}∥ s_{2} | s_{1} ∈ init (pnet np p_{1}) ∧ s_{2} ∈ init (pnet np p_{2})},

trans = pnet-sos (trans (pnet np p_{1})) (trans (pnet np p_{2}))|),

The states of such automata mirror the tree structure of the network term; we denote composed states s_{1}∥ s_{2}. This structure, and the node addresses, remain constant during an execution. These definitions suffice to model an example three node network of toy processes:

pnet (λi. ptoy i ⟨⟨ qmsg) (⟨A; {B}⟩^{∥} ⟨B; {A, C}⟩^{∥} ⟨C; {B}⟩).

Figure 4 presents rules typical of pnet-sos. There are rules where only one node acts, like the one shown for τ, and rules where all nodes act, like those for *cast and arrive. The latter ensure—since qmsg is always ready to receive m—that a partial network can always perform an H¬K:arrive(m) for any combination of H and K consistent with its node addresses, but that pairing with an R:*cast(m) restricts the possibilities to the one consistent with the destinations in R.

\frac{(s, R:*cast(m), s’) ∈ S (t, H¬K:arrive(m), t’) ∈ T H ⊆ R K ∩ R = ∅}{(s ∥ t, R:*cast(m), s’∥ t’) ∈ pnet-sos S T}

\frac{(s, H¬K:arrive(m), s’) ∈ S (t, H’¬K’:arrive(m), t’) ∈ T}{(s ∥ t, (H ∪ H’)¬(K ∪ K’):arrive(m), s’∥ t’) ∈ pnet-sos S T} \frac{(s, τ, s’) ∈ S}{(s ∥ t, τ, s’∥ t) ∈ pnet-sos S T}

Fig. 4: SOS rules for partial networks: examples from pnet-sos.

2.5 Complete networks

The last layer closes a network to further interactions with an environment; the *cast action becomes a τ and H¬K:arrive(m) is forbidden:

closed A = A(|trans := cnet-sos (trans A)|).

The rules for cnet-sos are straight-forward and not presented here.

3 Basic invariance

This paper only considers proofs of invariance, that is, properties of reachable states. The basic definitions are classic [14, Part III].

Definition 1 (reachability). Given an automaton A and an assumption I over actions, reachable A I is the smallest set defined by the rules:

s ∈ init A

s ∈ reachable A I

s ∈ reachable A I (s, a, s’) ∈ trans A I a

s’ ∈ reachable A I

Definition 2 (invariance). Given an automaton A and an assumption I, a predicate P is invariant, denoted A |⊧ (I →) P, iff ∀ s ∈ reachable A I. P s.

We state reachability relative to an assumption on (input) actions I. When I is λ-. True, we write simply A |⊧ P.

Definition 3 (step invariance). Given an automaton A and an assumption I, a predicate P is step invariant, denoted A ||≡ (I →) P, iff

∀ a. I a ⟶ (∀ s ∈ reachable A I. ∀ s’. (s, a, s’) ∈ trans A ⟶ P (s, a, s’)).

Our invariance proofs follow the compositional strategy recommended in [18, §1.6.2]. That is, we show properties of sequential process automata using the induction principle of Definition 1, and then apply generic proof rules to successively lift such properties over each of the other layers. The inductive assertion method, as stated in rule inv-b of [13], requires a finite set of transition schemas, which, together with the obligation on initial states yields a set of sufficient verification conditions. We develop this set in Section 3.1 and use it to derive the main proof rule presented in Section 3.2 together with some examples.

3.1 Control terms

Given a specification Γ over finitely many process names, we can generate a finite set of verification conditions because transitions from (’s, ’p, ’l) seqp terms always yield subterms of terms in Γ. But, rather than simply consider the set of all subterms, we prefer to define a subset of ‘control terms’ that reduces the number of verification conditions, avoids tedious duplication in proofs, and corresponds with the obligations considered in pen-and-paper proofs. The main idea is that the ⊕ and call operators serve only to combine process terms: they are, in a sense, executed recursively by seqp-sos to determine the actions that a term offers to its environment. This is made precise by defining a relation between sequential process terms.

Definition 4 (⇝_{Γ}). For a (recursive) specification Γ, let ⇝_{Γ} be the smallest

relation such that (p_{1} ⊕ p_{2}) ⇝_{Γ} p_{1}, (p_{1} ⊕ p_{2}) ⇝_{Γ} p_{2}, and (call(pn)) ⇝_{Γ} Γ pn.

We write ⇝_{Γ} ^{∗} for its reflexive transitive closure. We consider a specification to be well formed, when the inverse of this relation is well founded:

wellformed Γ = wf {(q, p) | p ⇝_{Γ} q}.

Most of our lemmas only apply to well formed specifications, since otherwise functions over the terms they contain cannot be guaranteed to terminate. Neither of these two specifications is well formed: Γ_{a}(1) = p ⊕ call(1); Γ_{b}(n) = call(n + 1).

We will also need a set of ‘start terms’—the subterms that can act directly.

Definition 5 (sterms). Given a wellformed Γ and a sequential process term p, sterms Γ p is the set of maximal elements related to p by the reflexive transitive closure of the ⇝_{Γ} relation^{5}:

sterms Γ (p_{1} ⊕ p_{2}) = sterms Γ p_{1} ∪ sterms Γ p_{2},
sterms Γ (call(pn)) = sterms Γ (Γ pn), and,
sterms Γ p  = {p} otherwise.

We also define ‘local start terms’ by stermsl (p_{1} ⊕ p_{2}) = stermsl p_{1} ∪ stermsl p_{2} and otherwise stermsl p = {p} to permit the sufficient syntactic condition that a specification Γ is well formed if call(pn’) ∉ stermsl (Γ pn).

Similarly to the way that start terms act as direct sources of transitions, we define ‘derivative terms’ giving possible active destinations of transitions.

Definition 6 (dterms). Given a wellformed Γ and a sequential process term p, dterms p is defined by:

dterms Γ (p_{1} ⊕ p_{2})  = dterms Γ p_{1} ∪ dterms Γ p_{2},
dterms Γ (call(pn))  = dterms Γ (Γ pn),
dterms Γ ({l}[[u]] p)  = sterms Γ p,
dterms Γ ({l}unicast(s_{ip}, s_{msg}) . p ▷ q)= sterms Γ p ∪ sterms Γ q, and so on.

5 This characterization is equivalent to {q | p ⇝_{Γ} ^{∗} q ∧ (∄ q’. q ⇝_{Γ} q’)}. Termination follows from wellformed Γ, that is, wellformed Γ ⟹ sterms-dom (Γ, p) for all p.

These derivative terms overapproximate the set of reachable sterms, since they do not consider the truth of guards nor the willingness of communication partners.

These auxiliary definitions lead to a succinct definition of the set of control terms of a specification.

Definition 7 (cterms). For a specification Γ, cterms is the smallest set where:

p ∈ sterms Γ (Γ pn) p ∈ cterms Γ

pp ∈ cterms Γ p ∈ dterms Γ pp
p ∈ cterms Γ

It is also useful to define a local version independent of any specification.

Definition 8 (ctermsl). Let ctermsl be the smallest set defined by:

ctermsl (p_{1} ⊕ p_{2})= ctermsl p_{1} ∪ ctermsl p_{2},
ctermsl (call(pn)) = {call(pn)},
ctermsl ({l}[[u]] p) = {{l}[[u]] p} ∪ ctermsl p, and so on.

Including call terms ensures that q ∈ stermsl p implies q ∈ ctermsl p, which facilitates proofs. For wellformed Γ, ctermsl allows an alternative definition of cterms,

cterms Γ = {p | ∃ pn. p ∈ ctermsl (Γ pn) ∧ not-call p}.  (1)

While the original definition is convenient for developing the meta-theory, due to the accompanying induction principle, this one is more useful for systematically generating the set of control terms of a specification, and thus, we will see, sets of verification conditions. And, for wellformed Γ, we have as a corollary

cterms Γ = {p | ∃ pn. p ∈ subterms (Γ pn) ∧ not-call p ∧ not-choice p},  (2)

where subterms, not-call, and not-choice are defined in the obvious way. We show that cterms over-approximates the set of reachable control states.

Lemma 1. For wellformed Γ and automaton A where control-within Γ (init A) and trans A = seqp-sos Γ, if (ξ, p) ∈ reachable A I and q ∈ sterms Γ p then q ∈ cterms Γ.

The predicate control-within Γ σ = ∀ (ξ, p) ∈ σ. ∃ pn. p ∈ subterms (Γ pn) serves to

state that the initial control state is within the specification.

3.2 Basic proof rule and invariants

Using the definition of invariance (Definition 2), we can state a basic property of an instance of the toy process:

ptoy i |⊧ onl Γ_{Toy} (λ(ξ, l). l ∈ {PToy-:2..PToy-:8} ⟶ nhip ξ = ip ξ),  (3)

This invariant states that between the lines labelled PToy-:2 and PToy-:8, that is, after the assignment of PToy-:1 until before the assignment of PToy-:8, the values

of nhip and ip are equal; onl Γ P, defined as λ(ξ, p). ∀ l ∈ labels Γ p. P (ξ, l), extracts

labels from control states.^{6} Invariants like these are solved using a procedure whose soundness is justified as a theorem. The proof exploits (1) and Lemma 1.

6 Using labels in this way is standard, see, for instance, [13, Chap. 1], or the ‘assertion networks’ of [18, §2.5.1]. Isabelle rapidly dispatches all the uninteresting cases.

Theorem 1. To prove A |⊧ (I →) onl Γ P, where wellformed Γ, simple-labels Γ, control-within Γ (init A), and trans A = seqp-sos Γ, it suffices

(init) for arbitrary (ξ, p) ∈ init A and l ∈ labels Γ p, to show P (ξ, l), and,

(step) for arbitrary p ∈ ctermsl (Γ pn), but not-call p, and l ∈ labels Γ p, given that p ∈ sterms Γ pp for some (ξ, pp) ∈ reachable A I, to assume P (ξ, l) and I a, and then for any (ξ’, q) such that ((ξ, p), a, (ξ’, q)) ∈ seqp-sos Γ and l’ ∈ labels Γ q, to show P (ξ’, l’).

Here, simple-labels Γ = ∀ pn. ∀ p ∈ subterms (Γ pn). ∃! l. labels Γ p = {l}: each control

term must have exactly one label, that is, ⊕ terms must be labelled consistently.

We incorporate this theorem into a tactic that (1) applies the introduction rule, (2) replaces p ∈ ctermsl (Γ pn) by a disjunction over the values of pn, (3) applies Definition 8 and repeated simplifications of Γs and eliminations on disjunctions to generate one subgoal (verification condition) for each control term, (4) replaces control term derivatives, the subterms in Definition 6, by fresh variables, and, finally, (5) tries to solve each subgoal by simplification. Step 4 replaces potentially large control terms by their (labelled) heads, which is important for readability and prover performance. The tactic takes as arguments a list of existing invariants to include after having applied the introduction rule and a list of lemmas for trying to solve any subgoals that survive the final simplification. There are no schematic variables in the subgoals and we benefit greatly from Isabelle’s parallel_goals tactical [22].

In practice, one states an invariant, applies the tactic, and examines the resulting goals. One may need new lemmas for functions over the data state or explicit proofs for difficult goals. That said, the tactic generally dispatches the uninteresting goals, and the remaining ones typically correspond with the cases treated explicitly in manual proofs [4].

For step invariants, we show a counterpart to Theorem 1, and declare it to the tactic. Then we can show, for our example, that the value of no never decreases:

ptoy i ||≡ (λ((ξ, -), -, (ξ’, -)). no ξ ≤ no ξ’).

4 Open invariance

The analysis of network protocols often requires ‘inter-node’ invariants, like

wf-net-tree n ⟹ closed (pnet (λi. ptoy i ⟨⟨ qmsg) n) |⊧

netglobal (λσ. ∀ i. no (σ i) ≤ no (σ (nhip (σ i)))) , (4)

which states that, for any net-tree with disjoint node addresses (wf-net-tree n), the value of no at a node is never greater than its value at the ‘next hop’—the address in nhip. This is a property of a global state σ mapping addresses to corresponding data states. Such a global state is readily constructed with:

netglobal P = λs. P (default toy-init (netlift fst s)), default df f = (λi. case f i of None ⇒ df i | Some s ⇒ s), and

netlift sr (s_{R}^{i}) = [i ↦ fst (sr s)]
netlift sr (s ∥ t) = netlift sr s ++ netlift sr t.

The applications of fst elide the state of qmsg and the protocol’s control state.^{7}

While we can readily state inter-node invariants of a complete model, showing them compositionally is another issue. Sections 4.1 and 4.2 present a way to state and prove such invariants at the level of sequential processes—that is, with only ptoy i left of the turnstile. Sections 4.3 and 4.4 present, respectively, rules for lifting such results to network models and for recovering invariants like (4).

4.1 The open model

Rather than instantiate the ’s of (’s, ’p, ’l) seqp with elements ξ of type state, our solution introduces a global state σ of type ip ⇒ state. This necessitates a stack of new SOS rules that we call the open model; Figure 5 shows some representatives.

The rules of oseqp-sos are parameterized by an address i and constrain only that entry of the global state, either to say how it changes (σ’ i = u (σ i)) or that it does not (σ’ i = σ i). The rules for oparp-sos only allow the first sub-process to constrain σ. This choice is disputable: it precludes comparing the states of qmsgs (and any other local filters) across a network, but is also simplifies the mechanics and use of this layer of the framework.^{8} The sets onode-sos and opnet-sos need not be parameterized since they are generated inductively from lower layers. Together they constrain subsets of elements of σ. This occurs naturally for rules like those for arrive and *cast, where the synchronous communication serves as a conjunction of constraints on sub-ranges of σ. But for others that normally only constrain a single element, like those for τ, assumptions (∀ j ≠ i. σ’ j = σ j) are introduced here and later dispatched (Section 4.4). The rules for ocnet-sos, not shown, are similar—elements not addressed within a model may not change.

The stack of operators and model layers described in Section 2 is refashioned to use the new transition rules and to distinguish the global state, which is preserved as the fst element across layers, from the local state elements which are combined in the snd element as before.

For instance, a sequential instance of the toy protocol is defined as

optoy i = (|init = {(toy-init, Γ_{Toy} PToy)}, trans = oseqp-sos Γ_{Toy} i|),

combined with the standard qmsg process using the operator

s ⟨⟨_{i} t = (|init = {(σ, (s_{l}, t_{l})) | (σ, s_{l}) ∈ init s ∧ t_{l} ∈ init t},
trans = oparp-sos i (trans s) (trans t)|) ,

and lifted to the node level via the open node constructor

⟨i : onp : R_{i}⟩_{o} = (|init = {(σ, s_{R_{i}}^{i}) | (σ, s) ∈ init onp}, trans = onode-sos (trans onp)|).

Similarly, to map a net-tree term to an open model we define:

opnet onp ⟨i; R_{i}⟩ = ⟨i : onp i : R_{i}⟩_{o}
opnet onp (p_{1} ^{∥} p_{2}) = (|init = {(σ, s_{1}∥ s_{2}) | (σ, s_{1}) ∈ init (opnet onp p_{1})
∧ (σ, s_{2}) ∈ init (opnet onp p_{2})
∧ net-ips s_{1} ∩ net-ips s_{2} = ∅},

trans = opnet-sos (trans(opnet onp p_{1})) (trans(opnet onp p_{2}))|).

7 The formulation here is a technical detail: sr corresponds to netlift as np does to pnet. 8 The treatment of the other layers is completely independent of this choice.

\frac{σ’ i = u (σ i)}{((σ, \{l\}[[u]] p), τ, (σ’, p)) ∈ oseqp-sos Γ i}  \frac{((σ, p), a, (σ’, p’)) ∈ oseqp-sos Γ i}{((σ, p ⊕ q), a, (σ’, p’)) ∈ oseqp-sos Γ i}

\frac{σ’ i = σ i}{((σ, \{l\}unicast(s_{ip}, s_{msg}) . p ▷ q), unicast (s_{ip} (σ i)) (s_{msg} (σ i)), (σ’, p)) ∈ oseqp-sos Γ i}

(a) Sequential processes: examples from oseqp-sos.

\frac{((σ, s), receive m, (σ’, s’)) ∈ S (t, send m, t’) ∈ T}{((σ, (s, t)), τ, (σ’, (s’, t’))) ∈ oparp-sos i S T}

(b) Parallel processes: example from oparp-sos.

\frac{((σ,s), receive m, (σ’,s’)) ∈ S}{((σ,s_{R}^{i}), \{i\}¬∅:arrive(m), (σ’,s’_{R}^{i})) ∈ onode-sos S}  \frac{((σ,s),τ, (σ’,s’)) ∈ S ∀ j ≠ i. σ’j = σ j}{((σ,s_{R}^{i}),τ, (σ’,s’_{R}^{i})) ∈ onode-sos S}

(c) Nodes: examples from onode-sos.

\frac{((σ, s), H¬K:arrive(m), (σ’, s’)) ∈ S ((σ, t), H’¬K’:arrive(m), (σ’, t’)) ∈ T}{((σ, s ∥ t), (H ∪ H’)¬(K ∪ K’):arrive(m), (σ’, s’∥ t’)) ∈ opnet-sos S T}

(d) Partial networks: example from opnet-sos.

Fig. 5: SOS rules for the open model (cf. Figures 1, 2, 3, and 4)

This definition is non-empty only for well-formed net-trees (net-ips gives the set of node addresses in the state of a partial network). Including such a constraint within the open model, rather than as a separate assumption like the wf-net-tree n in (4), eliminates an annoying technicality from the inductions described in Section 4.3. As with the extra premises in the open SOS rules, we can freely adjust the open model to facilitate proofs but each ‘encoded assumption’ becomes an obligation to be discharged in the transfer lemma of Section 4.4.

An operator for adding the last layer is also readily defined by

oclosed A = A(|trans := ocnet-sos (trans A)|),

giving all the definitions necessary to turn a standard model into an open one.

4.2 Open invariants

The basic definitions of reachability and invariance, Definitions 1–3, apply to open models, but constructing a compositional proof requires considering the effects of both synchronized and interleaved actions of possible environments.

Definition 9 (open reachability). Given an automaton A and assumptions S and U over, respectively, synchronized and interleaved actions, oreachable A S U is the smallest set defined by the rules:

(σ, p) ∈ init A

(σ, p) ∈ oreachable A S U U σ σ’

(σ, p) ∈ oreachable A S U

(σ’, p) ∈ oreachable A S U \frac{(σ, p) ∈ oreachable A S U ((σ, p), a, (σ’, p’)) ∈ trans A S σ σ’ a}{(σ’, p’) ∈ oreachable A S U}

In practice, we use restricted forms of the assumptions S and U, respectively,

otherwith E N I σ σ’ a = (∀ i. i ∉ N ⟶ E (σ i) (σ’ i)) ∧ I σ a ,  (5)
other F N σ σ’ = ∀ i. if i ∈ N then σ’ i = σ i else F (σ i) (σ’ i) .  (6)

The former permits the restriction of possible environments (E) and also the extraction of information from shared actions (I). The latter restricts (F) the effects of interleaved actions, which may only change non-local state elements.

Definition 10 (open invariance). Given an automaton A and assumptions S and U over, respectively, synchronized and interleaved actions, a predicate P is

an open invariant, denoted A ⊧ (S, U →) P, iff ∀ s ∈ oreachable A S U. P s.

It follows easily that existing invariants can be made open: most invariants can be shown in the basic context but still exploited in the more complicated one.

Lemma 2. Given an invariant A |⊧ (I →) P where trans A = seqp-sos Γ, and any

F, there is an open invariant A’ ⊧ (λ- -. I, other F {i} →) (λ(σ, p). P (σ i, p)) where trans A’ = oseqp-sos Γ i, provided that init A = {(σ i, p) | (σ, p) ∈ init A’}.

Open step invariance and a similar transfer lemma are defined similarly. The meta theory for basic invariants is also readily adapted, in particular,

Theorem 2. To show A ⊧ (S, U →) onl Γ P, in addition to the conditions and the obligations (init) and (step) of Theorem 1, suitably adjusted, it suffices,

(env) for arbitrary (σ, p) ∈ oreachable A S U and l ∈ labels Γ p, to assume both

P (σ, l) and U σ σ’, and then to show P (σ’, l).

This theorem is declared to the tactic described in Section 3.2 and proofs proceed as before, but with the new obligation to show invariance over interleaved steps.

We finally have sufficient machinery to state (and prove) Invariant (4) at the level of a sequential process:

optoy i ⊧ (otherwith nos-inc {i} (orecvmsg msg-ok), other nos-inc {i} →) (λ(σ, -). no (σ i) ≤ no (σ (nhip (σ i)))) ,

(7)

where nos-inc ξ ξ’ = no ξ ≤ no ξ’, orecvmsg applies its given predicate to receive actions and is otherwise true, msg-ok σ (pkt (data, src)) = (data ≤ no (σ src)),

and msg-ok σ (newpkt (data, dst)) = True. So, given that the variables no in the environment never decrease and that incoming pkts reflect the state of the sender, there is a relation between the local node and the next hop. Similar invariants occur in proofs of realistic protocols [4].

4.3 Lifting open invariants

The next step is to lift Invariant (7) over each composition operator of the open model. We mostly present the lemmas over oreachable, rather than those for open invariants and step invariants, which follow more or less directly.

The first lifting rule treats composition with the qmsg process. It mixes oreachable and reachable predicates: the former for the automaton being lifted, the latter for properties of qmsg. The properties of qmsg—only received messages are added to the queue and sent messages come from the queue—are shown using the techniques of Section 3.

Lemma 3 (qmsg lifting). Given (σ, (s, (q, t))) ∈ oreachable (A ⟨⟨_{i} qmsg) S U, where predicates S = otherwith E {i} (orecvmsg R) and U = other F {i}, and provided (1) A |≡ (S, U →) (λ((σ, -), -, (σ’, -)). F (σ i) (σ’ i)), (2) for all ξ, ξ’, E ξ ξ’ implies F ξ ξ’, (3) for all σ, σ’, m, ∀ j. F (σ j) (σ’ j) and R σ m imply R σ’ m, and, (4) F is reflexive, then (σ, s) ∈ oreachable A S U and (q, t) ∈ reachable qmsg (recvmsg (R σ)),

and furthermore ∀ m ∈ set q. R σ m.

The key intuition is that every message m received, queued, and sent by qmsg satisfies R σ m. The proof is by induction over oreachable. The R’s are preserved when the external environment acts independently (3, 4), when it acts synchronously (2), and when the local process acts (1, 3).

The rule for lifting to the node level adapts assumptions on receive actions

(orecvmsg) to arrive actions (oarrivemsg).

Lemma 4 (onode lifting). If, for all ξ and ξ’, E ξ ξ’ implies F ξ ξ’, then given

(σ, s_{R}^{i}) ∈ oreachable (⟨i : A : R_{i}⟩_{o}) (otherwith E {i} (oarrivemsg I)) (other F {i}) it follows that (σ, s) ∈ oreachable A (otherwith E {i} (orecvmsg I)) (other F {i}).

The sole condition is needed because certain node-level actions—namely connect, disconnect, and ∅¬{i}:arrive(m)—synchronize with the environment (giving E ξ ξ’) but appear to ‘stutter’ (requiring F ξ ξ’) relative to the underlying process.

The lifting rule for partial networks is the most demanding. The function net-tree-ips, giving the set of addresses in a net-tree, plays a key role.

Lemma 5 (opnet lifting). Given (σ, s ∥ t) ∈ oreachable (opnet onp (p_{1} ^{∥} p_{2})) S U, where S = otherwith E (net-tree-ips (p_{1} ^{∥} p_{2})) (oarrivemsg I), U = other F (net-tree-ips

(p_{1} ^{∥} p_{2})), and E and F are reflexive, for arbitrary p i of the form ⟨i : onp i : R⟩_{o},

p i |≡ (λσ -. oarrivemsg I σ, other F {i} →) (λ((σ, -), a, (σ’, -)). castmsg (I σ) a), and

similar step invariants for E (σ i) (σ’ i) and F (σ i) (σ’ i), then it follows that both

(σ, s) ∈ oreachable (opnet onp p_{1}) S_{1} U_{1} and (σ, t) ∈ oreachable (opnet onp p_{2}) S_{2} U_{2},

where S_{1} and U_{1} are over p_{1}, and S_{2} and U_{2} are over p_{2}.

The proof is by induction over oreachable. The initial and interleaved cases are trivial. For the local case, given open reachability of (σ, s) and (σ, t) for p_{1} and

p_{2}, respectively, and ((σ, s ∥ t), a, (σ’, s’∥ t’)) ∈ trans (opnet onp (p_{1} ^{∥} p_{2})), we must

show open reachability of (σ’, s’) and (σ’, t’). The proof proceeds by cases of a. The key step is to have stated the lemma without introducing cyclic dependencies between (synchronizing) assumptions and (step invariant) guarantees. For a synchronizing action like arrive, Definition 9 requires satisfaction of S_{1} to advance in p_{1} and of S_{2} to advance in p_{2}, but the assumption S only holds for addresses j ∉ net-tree-ips (p_{1} ^{∥} p_{2}). This is why the step invariants required of nodes only assume oarrivemsg I σ of the environment, rather than an S over node address {i}.

This is not unduly restrictive since the step invariants provide guarantees for individual local state elements and not between network nodes. The assumption oarrivemsg I σ is never cyclic: it is either assumed of the environment for paired arrives, or trivially satisfied for the side that *casts. The step invariants are lifted from nodes to partial networks by induction over net-trees. For non-synchronizing actions, we exploit the extra guarantees built into the open SOS rules.

The rule for closed networks is similar to the others. Its important function is to eliminate the synchronizing assumption (S in the lemmas above), since messages no longer arrive from the environment. The conclusion of this rule has the form required by the transfer lemma of the next section.

4.4 Transferring open invariants

The rules in the last section extend invariants over sequential processes, like that of (7), to arbitrary, open network models. All that remains is to transfer the extended invariants to the standard model. We do so using a locale [12]

openproc np onp sr where np has type ip ⇒ (’s, ’m seq-action) automaton, onp has type ip ⇒ ((ip ⇒ ’g) × ’l, ’m seq-action) automaton, and sr has type ’s ⇒ ’g × ’l. The

automata use the actions of Section 2.1 with arbitrary messages (’m seq-action).

The openproc locale relates an automaton np to a corresponding ‘open’ automaton onp, where sr splits the states of the former into global and local components. Besides two technical conditions on initial states, this relation requires

assuming σ i = fst (sr s), σ’ i = fst (sr s’) and (s, a, s’) ∈ trans (np i), and then showing ((σ, snd (sr s)), a, (σ’, snd (sr s’))) ∈ trans (onp i)—that is, that onp simulates np.

For our running example, we show openproc ptoy optoy id, and then lift it to the composition with qmsg, using a generic relation on openproc locales.

Lemma 6 (transfer). Given np, onp, and sr such that openproc np onp sr, then

for any wf-net-tree n and s ∈ reachable (closed (pnet np n)) (λ-. True), it follows that (default (someinit np sr) (netlift sr s), netliftl sr s)

∈ oreachable (oclosed (opnet onp n)) (λ- - -. True) U.

This lemma uses two openproc constants: someinit np sr i chooses an arbitrary

initial state from np (SOME x. x ∈ (fst ∘ sr) ‘ init (np i)), and

netliftl sr (s_{R}^{i}) = (snd (sr s))_{R}^{i}
netliftl sr (s ∥ t) = (netliftl sr s) ∥ (netliftl sr t).

The proof of the lemma ‘discharges’ the assumptions incorporated into the open SOS rules. An implication from an open invariant on an open model to an invariant on the corresponding standard model follows as a corollary.

Summary. The technicalities of the lemmas in this and the preceding section are essential for the underlying proofs to succeed. The key idea is that through an open version of AWN where automaton states are segregated into global and local components, one can reason locally about global properties, but still, using the so called transfer and lifting results, obtain a result over the original model.

5 Concluding remarks

We present a mechanization of a modelling language for MANET and WMN protocols, including a streamlined adaptation of standard theory for showing invariants of individual reactive processes, and a novel and compositional framework for lifting such results to network models. The framework allows the statement and proof of inter-node properties. We think that many elements of our approach would apply to similarly structured models in other formalisms.

It is reasonable to ask whether the basic model presented in Section 2 could not simply be abandoned in favour of the open model of Section 4.1. But we believe that the basic model is the most natural way of describing what AWN means, proving semantic properties of the language, showing ‘node-only’ invariants, and, potentially, for showing refinement relations. Having such a reference model allows us to freely incorporate assumptions into the open SOS rules, knowing that their soundness must later be justified.

The Ad hoc On-demand Distance Vector (AODV) case study. The framework we present in this paper was successfully applied in the mechanization of a proof of loop freedom [6, §7] of the AODV protocol [17], a widely-used routing protocol designed for MANETs, and one of the four protocols currently standardized by the IETF MANET working group. The model has about 100 control locations across 6 different processes, and uses about 40 functions to manipulate the data state. The main property (loop freedom) roughly states that ‘a data packet is never sent round in circles without being delivered’. To establish this property, we proved around 400 lemmas. Due to the complexity of the protocol logic and the length of the proof, we present the details elsewhere [4]. The case study shows that the presented framework can be applied to verification tasks of industrial relevance.

Acknowledgments. We thank G. Klein and M. Pouzet for support and complaisance, and M. Daum for participation in discussions. Isabelle/jEdit [21], Sledgehammer [2], parallel processing [22], and the TPTP project [19] were invaluable.

NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program.

References

1. J. Bengtson and J. Parrow. Psi-calculi in Isabelle. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, TPHOLs’09, volume 5674 of LNCS, pages 99– 114. Springer, 2009.

2. J. C. Blanchette, S. Böhme, and L. C. Paulson. Extending Sledgehammer with SMT solvers. In N. Bjørner and V. Sofronie-Stokkermans, editors, CADE-23, volume 6803 of LNCS, pages 116–130. Springer, 2011.

3. T. Bourke. Mechanization of the Algebra for Wireless Networks (AWN). Archive

    of Formal Proofs, 2014. http://afp.sf.net/entries/AWN.shtml.

4. T. Bourke, R. J. van Glabbeek, and P. Höfner. A mechanized proof of loop freedom of the (untimed) AODV routing protocol, 2014. See authors’ webpages.

5. K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz. Verifying safety properties with the TLA^{+} proof system. In J. Giesl and R. Hähnle, editors, IJCAR’10, volume 6173 of LNCS, pages 142–148. Springer, 2010.

6. A. Fehnker, R. J. van Glabbeek, P. Höfner, A. McIver, M. Portmann, and W. L. Tan. A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Technical Report 5513, NICTA, 2013. http://arxiv.org/

abs/1312.7645.

7. A. Feliachi, M.-C. Gaudel, and B. Wolff. Isabelle/Circus: A process specification and verification environment. In R. Joshi, P. Müller, and A. Podelski, editors, VSTTE’12, volume 7152 of LNCS, pages 243–260. Springer, 2012.

8. W. Fokkink, J. F. Groote, and M. Reniers. Process algebra needs proof methodology. In EATCS Bulletin 82, pages 109–125, 2004.

9. T. Göthel and S. Glesner. An approach for machine-assisted verification of Timed CSP specifications. Innovations in Systems and Software Engineering, 6(3):181– 193, 2010.

10. B. Heyd and P. Crégut. A modular coding of UNITY in COQ. In G. Goos, J. Hartmanis, J. Leeuwen, J. Wright, J. Grundy, and J. Harrison, editors, TPHOLs’96, volume 1125 of LNCS, pages 251–266. Springer, 1996.

11. D. Hirschkoff. A full formalisation of π-calculus theory in the Calculus of Constructions. In K. Schneider and J. Brandt, editors, TPHOLs’07, volume 4732 of LNCS, pages 153–169. Springer, 2007.

12. F. Kammüller, M. Wenzel, and L. C. Paulson. Locales: A sectioning concept for Isabelle. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, editors, TPHOLs’99, volume 1690 of LNCS, pages 149–165. Springer, 1999.

13. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer, 1995.

14. O. Müller. A Verification Environment for I/O Automata Based on Formalized Meta-Theory. PhD thesis, TU München, 1998.

15. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.

16. L. C. Paulson. The inductive approach to verifying cryptographic protocols. J. Computer Security, 6(1–2):85–128, 1998.

17. C. E. Perkins, E. M. Belding-Royer, and S. R. Das. Ad hoc on-demand distance vector (AODV) routing. RFC 3561 (Experimental), Network Working Group, 2003.

18. W.-P. de Roever, F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theor. Comp. Sci. 54. CUP, 2001.

19. G. Sutcliffe. The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. J. Automated Reasoning, 43(4):337–362, 2009.

20. H. Tej and B. Wolff. A corrected failure divergence model for CSP in Isabelle/HOL. In J. S. Fitzgerald, C. B. Jones, and P. Lucas, editors, FME’97, volume 1313 of LNCS, pages 318–337. Springer, 1997.

21. M. Wenzel. Isabelle/jEdit—a prover IDE within the PIDE framework. In J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge, editors, Intelligent Computer Mathematics, volume 7362 of LNCS, pages 468–471. Springer, 2012.

22. M. Wenzel. Shared-memory multiprocessing for interactive theorem proving. In S. Blazy, C. Paulin-Mohring, and D. Pichardie, editors, ITP’13, volume 7998 of LNCS, pages 418–434. Springer, 2013.