Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis

Bistarelli, Stefano and Cervesato, Iliano and Lenzini, Gabriele and Martinelli, Fabio (2005) Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis. Journal of computer security, 13 (1). pp. 3-47. ISSN 0926227X

PDF
Restricted to UT campus only: Request a copy
397Kb

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 bi-jection 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.
Item Type:	Article
Copyright:	© 2005 IOS Press
Research Group:	Distributed and Embedded Systems (DIES)
Link to this item:	http://purl.utwente.nl/publications/48620
Official URL:	http://iospress.metapress.com/link.asp?id=recdra67mg8nlfcj
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 220236