loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Ninth IEEE Computer Security Foundations Workshop
Language generation and verification in the NRL protocol analyzer
Dromquinna Manor, Kenmare, County Kerry, Ireland
March 10-March 12
ISBN: 0-8186-7522-5
ASCII Text
x 
 
C. Meadows, "Language generation and verification in the NRL protocol analyzer," Computer Security Foundations Workshop, IEEE, pp. 48, Ninth IEEE Computer Security Foundations Workshop, 1996.
 
 
BibTex
x
 
@article{ 10.1109/CSFW.1996.503690,
author = {C. Meadows},
title = {Language generation and verification in the NRL protocol analyzer},
journal ={Computer Security Foundations Workshop, IEEE},
volume = {0},
year = {1996},
issn = {1063-6900},
pages = {48},
doi = {http://doi.ieeecomputersociety.org/10.1109/CSFW.1996.503690},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer Security Foundations Workshop, IEEE
TI - Language generation and verification in the NRL protocol analyzer
SN - 1063-6900
SP
EP
A1 - C. Meadows,
PY - 1996
KW - access protocols; cryptography; formal languages; formal verification; language generation; language verification; NRL protocol analyzer; security properties; cryptographic protocols; infinite classes of states; exhaustive search; formal languages
VL - 0
JA - Computer Security Foundations Workshop, IEEE
ER -
 
C. Meadows, Center for High Assurance Comput. Syst., Naval Res. Lab., Washington, DC, USA
The NRL protocol analyzer is a tool for proving security properties of cryptographic protocols, and for finding flaws if they exist. It is used by having the user first prove a number of lemmas stating that infinite classes of states are unreachable, and then performing an exhaustive search on the remaining state space. One main source of difficulty in using the tool is in generating the lemmas that are to be proved. In this paper we show how we have made the test easier by automating the generation of lemmas involving the use of formal languages.
Index Terms:
access protocols; cryptography; formal languages; formal verification; language generation; language verification; NRL protocol analyzer; security properties; cryptographic protocols; infinite classes of states; exhaustive search; formal languages
Citation:
C. Meadows, "Language generation and verification in the NRL protocol analyzer," csfw, pp.48, Ninth IEEE Computer Security Foundations Workshop, 1996
Usage of this product signifies your acceptance of the Terms of Use.