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 proceedingConference contributionAcademicpeer-review

    2 Citations (Scopus)
    40 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 languageEnglish
    Title of host publicationComputer Network Security
    Subtitle of host publicationSecond International Workshop on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2003, St. Petersburg, Russia, September 21-23, 2003. Proceedings
    EditorsV.I. Gorodetski, V.A. Skormin, L.J. Popyack
    Place of PublicationBerlin
    PublisherSpringer
    Pages86-99
    Number of pages14
    ISBN (Print)3-540-40797-9
    DOIs
    Publication statusPublished - Sep 2003
    Event2nd International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security, MMM-ACNS 2003 - St. Petersburg, Russian Federation
    Duration: 21 Sep 200323 Sep 2003
    Conference number: 2

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer-Verlag
    Volume2776

    Workshop

    Workshop2nd International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security, MMM-ACNS 2003
    Abbreviated titleMMM-ACNS
    CountryRussian Federation
    CitySt. Petersburg
    Period21/09/0323/09/03

    Fingerprint

    Algebra
    Network protocols
    Specification languages
    Authentication

    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 proceedingConference contributionAcademicpeer-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