When formalizing security prtocols, different specification languages support very different reasoning methodologies, whose results are not directly or easily comparable. Therefore, establishingclear relationships among different frameworks is highly desirable, as it permits various methodologies to cooperate by interpreting thoretical and practical results of one system in another. In this paper, we examine the nontrivial relationship between two general verification frameworks: multiset rewriting (MSR) and a process algebra (PA) inspired to the CCS and the pi-calculus. We present two separate mappings, one from MSR to PA and the other from PA to MSR. Although defining a simple and general bijection between MSR and PA appears difficult, we show that in the specific context of cryptographic protocols they do admit effective translations that preserve traces.
Relating Process Algebras and Multiset Rewriting for Security Protocol Analysis
Bistarelli S;Martinelli F
2003
Abstract
When formalizing security prtocols, different specification languages support very different reasoning methodologies, whose results are not directly or easily comparable. Therefore, establishingclear relationships among different frameworks is highly desirable, as it permits various methodologies to cooperate by interpreting thoretical and practical results of one system in another. In this paper, we examine the nontrivial relationship between two general verification frameworks: multiset rewriting (MSR) and a process algebra (PA) inspired to the CCS and the pi-calculus. We present two separate mappings, one from MSR to PA and the other from PA to MSR. Although defining a simple and general bijection between MSR and PA appears difficult, we show that in the specific context of cryptographic protocols they do admit effective translations that preserve traces.File | Dimensione | Formato | |
---|---|---|---|
prod_91771-doc_123686.pdf
solo utenti autorizzati
Descrizione: Relating Process Algebras and Multiset Rewriting for Security Protocol Analysis
Tipologia:
Versione Editoriale (PDF)
Dimensione
227.26 kB
Formato
Adobe PDF
|
227.26 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.