Multiset Rewriting and Security Protocol Analysis

摘要

The Dolev-Yao model of security protocol analysis may be-formalized using a notation based on multi-set rewriting with existential quantification. This presentation describes the multiset rewriting approach to security protocol analysis, algorithmic upper and lower bounds on specific forms of protocol analysis, and some of the ways this model is useful for formalizing sublte properties of specific protocols.