×

A complete symbolic bisimilarity for an extended spi calculus. (English) Zbl 1294.68109

Kremer, Steve (ed.) et al., Proceedings of the 6th international workshop on security issues in concurrency (SecCo 2008), Toronto, Canada, August 23, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 242, No. 3, 3-20 (2009).
Summary: Several symbolic notions of bisimilarity have been defined for the spi calculus and the applied pi calculus. In this paper, we treat a spi calculus with a general constructor-destructor message algebra, and define a symbolic bisimilarity that is both sound and complete with respect to its concrete counterpart.
For the entire collection see [Zbl 1281.68030].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
94A60 Cryptography
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.; Cortier, V., Deciding knowledge in security protocols under equational theories, Theoretical Computer Science, 367, 2-32 (2006) · Zbl 1153.94339
[2] Abadi, M. and C. Fournet, Mobile values, new names, and secure communicationProceedings of POPL ’01; Abadi, M. and C. Fournet, Mobile values, new names, and secure communicationProceedings of POPL ’01 · Zbl 1323.68398
[3] Abadi, M.; Gordon, A. D., A bisimulation method for cryptographic protocols, Nordic Journal of Computing, 5, 267-303 (1998) · Zbl 0913.68062
[4] Abadi, M.; Gordon, A. D., A calculus for cryptographic protocols: The Spi calculus, Journal of Information and Computation, 148, 1-70 (1999) · Zbl 0924.68073
[5] Baldamus, M.; Parrow, J.; Victor, B., A fully abstract encoding of the pi-calculus with data terms, (Proceedings of ICALP ’05. Proceedings of ICALP ’05, LNCS, 3580 (2005)), 1202-1213 · Zbl 1085.68594
[6] Baudet, M., “Sécurité des protocoles cryptographiques : aspects logiques et calculatoires,” Ph.D. thesis, École Normale Supérieure de Cachan (2007); Baudet, M., “Sécurité des protocoles cryptographiques : aspects logiques et calculatoires,” Ph.D. thesis, École Normale Supérieure de Cachan (2007)
[7] Blanchet, B., An efficient cryptographic protocol verifier based on Prolog rulesProceedings of CSFW’01; Blanchet, B., An efficient cryptographic protocol verifier based on Prolog rulesProceedings of CSFW’01
[8] Boreale, M., “Process Algebraic Theories for Mobile Systems,” Ph.D. thesis, Università degli Studi di Roma “La Sapienza” (1995); Boreale, M., “Process Algebraic Theories for Mobile Systems,” Ph.D. thesis, Università degli Studi di Roma “La Sapienza” (1995)
[9] Boreale, M.; De Nicola, R.; Pugliese, R., Proof techniques for cryptographic processes, (Proceedings of LICS ’99 (1999), IEEE), 157-166
[10] Borgström, J., “Equivalences and Calculi for Formal Verification of Cryptographic Protocols,” Ph.D. thesis, EPFL (2008); Borgström, J., “Equivalences and Calculi for Formal Verification of Cryptographic Protocols,” Ph.D. thesis, EPFL (2008)
[11] Borgström, J.; Briais, S.; Nestmann, U., Symbolic bisimulation in the spi calculus, (Proceedings of CONCUR ’04. Proceedings of CONCUR ’04, LNCS, 3170 (2004)), 161-176 · Zbl 1099.68665
[12] Borgström, J.; Nestmann, U., On bisimulations for the spi calculus, Mathematical Structures in Computer Science, 15, 487-552 (2005) · Zbl 1077.18004
[13] Delaune, S., S. Kremer and M. D. Ryan, Coercion-resistance and receipt-freeness in electronic votingProceedings of CSFW’06; Delaune, S., S. Kremer and M. D. Ryan, Coercion-resistance and receipt-freeness in electronic votingProceedings of CSFW’06
[14] Delaune, S.; Kremer, S.; Ryan, M. D., Symbolic bisimulation for the applied pi-calculus, (Proceedings of FSTTCS’07. Proceedings of FSTTCS’07, LNCS, 4855 (2007)), 133-145 · Zbl 1135.94327
[15] Hennessy, M.; Lin, H., Symbolic bisimulations, Theoretical Computer Science, 138, 353-389 (1995) · Zbl 0874.68187
[16] Hüttel, H., Deciding framed bisimilarityPre-proceedings of INFINITY ’02; Hüttel, H., Deciding framed bisimilarityPre-proceedings of INFINITY ’02
[17] Johansson, M. and B. Victor, A fully abstract symbolic semantics for the applied pi-calculus; Johansson, M. and B. Victor, A fully abstract symbolic semantics for the applied pi-calculus
[18] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, part I/II, Journal of Information and Computation, 100, 1-77 (1992)
[19] Paulson, L. C., The inductive approach to verifying cryptographic protocols, Journal of Computer Security, 6, 85-128 (1998)
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.