A Comparison between Strand Spaces and Multiset Rewriting for Security Protocol Analysis

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 [FHG98] and multiset rewriting with existential quantification [CDL 99,DLMS99]. Strand spaces provide a simple and economical approach to state-based analysis of completed protocol runs by emphasizing causal interactions among protocol participants