Abstract
| 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 | |
| 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
}
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 -