Spi Calculus is an untyped high level modeling language for security protocols, used for formal protocols specification and verification. In this paper, a type system for the Spi Calculus and a translation function are formally defined, in order to formalize the refinement of a Spi Calculus specification into a Java implementation. The Java implementation generated by the translation function uses a custom Java library. Formal conditions on such library are stated, so that, if the library implementation code satisfies such conditions, then the generated Java implementation correctly simulates the Spi Calculus specification. A verified implementation of part of the custom library is further presented.

Provably correct Java implementations of Spi Calculus security protocols specifications / Pironti, Alfredo; Sisto, Riccardo. - In: COMPUTERS & SECURITY. - ISSN 0167-4048. - STAMPA. - 29(3):3(2010), pp. 302-314. [10.1016/j.cose.2009.08.001]

Provably correct Java implementations of Spi Calculus security protocols specifications

PIRONTI, ALFREDO;SISTO, Riccardo
2010

Abstract

Spi Calculus is an untyped high level modeling language for security protocols, used for formal protocols specification and verification. In this paper, a type system for the Spi Calculus and a translation function are formally defined, in order to formalize the refinement of a Spi Calculus specification into a Java implementation. The Java implementation generated by the translation function uses a custom Java library. Formal conditions on such library are stated, so that, if the library implementation code satisfies such conditions, then the generated Java implementation correctly simulates the Spi Calculus specification. A verified implementation of part of the custom library is further presented.
File in questo prodotto:
File Dimensione Formato  
cose2009_author_postprint.pdf

accesso aperto

Descrizione: Post-Print Author's version of an article published in Journal of Systems and Software. The final published version is available at http://dx.doi.org/10.1016/j.cose.2009.08.001
Tipologia: 2. Post-print / Author's Accepted Manuscript
Licenza: PUBBLICO - Tutti i diritti riservati
Dimensione 217.66 kB
Formato Adobe PDF
217.66 kB Adobe PDF Visualizza/Apri
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/2284514
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo