Computing symbolic models for verifying cryptographic protocols

被引：37

作者：

Fiore, M ^{[1
]}

Abadi, M ^{[1
]}

机构：

[1] Univ Cambridge, Comp Lab, Cambridge CB2 3QG, England

来源：

14TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS | 2001年

关键词：

D O I：

10.1109/CSFW.2001.930144

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We consider the problem of automatically verifying infinite-state cryptographic protocols. Specifically, we present an algorithm that given a finite, process describing a protocol in a hostile environment (trying to force the system into a "bad" state) computes a model of traces on which security properties can be checked. Because of unbounded inputs from the environment, even finite processes have an infinite set of traces; the main focus of our approach is the reduction of this infinite set to a finite set by a symbolic analysis of the knowledge of the environment. Our algorithm is sound (and we conjecture complete) for protocols with shared-key encryption/dectyption, that use arbitrary messages as keys; further it. is complete in the common and important case in which the cryptographic, keys are messages of bounded size.

引用

页码：160 / 173

页数：14

共 25 条

[1] A calculus for cryptographic protocols: The spi calculus [J].

Abadi, M ;

Gordon, AD .

INFORMATION AND COMPUTATION, 1999, 148 (01) :1-70

[2]

Abadi M, 2000, NATO ADV SCI I F-COM, V175, P39

[3]

Amadio R., 2000, LECT NOTES COMPUTER, V1877, P380

[4]

AMADIO R, 2001, 4147 INRIA

[5]

[Anonymous], 1996, LNCS

[6]

[Anonymous], 1985, INT SERIES COMP SCI

[7]

BOREALE M, 2000, UNPUB SYMBOLIC ANAL

[8]

BOREALE M, 2001, IN PRESS P ICALP

[9]

CLAKRE E, 1998, P IFIP WORK C PROGR

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

DOLEV, D ;

YAO, AC .

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

← 1 2 3 →