Sciweavers

COMPSEC
2010

Provably correct Java implementations of Spi Calculus security protocols specifications

13 years 10 days ago
Provably correct Java implementations of Spi Calculus security protocols specifications
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. Key words: Model-based software development, Correctness preserving code generation, Code verification, Formal methods, Security protocols
Alfredo Pironti, Riccardo Sisto
Added 21 Mar 2011
Updated 21 Mar 2011
Type Journal
Year 2010
Where COMPSEC
Authors Alfredo Pironti, Riccardo Sisto
Comments (0)