Testing equivalence is a quite powerful way of expressing security properties of cryptographic protocols, but its formal verification is a difficult task, because it is based on the universal quantification over contexts. A technique based on state exploration to address this verification problem has been previously presented; it relies on an environment-sensitive labelled transition system (ES-LTS) and on symbolic term representation. This paper shows that such a technique can be enhanced by exploiting symmetries found in the ES-LTS structure. Experimental results show that the proposed enhancement can substantially reduce the size of the ES-LTS and that the technique as a whole compares favorably with respect to related work.

Exploiting Symmetries for Testing Equivalence in the Spi Calculus / CIBRARIO BERTOLOTTI, I.; Durante, L.; Sisto, Riccardo; Valenzano, A.. - STAMPA. - 3299:(2004), pp. 135-149. (Intervento presentato al convegno Second International Conference, ATVA 2004, Taipei, Taiwan, ROC tenutosi a Taipei (TW) nel October 31-November 3, 2004) [10.1007/978-3-540-30476-0_15].

Exploiting Symmetries for Testing Equivalence in the Spi Calculus

CIBRARIO BERTOLOTTI I.;DURANTE L.;SISTO, Riccardo;VALENZANO A.
2004

Abstract

Testing equivalence is a quite powerful way of expressing security properties of cryptographic protocols, but its formal verification is a difficult task, because it is based on the universal quantification over contexts. A technique based on state exploration to address this verification problem has been previously presented; it relies on an environment-sensitive labelled transition system (ES-LTS) and on symbolic term representation. This paper shows that such a technique can be enhanced by exploiting symmetries found in the ES-LTS structure. Experimental results show that the proposed enhancement can substantially reduce the size of the ES-LTS and that the technique as a whole compares favorably with respect to related work.
2004
978-3-540-23610-8
File in questo prodotto:
File Dimensione Formato  
978-3-540-30476-0_15.pdf

non disponibili

Tipologia: 2a Post-print versione editoriale / Version of Record
Licenza: Non Pubblico - Accesso privato/ristretto
Dimensione 235.04 kB
Formato Adobe PDF
235.04 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/1418143