Formally Sound Refinement of Spi Calculus Protocol Specifications into Java']Java Code

被引：1
|
作者：
Pironti, Alfredo [1 ]
Sisto, Riccardo [1 ]
机构：
[1] Politecn Torino, Dipartimento Automat & Informat, I-10129 Turin, Italy
来源：
11TH IEEE HIGH ASSURANCE SYSTEMS ENGINEERING SYMPOSIUM, PROCEEDINGS | 2008年
关键词：
Model-based software development; Correctness preserving code generation; Formal methods; Security protocols;
D O I：
10.1109/HASE.2008.27
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
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.
引用
收藏
页码：241 / 250
页数：10
相关论文
共 14 条
  • [1] Spi2Java']Java: Automatic cryptographic protocol Java']Java code generation from spi calculus
    Pozza, D
    Sisto, R
    Durante, L
    [J]. 18TH INTERNATIONAL CONFERENCE ON ADVANCED INFORMATION NETWORKING AND APPLICATIONS, VOL 1 (LONG PAPERS), PROCEEDINGS, 2004, : 400 - 405
  • [2] Provably correct Java']Java implementations of Spi Calculus security protocols specifications
    Pironti, Alfredo
    Sisto, Riccardo
    [J]. COMPUTERS & SECURITY, 2010, 29 (03) : 302 - 314
  • [3] A formally verified calculus for full Java']Java card
    Stenzel, K
    [J]. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, 2004, 3116 : 491 - 505
  • [4] Provably correct Java implementations of Spi Calculus security protocols specifications
    Politecnico di Torino, Dip. di Automatica e Informatica, c.so Duca degli Abruzzi 24, I-10129 Torino, Italy
    [J]. Comput Secur, 3 (302-314):
  • [5] Implementing a formally verifiable security protocol in Java']Java Card
    Hubbers, E
    Oostdijk, M
    Poll, E
    [J]. SECURITY IN PERVASIVE COMPUTING, 2004, 2802 : 213 - 226
  • [6] From Lyee-calculus to Java']Java code
    Ktari, B
    Mejri, M
    Fujita, H
    [J]. NEW TRENDS IN SOFTWARE METHODOLOGIES, TOOLS AND TECHNIQUES, 2004, 111 : 283 - 300
  • [7] Java']Java card code generation from B specifications
    Tatibouët, B
    Requet, A
    Voisinet, JC
    Hammad, A
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2003, 2885 : 306 - 318
  • [8] An automatic approach to transform CafeOBJ specifications to Java']Java template code
    Doungsa-ard, C
    Suwannasart, T
    [J]. SERP'03: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING RESEARCH AND PRACTICE, VOLS 1 AND 2, 2003, : 171 - 176
  • [9] Formally sound implementations of security protocols with Java']JavaSPI
    Sisto, Riccardo
    Copet, Piergiuseppe Bettassa
    Avalle, Matteo
    Pironti, Alfredo
    [J]. FORMAL ASPECTS OF COMPUTING, 2018, 30 (02) : 279 - 317
  • [10] Feature Featherweight Java']Java: A Calculus for Feature-Oriented Programming and Stepwise Refinement
    Apel, Sven
    Kaestner, Christian
    Lengauer, Christian
    [J]. GPCE'08: PROCEEDINGS OF THE ACM SIGPLAN SEVENTH INTERNATIONAL CONFERENCE ON GENERATIVE PROGRAMMING AND COMPONENT ENGINEERING, 2008, : 101 - 111
12