Istituto di Scienza e Tecnologie dell'Informazione     
Bistarelli S., Cervesato I., Lenzini G., Martinelli F. Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols. In: Second International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security (MMM-ACNS 2003) (St. Petersburg, Russia, 20-24 September, 2003). Proceedings, pp. 86 - 99. V.I. Gorodetski, V.A. Skormin and L.J. Popyack (eds.). (Lecture Notes in Computer Science, vol. 2776). Springer-Verlag, 2003.
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. In this paper, we examine the non-trivial relationship between two general verification frameworks: multiset rewriting ($MSR$) and a process algebra ($PA$) inspired to CCS and the $pi$-calculus. Although defining a simple and general bijection 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 bijective 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.
URL: http://matrix.iei.pi.cnr.it/~lenzini/papers/mmm03.ps
Subject Security Protocols
Multiset Rewriting
Process Algebras
F.3.1 Specifying and Verifying and Reasoning about Programms

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional