Language generation and verification in the NRL protocol analyzer

Author

Meadows, Catherine

Author_Institution

Center for High Assurance Comput. Syst., Naval Res. Lab., Washington, DC, USA

fYear

1996

fDate

10-12 Jun 1996

Firstpage

48

Lastpage

61

Abstract

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

Keywords

access protocols; cryptography; formal languages; formal verification; NRL protocol analyzer; cryptographic protocols; exhaustive search; formal languages; infinite classes of states; language generation; language verification; security properties; Automation; Cryptographic protocols; Cryptography; Failure analysis; Formal languages; Inspection; Laboratories; Plasma welding; Security; State-space methods;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Security Foundations Workshop, 1996. Proceedings., 9th IEEE

Conference_Location

Kenmare

ISSN

1063-6900

Print_ISBN

0-8186-7522-5

Type

conf

DOI

10.1109/CSFW.1996.503690

Filename

503690