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