×

Deciding framed bisimilarity. (English) Zbl 1270.68216

Kucera, Antonin (ed.) et al., Infinity 2002. Selected papers of the 4th international workshop on verification of infinite-state systems (CONCUR 2002 satellite workshop), Brno, Czech Republic, August 24, 2002. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 68, No. 6, 1-18 (2003).
Summary: The spi-calculus, proposed by Abadi and Gordon, is a process calculus based on the \(\pi\)-calculus and is intended for reasoning about the behaviour of cryptographic protocols. We consider the finite-control fragment of the spi-calculus, showing it to be Turing-powerful (a result which is joint work with Josva Kleist, Uwe Nestmann, and Björn Victor). Next, we restrict our attention to finite (non-recursive) spi-calculus. Here, we show that framed bisimilarity, an equivalence relation proposed by Abadi and Gordon, showing that it is decidable for this fragment.
For the entire collection see [Zbl 1270.68031].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: Link

References:

[1] M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi-calculus. In Fourth ACM Conference on Computer and Communications Security. ACM Press, 1997. · Zbl 0924.68073
[2] Abadi, M.; Gordon, A. D.: A bisimulation method for cryptographic protocols. Nordic journal of computing 5, No. 4, 267-303 (Winter 1998) · Zbl 0913.68062
[3] R.M. Amadio, D. Lugiez. On the reachability problem in cryptographic protocols Proceedings of CONCUR 00, LNCS 1877, Springer-Verlag. · Zbl 0999.94538
[4] Boreale, Michele & De Nicola, Rocco & Pugliese, Rosario. Proof Techniques for Cryptographic Processes (Extended version). Proceedings of LICS 99, pp. 157–166, 1999. · Zbl 0928.68013
[5] Boreale, M.; Trevisan, L.: A complexity analysis of bisimilarity for value-passing processes. Theoretical computer science 238, No. Number 1-2, 313-345 (May 2000) · Zbl 0944.68135
[6] J. Borgström and U. Nestmann On Bisimulations for the Spi Calculus In Proceedings of AMAST 2002, LNCS 2422, pp. 287–303, September 2002. · Zbl 1275.68101
[7] Dam, Mads: On the decidability of process equivalences for the \({\pi}\)-calculus. Theoretical computer science 183, 215-228 (1997) · Zbl 0901.68033
[8] A.S. Elkjær, H. Hüttel M. Höhle and K. O. Nielsen. Towards automatic bisimilarity checking in the spi calculus. Proceedings of DMTCS’99 and CATS’99. Australian Computer Science Communications, 21 (3), Springer, 1999. · Zbl 0960.68066
[9] U. Frendrup and J. Nyholm Jensen. Bisimilarity in the Spi-Calculus, Masters’ Thesis, Department of Computer Science, Aalborg University, June 2001.
[10] Hans Hüttel, Josva Kleist, Uwe Nestmann and Björn Victor. A symbolic semantics for the spi-calculus. Unpublished manuscript.
[11] Huimin Lin. Complete Proof Systems for Observation Congruences in Finite-Control Pi-calculus. In Kim G. Larsen and Mogens Nielsen (editors), Automata, Languages and Programming, 25th Colloquium. Volume 1443 of Lecture Notes in Computer Science, pages 443–454, Aalborg, Denmark, July 1998, Springer-Verlag. · Zbl 0910.03020
[12] Milner, Robin; Parrow, Joachim; Walker, David: A calculus of mobile processes, parts I and II. Information and computation 100, No. 1, 1-77 (1992) · Zbl 0752.68037
[13] Milner, Robin: Communicating and mobile systems: the \({\pi}\)-calculus. (1999) · Zbl 0942.68002
[14] Minsky, Marvin: Computation: finite and infinite machines. (1967) · Zbl 0195.02402
[15] Rocco De Nicola and Matthew C. B. Hennessy. Testing equivalence for processes. In Josep Díaz (editor) Automata, Languages and Programming, 10th Colloquium. Volume 154 of Lecture Notes in Computer Science, pages 548–560, Barcelona, Spain, 18–22 July 1983. Springer-Verlag.
[16] Sangiorgi, Davide: A theory of bisimulation for the \({\pi}\)-calculus. Acta informatica 33, 69-97 (1996) · Zbl 0835.68072
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.