Finiteness of the Search for Respectful Substitutions

Jeremy E. Dawson and Alwen Tiu

Logic and Computation Group 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/

Abstract. YET TO CHANGE FROM TPHOLS 2009 PAPER We consider a formalisation of a notion of observer (or intruder) theories, commonly used in symbolic analysis of security protocols. An observer theory describes the knowledge and capabilities of an observer, and can be given a formal account using deductive systems, such as those used in various “environment-sensitive” bisimulation for process calculi, e.g., the spi-calculus. Two notions are critical to the correctness of such formalisations and the effectiveness of symbolic techniques based on them: decidability of message deduction by the observer and consistency of a given observer theory. We consider a formalisation, in Isabelle/HOL, of both notions based on an encoding of observer theories as pairs of symbolic traces. This encoding has recently been used in a theory of open bisimulation for the spi-calculus. We machine-checked some important properties, including decidability of observer deduction and consistency, and some key steps which are crucial to the automation of open bisimulation checking for the spi-calculus, and highlight some novelty in our Isabelle/HOL formalisations of decidability proofs.

1 Introduction

YET TO CHANGE FROM TPHOLS 2009 PAPER In most symbolic techniques for reasoning about security protocols, certain assumptions are often made concerning the capability of an intruder that tries to compromise the protocols. A well-known model of intruder is the so-called Dolev-Yao model [10], which assumes perfect crytography. We consider here a formal account of Dolev-Yao intruder model, formalised as some sort of deduction system. This deductive formulation is used in formalisations of various “environment-sensitive” bisimulations (see e.g., [6]) for process calculi designed for modeling security protocols, such as the spi-calculus [3]. An environment-sensitive bisimulation is a bisimulation relation which is indexed by a structure representing the intruder’s knowledge, which we call an observer theory.

An important line of work related to the spi-calculus, or process calculi in general, is that of automating bisimulation checking. The transition semantics of these calculi often involve processes with infinite branching (e.g., transitions for input-prefixed processes in the π-calculus [12]), and therefore a symbolic method is needed to deal with potential infinite branches lazily. The resulting bisimulation, called symbolic bisimulation, has been developed for the spi-calculus [7]. The work reported in [7] is, however, only aimed at finding an effective approximation of environment-sensitive bisimulation, and there has been no metatheory developed for this symbolic bisimulation so far. A recent work by the second author [14] attempts just that: to establish a symbolic bisimulation that has good metatheory, in particular, a symbolic bisimulation which is also a congruence. The latter is also called open bisimulation [13]. One important part of the formulation of open bisimulation for the spi-calculus is a symbolic representation of observer theories, which needs to satisfy certain consistency properties, in addition to closure under a certain notion of “respectful substitutions”, as typical in formulations of open bisimulation.

A large part of the work on open bisimulation in [14] deals with establishing properties of observer theories and their symbolic counterparts. This paper is essentially about formally verifying the results of [14] concerning properties of (symbolic) observer theories in Isabelle/HOL. In particular, it is concerned with proving decidability of the deduction system for observer theory, correctness of a finite characterisation of consistency of observer theories (hence decidability of consistency of observer theories), and preservation of consistency under respectful substitutions. Additionally, we also verify some key steps towards a decision procedure for checking consistency of symbolic observer theories, which is needed in automation of open bisimulation. A substantial formalisation work described here concerns decidability proofs. Such proofs are difficult to formalise in Isabelle/HOL, as noted in [17], due to the fact that Isabelle/HOL is based on classical logic. We essentially follow [17] in that decidability in this case can be inferred straightforwardly by inspection on the way we define total functions corresponding to the decidability problems in question. That is, we show, by meta-level inspection, that the definitions of the functions do not introduce any infinite aspect and are therefore are finitely computable.

There is a recent work [11] in formalising the spi-calculus and a notion of environment-sensitive bisimulation (called the hedged bisimulation [8]) in Isabelle/HOL. However, this notion of bisimulation is a “concrete” bisimulation (as opposed to symbolic), which means that the structure of observer theories is less involved and much easier to deal with compared to its symbolic counterpart. Our work on observer theories is mostly orthogonal to their work, and it can eventually be integrated into their formalisation to provide a completely formalised open bisimulation for the spi-calculus. Such an integration may not be too difficult, given that much of their work, e.g., formalisation of the operational semantics of the spi-calculus, can be reused without modifications.

NEW TO THIS PAPER

In [?] we discussed respectful substitutions for bitraces. Since a bitrace is a sequence of pairs of messages (marked as input or output), we projected this notion to a similar trace of single messages. This gave the notion of a “respectful substitution” trace of single messages. We reproduce [?, Theorem 20] here.

Theorem 1 (subst exists, subst unique). Given a consistent bi-trace h whose projections to a single message trace are s_{1} and s_{2}, and a substitution θ_{1} which respects s_{1}, there exists θ_{2} such that θ⃗ = (θ_{1}, θ_{2}) respects h, and θ_{2} is “unique” in the sense that any two such θ_{2} act the same on names in π_{2}(h)

We also reproduce (in part) the definition of a consistent bi-trace.

Definition 2. [15, Definition 35] The set of consistent bi-traces are defined inductively (on the length of bi-traces) as follows:

(a) The empty bi-trace is consistent.

(b) If h is a consistent bi-trace then h.(M, N)^{i} is also a consistent bi-trace, provided that h ⊢ M ↔ N.

(c) If h is a consistent bi-trace, then h′ = h.(M, N)^{o} is a consistent bi-trace, provided that for every h-respectful substitution pair θ⃗, {h′θ⃗} is a consistent theory.

We assume that the reader is familar with Isabelle proof assistant, its object logic HOL and logical frameworks in general. In the remainder of this section we briefly describe relevant Isabelle notations used throughout the paper. In Section ??, we give an overview of observer theories and an intuition behind them. We also give a brief description of two problems that will be the focus of subsequent sections, namely, those that concern decidability of consistency checking for (symbolic) observer theories. In Section ?? we consider formalisation of a notion of theory reduction and decidability of consistency checking for observer theories. In Section ?? we discuss a symbolic representation of observer theories using pairs of symbolic traces [5], called bi-traces, their consistency requirements and a notion of respectful substitutions. We prove a key lemma which relates a symbolic technique for trace refinement [5] to bi-traces, and discuss how this may lead to a decision procedure for testing bi-trace consistency. Section 2 concludes.

Isabelle notation The Isabelle codes for the results of this paper can be found at

http://users.rsise.anu.edu.au/^{∼}jeremy/isabelle/2005/spi/. In the state-

ment of lemma or theorem, a name given in typewriter font indicates the name of the relevant theorem in our Isabelle development. We show selected theorems and definitions in the text, and more in the Appendix. A version of the paper, in-

cluding the Appendix, is in http://users.rsise.anu.edu.au/^{∼}jeremy/pubs/

spi/fotesb/. So now we indicate some key points of the Isabelle notation.

– A name preceded by ? indicates a variable: other names are entities which have been defined as part of the theory

– Conclusion β depending on assumptions α_{i} is [| α_{1};α_{2}; …;α_{n} |] ==> β – ∀, ∃ are written as ALL, EX

– ⊆, ⊇, ∈ are written as <=, >=, :

2 Conclusions and Further Work

YET TO CHANGE FROM TPHOLS 2009 PAPER

We have modelled observer theories and bi-traces in the Isabelle theorem prover, and have confirmed, by proofs in Isabelle, the results of a considerable part of [14]. This work constitutes a significant step formalising open bisimulation for the spi-calculus in Isabelle/HOL, and ultimately towards a logical framework for proving process equivalence.

We discussed the issue of showing finite computability in Isabelle/HOL, using a mixed formal/informal argument, and building upon the discussion in Urban et al [17]. We defined a function reduce in Isabelle, and showed that it computes Γ⇓. Isabelle required us to show that the function terminates. We asserted, with relevant discussion, that inspection shows that the definition does not introduce any infinite aspect into the computation and so asserted that therefore the function is finitely computable. Similarly, we provided a finitely computable function is der virt and proved that it tests Γ ⊢ M ↔ N for a reduced theory Γ.

We then considered bi-traces and bi-trace consistency. The problem here is that, to test bi-trace consistency, it is necessary to test whether Γ θ is consistent for all θ satisfying certain conditions. We proved a number of lemmas which simplify this task, and appear to lead to a finitely computable algorithm for this. In particular, our result on the unique completion of respectful substitutions that relates symbolic trace and bi-trace opens up the possibility to use symbolic trace refinement algorithm [5] to compute a notion of bi-trace refinement, which will be useful for bi-trace consistency checking.

Another approach to representating observer theories is to use equational theories, instead of deduction rules, e.g., as in the applied-pi calculus [1]. In this setting, the notion of consistency of a theory is replaced by the notion of static equivalence between knowledge of observers [1]. Baudet has shown that static equivalence between two symbolic theories is decidable [4], for a class of theories called subterm-convergent theories (which subsumes the Dolev-Yao model of intruder). It will be interesting to work out the precise correspondence between static equivalence and our notion of bi-trace consistency, as such correspondence may transfer proof techniques from one approach to the other.

Acknowledgment We thank the anonymous referees for their comments on an earlier draft. This work is supported by the Australian Research Council through the Discovery Projects funding scheme (project number DP0880549).

References

1. Martín Abadi and Cédric Fournet. Mobile values, new names, and secure communication. In POPL, pages 104–115, 2001.

2. Martín Abadi and Andrew D. Gordon. A bisimulation method for cryptographic protocols. Nord. J. Comput., 5(4):267–303, 1998.

3. Martin Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1–70, 99.

4. Mathieu Baudet. Sécurité des protocoles cryptographiques: aspects logiques et calculatoires. PhD thesis, École Normale Supérieure de Cachan, France, 2007.

5. Michele Boreale. Symbolic trace analysis of cryptographic protocols. In Proceedings of ICALP 2001, volume 2076 of LNCS, pages 667 – 681. Springer-Verlag, 2001.

6. Michele Boreale, Rocco De Nicola, and Rosario Pugliese. Proof techniques for cryptographic processes. SIAM J. Comput., 31(3):947–986, 2001.

7. Johannes Borgström, Sébastien Briais, and Uwe Nestmann. Symbolic bisimulation in the spi calculus. In CONCUR, vol. 3170 of LNCS, pp 161–176. Springer, 2004.

8. Johannes Borgström and Uwe Nestmann. On bisimulations for the spi calculus. Mathematical Structures in Computer Science, 15(3):487–552, 2005.

9. J. E. Dawson and R. Goré. Formalising cut-admissibility for provability logic. Submitted, 2009.

10. D. Dolev and A. Yao. On the security of public-key protocols. IEEE Transactions on Information Theory, 2(29), 1983.

11. Temesghen Kahsai and Marino Miculan. Implementing spi calculus using nominal techniques. In CiE, volume 5028 of LNCS, pages 294–305. Springer, 2008.

12. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, Part II. Information and Computation, pages 41–77, 1992.

13. Davide Sangiorgi. A theory of bisimulation for the pi-calculus. Acta Inf., 33(1):69– 97, 1996.

14. Alwen Tiu. A trace based bisimulation for the spi calculus: An extended abstract. In Proc. APLAS, vol. 4807 of LNCS, pages 367–382. Springer, 2007.

15. Alwen Tiu. A trace based bisimulation for the spi calculus. Preprint, available

from http://arxiv.org/pdf/0901.2166v1, 2009.

16. Alwen Tiu and Rajeev Goré. A proof theoretic analysis of intruder theories. In Proceedings of RTA 2009, 2009. To appear.

17. Christian Urban, James Cheney, and Stefan Berghofer. Mechanizing the metatheory of LF. In LICS, pages 45–56. IEEE Computer Society, 2008.