ProToc-An Universal Language for Security Protocols Specifications

被引：6
|
作者：
Grosser, A. [1 ]
Kurkowski, M. [2 ]
Piatkowski, J. [1 ]
Szymoniak, S. [1 ]
机构：
[1] Politech Czestochowska, Inst Informat Teoretycznej & Stosowanej, Dabrowskiego 69-73, PL-42200 Czestochowa, Poland
[2] Univ Luxembourg, Comp Sci & Commun Grp, L-1359 Luxembourg, Luxembourg
来源：
SOFT COMPUTING IN COMPUTER AND INFORMATION SCIENCE | 2015年 / 342卷
关键词：
Security protocols; Formal verification; Specification languages; AUTOMATA; NETWORKS; VERIFICATION;
D O I：
10.1007/978-3-319-15147-2_20
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
This paper shows a new language for security protocols specifications. First, we present other specification languages. As far as the use is concerned, Common-Language and its restrictions are presented. Then, CAPSL language is shown and introduced within the AVISPA Project, HLPSL Language. The paper ends with the original approach toward protocol specifications, which is a new ProToc language as well as its grammar and examples of protocols specifications in the language. ProToc has been used as the language of specification for the tool of automatic verification of concurrent systems VerICS.
引用
收藏
页码：237 / 248
页数：12
相关论文
共 50 条
  • [1] Security protocols and specifications
    Abadi, M
    [J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, 1999, 1578 : 1 - 13
  • [2] Intensional specifications of security protocols
    Roscoe, AW
    [J]. 9TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 1996, : 28 - 38
  • [3] The layered games framework for specifications and analysis of security protocols
    Herzberg, Amir
    Yoffe, Igal
    [J]. THEORY OF CRYPTOGRAPHY, 2008, 4948 : 125 - 141
  • [4] On the semantics of Alice&Bob specifications of security protocols
    Caleiro, Carlos
    Vigano, Luca
    Basin, David
    [J]. THEORETICAL COMPUTER SCIENCE, 2006, 367 (1-2) : 88 - 122
  • [5] On Universal Composable Security of Time-Stamping Protocols
    Matsuo, Toshihiko
    Matsuo, Shin'ichiro
    [J]. APPLIED PUBLIC KEY INFRASTRUCTURE, 2005, 128 : 169 - 181
  • [6] A policy-oriented language for expressing security specifications
    Ribeiro, Carlos
    Ferreira, Paulo
    [J]. International Journal of Security and Networks, 2010, 5 (2-3) : 299 - 316
  • [7] 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):
  • [8] Overview security analysis of 3G authentication protocols and technical specifications
    Cao, Chenlei
    Zhang, Ru
    Niu, Xinxin
    Zhou, Linna
    Zhang, Zhentao
    [J]. Qinghua Daxue Xuebao/Journal of Tsinghua University, 2009, 49 (SUPPL. 2): : 2193 - 2199
  • [9] Provably correct Java']Java implementations of Spi Calculus security protocols specifications
    Pironti, Alfredo
    Sisto, Riccardo
    [J]. COMPUTERS & SECURITY, 2010, 29 (03) : 302 - 314
  • [10] Experience report: How to extract security protocols' specifications from C libraries
    Sandoval, Itzel Vazquez
    Lenzini, Gabriele
    [J]. 2018 IEEE 42ND ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC 2018), VOL 2, 2018, : 719 - 724
12345