Ping-pong protocols as prefix grammars: Modelling and verification via program transformation

被引：2

作者：

Nepeivoda, Antonina ^{[1
]}

机构：

[1] RAS, Program Syst Inst, Pereslavl Zalesskii, Russia

来源：

JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING | 2016年 / 85卷 / 05期

基金：

俄罗斯基础研究基金会;

关键词：

Prefix grammar; Ping-pong protocol; Program transformation; Supercompilation; Dolev-Yao intruder model; Verification; SECURITY;

D O I：

10.1016/j.jlamp.2016.06.001

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper presents a technique to model ping-pong protocols by prefix grammars in such a way that the security of the protocol models becomes decidable by a general-purpose program transformation tool with unfolding. The presented approach not only decides whether a protocol model is insecure but also builds a set of possible attack models explicitly. (C) 2016 Elsevier Inc. All rights reserved.

引用

页码：782 / 804

页数：23

共 21 条

[1]

Abadi M., 1998, Nordic Journal of Computing, V5, P267

[2]

Ahmed A., 2013, EPIC SERIES, V16, P16, DOI DOI 10.29007/GPSH

[3] ON THE SECURITY OF PING-PONG PROTOCOLS [J].

DOLEV, D ;

EVEN, S ;

KARP, RM .

INFORMATION AND CONTROL, 1982, 55 (1-3) :57-68

[4] ON THE SECURITY OF PUBLIC KEY PROTOCOLS [J].

DOLEV, D ;

YAO, AC .

IEEE TRANSACTIONS ON INFORMATION THEORY, 1983, 29 (02) :198-208

[5]

Even S., 1985, TECHNICAL REPORT

[6]

Hamilton G. W., 2012, DISTILLATION LABELLE, P15, DOI [10.1145/2103746.2103753, DOI 10.1145/2103746.2103753]

[7]

Klimov Andrei V., 2012, Perspectives of System Informatics. 8th International Ershov Informatics Conference, PSI 2011. Revised Selected Papers, P193, DOI 10.1007/978-3-642-29709-0_18

[8]

Klyuchnikov I., 2014, 4 INT VAL TURCH WORK, P161

[9]

Lisitsa A., 2014, EPIC SER, V28, P52

[10] On One Application of Computations with Oracle [J].

Lisitsa, A. P. ;

Nemytykh, A. P. .

PROGRAMMING AND COMPUTER SOFTWARE, 2010, 36 (03) :157-165

← 1 2 3 →