Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols

S. Bistarelli; I. Cervesato; Gabriele Lenzini; F. Martinelli

doi:10.1007/978-3-540-45215-7_7

Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols

S. Bistarelli, I. Cervesato, Gabriele Lenzini, F. Martinelli

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

50 Downloads (Pure)

Abstract

When formalizing security protocols, different specification languages support very different reasoning methodologies whose results are not directly or easily comparable. Therefore, establishing clear mappings among different frameworks is highly desirable, as it permits various methodologies to cooperate by interpreting theoretical and practical results of one system in another. We examine the non-trivial relationship between two general verification frameworks: multiset rewriting (MSR) and a process algebra (PA) inspired to CCS and the π-calculus. Although defining a simple and general bi-jection between MSR and PA appears difficult, we show that the sublanguages needed to specify a large class of cryptographic protocols (immediate decryption protocols) admits an effective translation that is not only bi-jective and trace-preserving, but also induces a weak form of bisimulation across the two languages. In particular, the correspondence sketched in this abstract permits transferring several important trace-based properties such as secrecy and many forms of authentication

Original language	English
Title of host publication	Computer Network Security
Subtitle of host publication	Second International Workshop on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2003, St. Petersburg, Russia, September 21-23, 2003. Proceedings
Editors	V.I. Gorodetski, V.A. Skormin, L.J. Popyack
Place of Publication	Berlin
Publisher	Springer
Pages	86-99
Number of pages	14
ISBN (Print)	3-540-40797-9
DOIs	https://doi.org/10.1007/978-3-540-45215-7_7
Publication status	Published - Sep 2003
Event	2nd International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security, MMM-ACNS 2003 - St. Petersburg, Russian Federation Duration: 21 Sep 2003 → 23 Sep 2003 Conference number: 2

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer-Verlag
Volume	2776

Workshop

Workshop	2nd International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security, MMM-ACNS 2003
Abbreviated title	MMM-ACNS
Country	Russian Federation
City	St. Petersburg
Period	21/09/03 → 23/09/03

Fingerprint

Keywords

IR-46092
METIS-214032
EWI-814

Cite this

Bistarelli, S., Cervesato, I., Lenzini, G., & Martinelli, F. (2003). Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols. In V. I. Gorodetski, V. A. Skormin, & L. J. Popyack (Eds.), Computer Network Security: Second International Workshop on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2003, St. Petersburg, Russia, September 21-23, 2003. Proceedings (pp. 86-99). (Lecture Notes in Computer Science; Vol. 2776). Berlin: Springer. https://doi.org/10.1007/978-3-540-45215-7_7

Bistarelli, S. ; Cervesato, I. ; Lenzini, Gabriele ; Martinelli, F. / Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols. Computer Network Security: Second International Workshop on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2003, St. Petersburg, Russia, September 21-23, 2003. Proceedings. editor / V.I. Gorodetski ; V.A. Skormin ; L.J. Popyack. Berlin : Springer, 2003. pp. 86-99 (Lecture Notes in Computer Science).

@inproceedings{8c781c76bcba4bafb893aa69ba7d7aa3,

title = "Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols",

abstract = "When formalizing security protocols, different specification languages support very different reasoning methodologies whose results are not directly or easily comparable. Therefore, establishing clear mappings among different frameworks is highly desirable, as it permits various methodologies to cooperate by interpreting theoretical and practical results of one system in another. We examine the non-trivial relationship between two general verification frameworks: multiset rewriting (MSR) and a process algebra (PA) inspired to CCS and the π-calculus. Although defining a simple and general bi-jection between MSR and PA appears difficult, we show that the sublanguages needed to specify a large class of cryptographic protocols (immediate decryption protocols) admits an effective translation that is not only bi-jective and trace-preserving, but also induces a weak form of bisimulation across the two languages. In particular, the correspondence sketched in this abstract permits transferring several important trace-based properties such as secrecy and many forms of authentication",

keywords = "IR-46092, METIS-214032, EWI-814",

author = "S. Bistarelli and I. Cervesato and Gabriele Lenzini and F. Martinelli",

note = "Imported from DIES",

year = "2003",

month = "9",

doi = "10.1007/978-3-540-45215-7_7",

language = "English",

isbn = "3-540-40797-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "86--99",

editor = "V.I. Gorodetski and V.A. Skormin and L.J. Popyack",

booktitle = "Computer Network Security",

}

Bistarelli, S, Cervesato, I, Lenzini, G & Martinelli, F 2003, Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols. in VI Gorodetski, VA Skormin & LJ Popyack (eds), Computer Network Security: Second International Workshop on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2003, St. Petersburg, Russia, September 21-23, 2003. Proceedings. Lecture Notes in Computer Science, vol. 2776, Springer, Berlin, pp. 86-99, 2nd International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security, MMM-ACNS 2003, St. Petersburg, Russian Federation, 21/09/03. https://doi.org/10.1007/978-3-540-45215-7_7

Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols. / Bistarelli, S.; Cervesato, I.; Lenzini, Gabriele; Martinelli, F.

Computer Network Security: Second International Workshop on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2003, St. Petersburg, Russia, September 21-23, 2003. Proceedings. ed. / V.I. Gorodetski; V.A. Skormin; L.J. Popyack. Berlin : Springer, 2003. p. 86-99 (Lecture Notes in Computer Science; Vol. 2776).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols

AU - Bistarelli, S.

AU - Cervesato, I.

AU - Lenzini, Gabriele

AU - Martinelli, F.

N1 - Imported from DIES

PY - 2003/9

Y1 - 2003/9

N2 - When formalizing security protocols, different specification languages support very different reasoning methodologies whose results are not directly or easily comparable. Therefore, establishing clear mappings among different frameworks is highly desirable, as it permits various methodologies to cooperate by interpreting theoretical and practical results of one system in another. We examine the non-trivial relationship between two general verification frameworks: multiset rewriting (MSR) and a process algebra (PA) inspired to CCS and the π-calculus. Although defining a simple and general bi-jection between MSR and PA appears difficult, we show that the sublanguages needed to specify a large class of cryptographic protocols (immediate decryption protocols) admits an effective translation that is not only bi-jective and trace-preserving, but also induces a weak form of bisimulation across the two languages. In particular, the correspondence sketched in this abstract permits transferring several important trace-based properties such as secrecy and many forms of authentication

AB - When formalizing security protocols, different specification languages support very different reasoning methodologies whose results are not directly or easily comparable. Therefore, establishing clear mappings among different frameworks is highly desirable, as it permits various methodologies to cooperate by interpreting theoretical and practical results of one system in another. We examine the non-trivial relationship between two general verification frameworks: multiset rewriting (MSR) and a process algebra (PA) inspired to CCS and the π-calculus. Although defining a simple and general bi-jection between MSR and PA appears difficult, we show that the sublanguages needed to specify a large class of cryptographic protocols (immediate decryption protocols) admits an effective translation that is not only bi-jective and trace-preserving, but also induces a weak form of bisimulation across the two languages. In particular, the correspondence sketched in this abstract permits transferring several important trace-based properties such as secrecy and many forms of authentication

KW - IR-46092

KW - METIS-214032

KW - EWI-814

U2 - 10.1007/978-3-540-45215-7_7

DO - 10.1007/978-3-540-45215-7_7

M3 - Conference contribution

SN - 3-540-40797-9

T3 - Lecture Notes in Computer Science

SP - 86

EP - 99

BT - Computer Network Security

A2 - Gorodetski, V.I.

A2 - Skormin, V.A.

A2 - Popyack, L.J.

PB - Springer

CY - Berlin

ER -

Bistarelli S, Cervesato I, Lenzini G, Martinelli F. Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols. In Gorodetski VI, Skormin VA, Popyack LJ, editors, Computer Network Security: Second International Workshop on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2003, St. Petersburg, Russia, September 21-23, 2003. Proceedings. Berlin: Springer. 2003. p. 86-99. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-45215-7_7

Access to Document

10.1007/978-3-540-45215-7_7

bistarelli02relating
open
Accepted author version, 249 KB