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