Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis

Stefano Bistarelli, Iliano Cervesato, Gabriele Lenzini, Fabio Martinelli

    Research output: Book/ReportReportProfessional

    13 Citations (Scopus)
    44 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 into another. In this paper, we examine the 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 bijection between MSR and PA appears difficult, we show that the sublanguages needed to specify cryptographic protocols admit an effective translation that is not only trace-preserving, but also induces a correspondence relation between the two languages. In particular, the correspondence sketched in this paper permits transferring several important trace-based properties such as secrecy and many forms of authentication.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherDistributed and Embedded Security (DIES)
    Number of pages42
    Publication statusPublished - Dec 2005

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematica and Information Technology (CTIT)
    No.TR-CTIT-05-61
    ISSN (Print)1381-3625

    Keywords

    • EWI-5718
    • IR-57048
    • METIS-248096

    Cite this

    Bistarelli, S., Cervesato, I., Lenzini, G., & Martinelli, F. (2005). Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis. (CTIT Technical Report Series; No. TR-CTIT-05-61). Enschede: Distributed and Embedded Security (DIES).
    Bistarelli, Stefano ; Cervesato, Iliano ; Lenzini, Gabriele ; Martinelli, Fabio. / Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis. Enschede : Distributed and Embedded Security (DIES), 2005. 42 p. (CTIT Technical Report Series; TR-CTIT-05-61).
    @book{974e4ce697ea4ce2b8483649762ce27e,
    title = "Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis",
    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 into another. In this paper, we examine the 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 bijection between MSR and PA appears difficult, we show that the sublanguages needed to specify cryptographic protocols admit an effective translation that is not only trace-preserving, but also induces a correspondence relation between the two languages. In particular, the correspondence sketched in this paper permits transferring several important trace-based properties such as secrecy and many forms of authentication.",
    keywords = "EWI-5718, IR-57048, METIS-248096",
    author = "Stefano Bistarelli and Iliano Cervesato and Gabriele Lenzini and Fabio Martinelli",
    note = "Imported from CTIT",
    year = "2005",
    month = "12",
    language = "Undefined",
    series = "CTIT Technical Report Series",
    publisher = "Distributed and Embedded Security (DIES)",
    number = "TR-CTIT-05-61",

    }

    Bistarelli, S, Cervesato, I, Lenzini, G & Martinelli, F 2005, Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis. CTIT Technical Report Series, no. TR-CTIT-05-61, Distributed and Embedded Security (DIES), Enschede.

    Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis. / Bistarelli, Stefano; Cervesato, Iliano; Lenzini, Gabriele; Martinelli, Fabio.

    Enschede : Distributed and Embedded Security (DIES), 2005. 42 p. (CTIT Technical Report Series; No. TR-CTIT-05-61).

    Research output: Book/ReportReportProfessional

    TY - BOOK

    T1 - Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis

    AU - Bistarelli, Stefano

    AU - Cervesato, Iliano

    AU - Lenzini, Gabriele

    AU - Martinelli, Fabio

    N1 - Imported from CTIT

    PY - 2005/12

    Y1 - 2005/12

    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 into another. In this paper, we examine the 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 bijection between MSR and PA appears difficult, we show that the sublanguages needed to specify cryptographic protocols admit an effective translation that is not only trace-preserving, but also induces a correspondence relation between the two languages. In particular, the correspondence sketched in this paper 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 into another. In this paper, we examine the 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 bijection between MSR and PA appears difficult, we show that the sublanguages needed to specify cryptographic protocols admit an effective translation that is not only trace-preserving, but also induces a correspondence relation between the two languages. In particular, the correspondence sketched in this paper permits transferring several important trace-based properties such as secrecy and many forms of authentication.

    KW - EWI-5718

    KW - IR-57048

    KW - METIS-248096

    M3 - Report

    T3 - CTIT Technical Report Series

    BT - Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis

    PB - Distributed and Embedded Security (DIES)

    CY - Enschede

    ER -

    Bistarelli S, Cervesato I, Lenzini G, Martinelli F. Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis. Enschede: Distributed and Embedded Security (DIES), 2005. 42 p. (CTIT Technical Report Series; TR-CTIT-05-61).