Formally Sound Refinement of Spi Calculus Protocol Specifications into Java Code

摘要：

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. Since the generated Java implementation uses a custom Java library, formal conditions on the custom Java library are also stated, so that, if the library implementation code satisfies such conditions, then the generated Java implementation correctly simulates the Spi Calculus specification.

关键词： Model-based software development Correctness preserving code generation Formal methods Security protocols

作者: Alfredo Pironti Riccardo Sisto

作者单位: Politecnico di Torino Dip.di Automatica e Informatica c.so Duca degli Abruzzi 24, I-10129 Torino (Italy)

会议类型: 国际会议

会议名称: 11th IEEE High Assurance Systems Engineering Symposium(HASE 2008)(第十一届IEEE高可信系统工程国际研讨会)

会议地点: 南京

会议语种:英文

页码: 241-250

在线出版日期: 2008-12-03（万方平台首次上网日期，不代表论文的发表时间）