Carnegie Mellon University
Browse

Relating Strands and Multiset Rewriting for Security Protocol Analysis

Download (242.5 kB)
journal contribution
posted on 1984-01-01, 00:00 authored by Iliano Cervesato, N. Durgin, J. Mitchell, P. Lincoln, A Scedrov
Formal analysis of security protocols is largely based on a set of assumptions commonly referred to as the Dolev-Yao model. Two formalisms that state the basic assumptions of this model are related here: strand spaces and multiset rewriting with existential quantification. Although it is fairly intuitive that these two languages should be equivalent in some way, a number of modifications to each system are required to obtain a meaningful equivalence. We extend the strand formalism with a way of incrementally growing bundles in order to emulate an execution of a protocol with parametric strands. We omit the initialization part of the multiset rewriting setting, which formalizes the choice of initial data, such as shared public or private keys, and which has no counterpart in the strand space setting. The correspondence between the modified formalisms directly relates the intruder theory from the multiset rewriting formalism to the penetrator strands.

History

Publisher Statement

All Rights Reserved

Date

1984-01-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC