On Bisimulations for the Spi Calculus

Abstract:

The spi calculus is an extension of the pi calculus with cryptographic primitives, designed for the verification of cryptographic protocols. Due to the extension, the naive adaptation of labeled bisimulations for the pi calculus is too strong to be useful for the purpose of verification. Instead, as a viable alternative, several ``environment-sensitive'' bisimulations have been proposed. In this paper we formally study the differences between these bisimulations.

	  (Volume not yet known)
	  

Static equivalence is harder than knowledge

Abstract:

There are two main ways of defining secrecy of cryptographic protocols. The first version checks if the adversary can learn the value of a secret parameter. In the second version, one checks if the adversary can notice any difference between protocol runs with different values of the secret parameter.
We give a new proof that when considering more complex equational theories than partially inversible functions, these two kinds of secrecy are not equally difficult to verify. More precisely, we identify a message language equipped with a convergent rewrite system such that after a completed protocol run, the first problem mentioned above (adversary knowledge) is decidable but the second problem (static equivalence) is not. The proof is by reduction of the ambiguity problem for context-free grammars.

Symbolic Bisimulation in the Spi Calculus

Abstract:

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.

@InProceedings{BBN04_symspibisim,
  author = 	 {Johannes Borgstr\"om and S\'ebastien Briais 
                  and Uwe Nestmann},
  title = 	 {Symbolic Bisimulation in the Spi Calculus},
  booktitle = 	 {Proc. CONCUR 2004},
  pages =	 {161-176},
  year =	 2004,
  editor =	 {Philippa Gardner and Nobuko Yoshida},
  volume =	 3170,
  series =	 {Lecture Notes in Computer Science},
  publisher =	 {Springer}
}

Verifying a Structured Peer-to-peer Overlay Network: The Static Case

Abstract:

Structured peer-to-peer overlay networks are a class of algorithms that provide efficient message routing for distributed applications using a sparsely connected communication network. In this paper, we formally verify a typical application running on a fixed set of nodes. This work is the foundation for studies of a more dynamic system.
We identify a value and expression language for a value-passing CCS that allows us to formally model a distributed hash table implemented over a static DKS overlay network. We then provide a specification of the lookup operation in the same language, allowing us to formally verify the correctness of the system in terms of observational equivalence between implementation and specification. For the proof, we employ an abstract notation for reachable states that allows us to work conveniently up to structural congruence, thus drastically reducing the number and shape of states to consider. The structure and techniques of the correctness proof are reusable for other overlay networks.

@InProceedings{BNOG04_static_dks,
  author = 	 {Johannes Borgstr\"om and Uwe Nestmann
                  and Luc Onana Alima and Dilian Gurov},
  title = 	 {Verifying a Structured Peer-to-peer 
                  Overlay Network: The Static Case},
  booktitle = 	 {Proc. Global Computing 2004},
  pages =	 {251-266},
  year =	 2004,
  editor =	 {Corrado Priami and Paoloa Quaglia},
  volume =	 3267,
  series =	 {Lecture Notes in Computer Science},
  publisher =	 {Springer}
}

On Bisimulations for the Spi Calculus

Abstract:

The spi calculus is an extension of the pi calculus with cryptographic primitives, designed for the verification of cryptographic protocols. Due to the extension, the naive adaptation of labeled bisimulations for the pi calculus is too strong to be useful for the purpose of verification. Instead, as a viable alternative, several ``environment-sensitive'' bisimulations have been proposed. In this paper we formally study the differences between these bisimulations.

@InProceedings{BN02_spibisim,
  author = 	 {Johannes Borgstr\"om and Uwe Nestmann},
  title = 	 {On Bisimulations for the Spi Calculus},
  booktitle = 	 {Proc. AMAST'02},
  pages =	 {287--303},
  year =	 2002,
  editor =	 {H. Kirchner and C. Ringeissen},
  volume =	 2422,
  series =	 {Lecture Notes in Computer Science},
  publisher =	 {Springer}
}

Symbolic Bisimulation in the Spi Calculus.