Paper Info
Title
Provably correct Java implementations of Spi Calculus security protocols specifications
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.
Year
DOI
Venue
2010
10.1016/j.cose.2009.08.001
Computers and Security
Keywords
Field
DocType
code verification,correctness preserving code generation,model-based software development,formal methods,security protocols,software development,security protocol,modeling language,code generation,satisfiability,type system,formal method
Model based software development,High level modeling,Programming language,Cryptographic protocol,Computer science,Formal specification,Implementation,Formal methods,Java Modeling Language,Java,Calculus
Journal
Volume
Issue
ISSN
29
3
Computers & Security
Citations 
PageRank 
References 
11
0.51
18
Authors
2
Name
Order
Citations
PageRank
Alfredo Pironti133027.47
Riccardo Sisto255656.79