Static analysis for secrecy and non-interference in networks of processes

C. Bodei; P. Degano; Hanne Riis Nielson; Flemming Nielson

doi:10.1007/3-540-44743-1_3

Static analysis for secrecy and non-interference in networks of processes

C. Bodei, P. Degano, Hanne Riis Nielson, Flemming Nielson

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Abstract

We introduce the νSPI-calculus that strengthens the notion of “perfect symmetric cryptography” of the spi-calculus by taking time into account. This involves defining an operational semantics, defining a control flow analysis (CFA) in the form of a flow logic, and proving semantic correctness. Our first result is that secrecy in the sense of Dolev- Yao can be expressed in terms of the CFA. Our second result is that also non-interference in the sense of Abadi can be expressed in terms of the CFA; unlike Abadi we find the non-interference property to be an extension of the Dolev-Yao property.

Original language	English
Title of host publication	Proc. PACT'01
Publisher	Springer
Publication date	2001
Pages	27-41
DOIs	https://doi.org/10.1007/3-540-44743-1_3
Publication status	Published - 2001
Event	6th International Conference on Parallel Computing Technologies - Novosibirsk, Russian Federation Duration: 3 Sept 2001 → 7 Sept 2001 Conference number: 6

Conference

Conference	6th International Conference on Parallel Computing Technologies
Number	6
Country/Territory	Russian Federation
City	Novosibirsk
Period	03/09/2001 → 07/09/2001

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2177
ISSN	0302-9743

Access to Document

10.1007/3-540-44743-1_3

OpenUrl availability

Full text

Cite this

@inproceedings{d287a15e81184de1ba660451b60058ac,

title = "Static analysis for secrecy and non-interference in networks of processes",

abstract = "We introduce the νSPI-calculus that strengthens the notion of “perfect symmetric cryptography” of the spi-calculus by taking time into account. This involves defining an operational semantics, defining a control flow analysis (CFA) in the form of a flow logic, and proving semantic correctness. Our first result is that secrecy in the sense of Dolev- Yao can be expressed in terms of the CFA. Our second result is that also non-interference in the sense of Abadi can be expressed in terms of the CFA; unlike Abadi we find the non-interference property to be an extension of the Dolev-Yao property. ",

author = "C. Bodei and P. Degano and Nielson, {Hanne Riis} and Flemming Nielson",

year = "2001",

doi = "10.1007/3-540-44743-1_3",

language = "English",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "27--41",

booktitle = "Proc. PACT'01",

note = "6th International Conference on Parallel Computing Technologies, PaCT 2001 ; Conference date: 03-09-2001 Through 07-09-2001",

}

Bodei, C, Degano, P, Nielson, HR & Nielson, F 2001, Static analysis for secrecy and non-interference in networks of processes. in Proc. PACT'01. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2177, pp. 27-41, 6th International Conference on Parallel Computing Technologies, Novosibirsk, Russian Federation, 03/09/2001. https://doi.org/10.1007/3-540-44743-1_3

Static analysis for secrecy and non-interference in networks of processes. / Bodei, C.; Degano, P.; Nielson, Hanne Riis et al.
Proc. PACT'01. Springer, 2001. p. 27-41 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 2177).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Static analysis for secrecy and non-interference in networks of processes

AU - Bodei, C.

AU - Degano, P.

AU - Nielson, Hanne Riis

AU - Nielson, Flemming

N1 - Conference code: 6

PY - 2001

Y1 - 2001

N2 - We introduce the νSPI-calculus that strengthens the notion of “perfect symmetric cryptography” of the spi-calculus by taking time into account. This involves defining an operational semantics, defining a control flow analysis (CFA) in the form of a flow logic, and proving semantic correctness. Our first result is that secrecy in the sense of Dolev- Yao can be expressed in terms of the CFA. Our second result is that also non-interference in the sense of Abadi can be expressed in terms of the CFA; unlike Abadi we find the non-interference property to be an extension of the Dolev-Yao property.

AB - We introduce the νSPI-calculus that strengthens the notion of “perfect symmetric cryptography” of the spi-calculus by taking time into account. This involves defining an operational semantics, defining a control flow analysis (CFA) in the form of a flow logic, and proving semantic correctness. Our first result is that secrecy in the sense of Dolev- Yao can be expressed in terms of the CFA. Our second result is that also non-interference in the sense of Abadi can be expressed in terms of the CFA; unlike Abadi we find the non-interference property to be an extension of the Dolev-Yao property.

U2 - 10.1007/3-540-44743-1_3

DO - 10.1007/3-540-44743-1_3

M3 - Article in proceedings

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 27

EP - 41

BT - Proc. PACT'01

PB - Springer

T2 - 6th International Conference on Parallel Computing Technologies

Y2 - 3 September 2001 through 7 September 2001

ER -

Static analysis for secrecy and non-interference in networks of processes

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this