loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
14th IEEE Computer Security Foundations Workshop (CSFW'01)
Computing Symbolic Models for Verifying Cryptographic Protocols
Cape Breton, Novia Scotia, Canada
June 11-June 13
ISBN: 0-7695-1146-5
ASCII Text
x 
 
Marcelo Fiore, MartÍn Abadi, "Computing Symbolic Models for Verifying Cryptographic Protocols," Computer Security Foundations Workshop, IEEE, pp. 0160, 14th IEEE Computer Security Foundations Workshop (CSFW'01), 2001.
 
 
BibTex
x
 
@article{ 10.1109/CSFW.2001.930144,
author = {Marcelo Fiore and MartÍn Abadi},
title = {Computing Symbolic Models for Verifying Cryptographic Protocols},
journal ={Computer Security Foundations Workshop, IEEE},
volume = {0},
year = {2001},
isbn = {0-7695-1146-5},
pages = {0160},
doi = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2001.930144},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer Security Foundations Workshop, IEEE
TI - Computing Symbolic Models for Verifying Cryptographic Protocols
SN - 0-7695-1146-5
SP
EP
A1 - Marcelo Fiore,
A1 - MartÍn Abadi,
PY - 2001
VL - 0
JA - Computer Security Foundations Workshop, IEEE
ER -
 
Marcelo Fiore, University of Cambridge
MartÍn Abadi, Lucent Technologies
Abstract: 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/decryption 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.
Citation:
Marcelo Fiore, MartÍn Abadi, "Computing Symbolic Models for Verifying Cryptographic Protocols," csfw, pp.0160, 14th IEEE Computer Security Foundations Workshop (CSFW'01), 2001
Usage of this product signifies your acceptance of the Terms of Use.