Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Symbolic Bisimulation in the Spi Calculus
EPFL.
EPFL.
EPFL.
2004 (English)In: CONCUR 2004: Concurrency theory, proceedings / [ed] P. Gardner and N. Yoshida, Berlin Heidelberg: Springer Berlin/Heidelberg, 2004, Vol. 3170, p. 161-176Conference paper, Published paper (Refereed)
Abstract [en]

The spi calculus is an executable model for the description and analysis of cryptographic protocols. Security objectives like secrecy and authenticity can be formulated as equations between spi calculus terms, where equality is interpreted as a contextual equivalence. One problem with verifying contextual equivalences for message-passing process calculi is the infinite branching on process input. In this paper, we propose a general symbolic semantics for the spi calculus, where an input prefix gives rise to only one transition. To avoid infinite quantification over contexts, non-contextual concrete bisimulations approximating barbed equivalence have been defined. We propose a symbolic bisimulation that is sound with respect to barbed equivalence, and brings us closer to automated bisimulation checks.

Place, publisher, year, edition, pages
Berlin Heidelberg: Springer Berlin/Heidelberg, 2004. Vol. 3170, p. 161-176
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 3170
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-161485DOI: 10.1007/978-3-540-28644-8_11ISBN: 3-540-22940-X (print)OAI: oai:DiVA.org:uu-161485DiVA, id: diva2:456278
Conference
International Conference on Concurrency Theory (CONCUR), 15th international conference, August 31 - September 3, 2004, London, UK
Available from: 2011-12-06 Created: 2011-11-14 Last updated: 2018-01-12Bibliographically approved

Open Access in DiVA

fulltext(521 kB)264 downloads
File information
File name FULLTEXT02.pdfFile size 521 kBChecksum SHA-512
c172935c99a6e43a55af3746755ca04f51a4f3d38aebbf3984fadf689da79a8f83c5078ffd1bb5cc6bd4d71e202e13ac4530be0c6a4776068d8f742aa1311c11
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Borgström, Johannes
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 264 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 395 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf