We introduce a notion of noninterference for a typed version of the pi-calculus where types are used to assign secrecy levels to channels. Noninterference is expressed in terms of a partial congruence (p-congruence, for short). We provide a proof technique in the form of a bisimulation-like partial equivalence relation that is a binary relation which is symmetric and transitive but not reflexive. We show that the noninterference property is compositional with respect to most of the operators of the language leading to efficient proof techniques for the verification and the construction of (compositional) secure systems. In order to allow downgrading of sensitive information, we extend the pi-calculus with declassification primitives and we study a property which scales to noninterference when downgrading is not permitted.

P-congruences as noninterference for the pi-calculus.

CRAFA, SILVIA;
2006

Abstract

We introduce a notion of noninterference for a typed version of the pi-calculus where types are used to assign secrecy levels to channels. Noninterference is expressed in terms of a partial congruence (p-congruence, for short). We provide a proof technique in the form of a bisimulation-like partial equivalence relation that is a binary relation which is symmetric and transitive but not reflexive. We show that the noninterference property is compositional with respect to most of the operators of the language leading to efficient proof techniques for the verification and the construction of (compositional) secure systems. In order to allow downgrading of sensitive information, we extend the pi-calculus with declassification primitives and we study a property which scales to noninterference when downgrading is not permitted.
Proceedings of the 2006 ACM workshop on Formal methods in security engineering, FMSE
9781595935502
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/1555784
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
social impact