Provably correct Java']Java implementations of Spi Calculus security protocols specifications

被引：11
|
作者：
Pironti, Alfredo [1 ]
Sisto, Riccardo [1 ]
机构：
[1] Politecn Torino, Dip Automat & Informat, I-10129 Turin, Italy
来源：
COMPUTERS & SECURITY | 2010年 / 29卷 / 03期
关键词：
Model-based software development; Correctness preserving code generation; Code verification; Formal methods; Security protocols; VERIFICATION; REFINEMENT;
D O I：
10.1016/j.cose.2009.08.001
中图分类号：
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 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 (C) 2009 Elsevier Ltd All rights reserved
引用
收藏
页码：302 / 314
页数：13
相关论文
共 17 条
  • [1] 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
    Comput Secur, 3 (302-314):
  • [2] Formally Sound Refinement of Spi Calculus Protocol Specifications into Java']Java Code
    Pironti, Alfredo
    Sisto, Riccardo
    11TH IEEE HIGH ASSURANCE SYSTEMS ENGINEERING SYMPOSIUM, PROCEEDINGS, 2008, : 241 - 250
  • [3] Testing Java']Java implementations of algebraic specifications
    Nunes, Isabel
    Luis, Filipe
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (111): : 35 - 50
  • [4] Formally sound implementations of security protocols with Java']JavaSPI
    Sisto, Riccardo
    Copet, Piergiuseppe Bettassa
    Avalle, Matteo
    Pironti, Alfredo
    FORMAL ASPECTS OF COMPUTING, 2018, 30 (02) : 279 - 317
  • [5] Defining the Java']Java Virtual Machine as platform for provably correct Java']Java compilation
    Börger, E
    Schulte, W
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 1998, 1998, 1450 : 17 - 35
  • [6] A Provably Correct Stackless Intermediate Representation for Java']Java Bytecode
    Demange, Delphine
    Jensen, Thomas
    Pichardie, David
    PROGRAMMING LANGUAGES AND SYSTEMS, 2010, 6461 : 97 - +
  • [7] Spi2Java']Java: Automatic cryptographic protocol Java']Java code generation from spi calculus
    Pozza, D
    Sisto, R
    Durante, L
    18TH INTERNATIONAL CONFERENCE ON ADVANCED INFORMATION NETWORKING AND APPLICATIONS, VOL 1 (LONG PAPERS), PROCEEDINGS, 2004, : 400 - 405
  • [8] From finite state machines to provably correct Java']Java card applets
    Hubbers, E
    Oostdijk, M
    Poll, E
    SECURITY AND PRIVACY IN THE AGE OF UNCERTAINTY, 2003, 122 : 465 - 470
  • [9] Provably correct inline monitoring for multithreaded Java']Java-like programs
    Dam, Mads
    Jacobs, Bart
    Lundblad, Andreas
    Piessens, Frank
    JOURNAL OF COMPUTER SECURITY, 2010, 18 (01) : 37 - 59
  • [10] A 5-step hunt for faults in Java']Java implementations of algebraic specifications
    Nunes, Isabel
    Luis, Filipe
    IEEE SIXTH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION WORKSHOPS (ICSTW 2013), 2013, : 168 - 177
12