PORTO @ 
Publications Open Repository TOrino
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishSpi 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.
http://hdl.handle.net/11583/2284514| Titolo: | Provably correct Java implementations of Spi Calculus security protocols specifications |
| Autori: | |
| Data di pubblicazione: | 2010 |
| Rivista: | |
| 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. |
| Digital Object Identifier (DOI): | 10.1016/j.cose.2009.08.001 |
| Appare nelle tipologie: | 1.1 Articolo in rivista |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| 1-s2.0-S0167404809000832-main.pdf | 4. Altro | Non Pubblico - Accesso privato/ristretto | Administrator Richiedi una copia | |
| cose2009_author_postprint.pdf | 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 | 2. Post-print | PUBBLICO - Tutti i diritti riservati | Visibile a tuttiVisualizza/Apri |
Copyright © 2018