Section title  Observer theories  Decidability of ⊢  Proving decidability or computability

Formalising Observer Theory for Environment-Sensitive Bisimulation

Jeremy Dawson and Alwen Tiu

Logic and Computation Group School of Computer Science

College of Engineering and Computer Science Australian National University Canberra ACT 0200, Australia

http://users.rsise.anu.edu.au/^{∼}jeremy/
http://users.rsise.anu.edu.au/^{∼}tiu/

July 28, 2009

Outline

1 Section title

Subsection title

2 Observer theories

Messages Message indistinguishability Proof system for message indistinguishability Observer theory consistency

3 Decidability of ⊢

Results about theory reduction Use of theory reduction The alternative theory reduction Another proof: normal derivations Using normal derivations

4 Proving decidability or computability

Decidability of reduction

Outline

1 Section title

Subsection title

2 Observer theories

Messages Message indistinguishability Proof system for message indistinguishability Observer theory consistency

3 Decidability of ⊢

Results about theory reduction Use of theory reduction The alternative theory reduction Another proof: normal derivations Using normal derivations

4 Proving decidability or computability

Decidability of reduction

Frame title

Frame subtitle

Outline

1 Section title

Subsection title

2 Observer theories

Messages Message indistinguishability Proof system for message indistinguishability Observer theory consistency

3 Decidability of ⊢

Results about theory reduction Use of theory reduction The alternative theory reduction Another proof: normal derivations Using normal derivations

4 Proving decidability or computability

Decidability of reduction

Observer theories

We consider a formalisation of a notion of observer theories. used in various “environment-sensitive” bisimulation for process calculi, e.g., the spi-calculus. describes the knowledge and capabilities of an observer given a formal account using deductive systems

Two critical notions:

decidability of message deduction by the observer consistency of a given theory

We formalise a theory in Isabelle/HOL, encoding observer theories as pairs of symbolic traces.

Messages

Messages are formed from “names” (or flexible names), a, x, y : like variables rigid names, a, b : like constants pairs of messages, ⟨M, N⟩, symmetric encryption, {M}_{K}, (key K, message M)

datatype msg = Name nat
         | Rigid nat
         | Mpair msg msg
         | Enc msg msg

Message indistinguishability

Can an observer to differentiate two processes based on the messages output by the processes? With encryption, indistinguishability is not just syntactic equality. For Γ an observer theory (a finite set of pairs of messages) Γ ⊢ M ↔ N means the observer cannot distinguish between M and N, given the indistinguishability assumption Γ In Isabelle, (Γ, M, N) ∈ indist

Proof system for message indistinguishability

{x ∈ N \atop Γ ⊢ x ↔ x} (var)  {(M, N) ∈ Γ \atop Γ ⊢ M ↔ N} (id)
Γ ⊢ M_{a} ↔ N_{a} Γ ⊢ M_{b} ↔ N_{b}
Γ ⊢ ⟨M_{a}, M_{b}⟩ ↔ ⟨N_{a}, N_{b}⟩

(pr)

Γ ⊢ M_{p} ↔ N_{p} Γ ⊢ M_{k} ↔ N_{k}
Γ ⊢ {M_{p}}_{M_{k}} ↔ {N_{p}}_{N_{k}}

(er)

Γ, (M_{a}, N_{a}), (M_{b}, N_{b}) ⊢ M ↔ N Γ, (⟨M_{a}, M_{b}⟩, ⟨N_{a}, N_{b}⟩) ⊢ M ↔ N

(pl)

Γ ⊢ M_{k} ↔ N_{k} Γ, (M_{p}, N_{p}), (M_{k}, N_{k}) ⊢ M ↔ N

Γ, ({M_{p}}_{M_{k}}, {N_{p}}_{N_{k}}) ⊢ M ↔ N (el)

Section title  Observer theories  Decidability of ⊢  Proving decidability or computability

Lemmas regarding the proof system

(These lemmas in Tiu, 2007) “Cut-admissibility” If Γ ⊢ M ↔ N and Δ, (M, N) ⊢ R ↔ T then Γ ∪ Δ ⊢ R ↔ T Partial invertibility of rules Γ, (⟨M_{a}, M_{b}⟩, ⟨N_{a}, N_{b}⟩) ⊢ M ↔ N ⟺ Γ, (M_{a}, N_{a}), (M_{b}, N_{b}) ⊢ M ↔ N If Γ, ({M_{p}}_{M_{k}}, {N_{p}}_{N_{k}}) ⊢ M_{k} ↔ N_{k}, then Γ, ({M_{p}}_{M_{k}}, {N_{p}}_{N_{k}}) ⊢ M ↔ N ⟺ Γ, (M_{p}, N_{p}), (M_{k}, N_{k}) ⊢ M ↔ N Γ ⊢ ⟨M_{a}, M_{b}⟩ ↔ ⟨N_{a}, N_{b}⟩ ⟺ Γ ⊢ M_{a} ↔ N_{a} and Γ ⊢ M_{b} ↔ N_{b} If Γ ⊢ M_{k} ↔ N_{k} then Γ ⊢ {M_{p}}_{M_{k}} ↔ {N_{p}}_{N_{k}} ⟺ Γ ⊢ M_{p} ↔ N_{p}

Observer theory consistency

Intuitively, is the theory plausibly a set of pairs of messages which the observer would see as indistinguishable ? For example, the theory {({a}_{b}, {c}_{d}), (b, c)} is not consistent, since on the first projection (i.e., the set {{a}_{b}, b}), one can decrypt the first message {a}_{b} using the second message b, but the same operation cannot be done on the second projection. Definition in paper, proved equivalent to: A theory Γ is consistent if for every M and N, if Γ ⊢ M ↔ N then the following hold:

1 M and N are of the same type of expressions, i.e., M is a pair

(an encrypted message, a (rigid) name) if and only if N is. 2 for every M′, N′, M_{p}, N_{p} if Γ ⊢ M′ ↔ N′ or

Γ ⊢ {M_{p}}_{M′} ↔ {N_{p}}_{N′}, then M′ = M iff N′ = N

Outline

1 Section title

Subsection title

2 Observer theories

Messages Message indistinguishability Proof system for message indistinguishability Observer theory consistency

3 Decidability of ⊢

Results about theory reduction Use of theory reduction The alternative theory reduction Another proof: normal derivations Using normal derivations

4 Proving decidability or computability

Decidability of reduction

Decidability of ⊢

We want consistency to be decidable but this involves deciding Γ ⊢ M ↔ N Naive approach to testing Γ ⊢ M ↔ N can loop, as in (el) rule, left premise can equal the conclusion Finiteness argument shows decidability since backwards proof only introduces sub-messages of messages in conclusion But we want a more focussed procedure than exhaustive search ergo, theory reduction: we “reduce” a theory to its “simplest” form

Theory reduction

As originally defined (Tiu, 2007)

Γ, (⟨M_{a}, M_{b}⟩, ⟨N_{a}, N_{b}⟩) ⟶ Γ, (M_{a}, N_{a}), (M_{b}, N_{b})
Γ, ({M_{p}}_{M_{k}}, {N_{p}}_{N_{k}}) ⟶ Γ, (M_{p}, N_{p}), (M_{k}, N_{k})
if Γ, ({M_{p}}_{M_{k}}, {N_{p}}_{N_{k}}) ⊢ M_{k} ↔ N_{k}

(assume (⟨M_{a}, M_{b}⟩, ⟨N_{a}, N_{b}⟩) ∉ Γ ; ({M_{p}}_{M_{k}}, {N_{p}}_{N_{k}}) ∉ Γ) This involves deciding whether Γ, ({M_{p}}_{M_{k}}, {N_{p}}_{N_{k}}) ⊢ M_{k} ↔ N_{k} Alternative definition:

Γ, (⟨M_{a}, M_{b}⟩, ⟨N_{a}, N_{b}⟩) ⟶′ Γ, (M_{a}, N_{a}), (M_{b}, N_{b})
Γ, ({M_{p}}_{M_{k}}, {N_{p}}_{N_{k}}) ⟶′ Γ, (M_{p}, N_{p}), (M_{k}, N_{k}) if Γ ⊢ M_{k} ↔ N_{k}

This involves deciding Γ ⊢ M_{k} ↔ N_{k} (a smaller theory Γ).

Results about theory reduction

If Γ ⟶ Γ′ then Γ ⊢ M ↔ N if and only if Γ′ ⊢ M ↔ N ⟶ is clearly well-founded (as total size reduces) Note, ⟶′ ⊆ ⟶, so the above hold for ⟶′ also. By first result, side condition for the second rule for ⟶ continue to hold, or not (for a particular M_{k}, N_{k}), so confluence seems easy. (Actually, Isabelle proof difficult, as number of cases explodes). Thus Γ has a ⟶-normal form Γ⇓

Section title  Observer theories  Decidability of ⊢  Proving decidability or computability

Use of theory reduction

We define a right derivation ⊢_{R}

{x ∈ N \atop Γ ⊢_{R} x ↔ x} (var)  {(M, N) ∈ Γ \atop Γ ⊢_{R} M ↔ N} (id)
Γ ⊢_{R} M_{a} ↔ N_{a} Γ ⊢_{R} M_{b} ↔ N_{b}
Γ ⊢_{R} ⟨M_{a}, M_{b}⟩ ↔ ⟨N_{a}, N_{b}⟩

(pr)

Γ ⊢_{R} M_{p} ↔ N_{p} Γ ⊢_{R} M_{k} ↔ N_{k}
Γ ⊢_{R} {M_{p}}_{M_{k}} ↔ {N_{p}}_{N_{k}}

(er)

Now Γ ⊢_{R} M ↔ N is obviously decidable (just keep decomposing the right-hand side).

The alternative theory reduction ⟶′

If Γ is ⟶-reducible, then it is ⟶′-reducible, (even though the same reduction may not be available) (long proof in paper) Therefore (recall ⟶′ ⊆ ⟶) Γ⇓ is also the ⟶′-normal form of Γ Now we get decidability: to decide whether Γ ⊢ M ↔ N is: calculate Γ⇓ and determine whether Γ⇓ ⊢ M ↔ N. Calculating Γ⇓ requires deciding questions of the form Γ′ ⊢ M_{k} ↔ N_{k}, where Γ′ is smaller than Γ (because a pair ({M_{p}}_{M_{k}},{N_{p}}_{N_{k}}) is omitted). Thus this procedure terminates.

Section title  Observer theories  Decidability of ⊢  Proving decidability or computability

Another proof: normal derivations

Recall the right derivation ⊢_{R}; we define a normal derivation ⊢_{N}

Γ ⊢_{R} M ↔ N ; Γ ⊢_{N} M ↔ N (virt)
Γ, (M_{a}, N_{a}), (M_{b}, N_{b}) ⊢_{N} M ↔ N
Γ, (⟨M_{a}, M_{b}⟩, ⟨N_{a}, N_{b}⟩) ⊢_{N} M ↔ N

(pl)

Γ ⊢_{R} M_{k} ↔ N_{k} Γ, (M_{p}, N_{p}), (M_{k}, N_{k}) ⊢_{N} M ↔ N
Γ, ({M_{p}}_{M_{k}}, {N_{p}}_{N_{k}}) ⊢_{N} M ↔ N

(el)

Using normal derivations

Can prove that Γ ⊢_{N} M ↔ N iff Γ ⊢ M ↔ N This supports definition of yet another reduction relation ⟶_{R}, like ⟶′, but with side condition Γ ⊢_{R} M_{k} ↔ N_{k} So clearly ⟶_{R} ⊆ ⟶. We can get a similar result to that for ⟶′, that if Γ is ⟶-reducible, then it is ⟶_{R}-reducible, (even though the same reduction may not be available), and so Γ⇓ is the ⟶_{R}-normal form of Γ. As Γ ⊢_{R} M ↔ N is decidable, so Γ⇓ is computable.

Outline

1 Section title

Subsection title

2 Observer theories

Messages Message indistinguishability Proof system for message indistinguishability Observer theory consistency

3 Decidability of ⊢

Results about theory reduction Use of theory reduction The alternative theory reduction Another proof: normal derivations Using normal derivations

4 Proving decidability or computability

Decidability of reduction

Proving decidability or computability

To formally prove computability requires modellling the computation process. We can “semi-formally” prove computability: We have set out rules above for Γ ⊢_{R} M ↔ N, leading to a definition in Isabelle as an inductively defined set. We provided an alternative definition as a recursive function

is der virt, eg

Γ ⊢ ⟨M_{a}, M_{b}⟩ ↔ ⟨N_{a}, N_{b}⟩ ⟺ (⟨M_{a}, M_{b}⟩, ⟨N_{a}, N_{b}⟩) ∈ Γ∨(Γ ⊢ M_{a} ↔ N_{a}∧Γ ⊢ M_{b} ↔ N_{b})

Isabelle makes us prove that the recursive function is der virt terminates. We can inspect to see the absence of any further “infinite” features (eg testing for membership of an infinite set, quantification over an infinite set) We then proved Γ ⊢_{R} M ↔ N iff is der virt (Γ, M, N)

Section title  Observer theories  Decidability of ⊢  Proving decidability or computability

Decidability of reduction

TO BE DONE