Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols

Bistarelli, S. and Cervesato, I. and Lenzini, G. and Martinelli, F. (2003) Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols. In: 2nd Int. Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security.

Preview

PDF
249Kb

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 in another. We examine the non-trivial 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 a large class of cryptographic protocols (immediate decryption protocols) admits an effective translation that is not only bi-jective and trace-preserving, but also induces a weak form of bisimulation across the two languages. In particular, the correspondence sketched in this abstract permits transferring several important trace-based properties such as secrecy and many forms of authentication
Item Type:	Conference or Workshop Item
Copyright:	©2003 Springer
Research Group:	Distributed and Embedded Systems (DIES)
Link to this item:	http://purl.utwente.nl/publications/46092
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 214032