Accession Number:

ADA374554

Title:

Combining Theory Generation and Model Checking for Security Protocol Analysis,

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Report Date:

2000-01-01

Pagination or Media Count:

23.0

Abstract:

This paper reviews two relatively new tools for automated formal analysis of security protocols. One applies the formal methods technique of model checking to the task of protocol analysis, while the other utilizes the method of theory generation. which borrows from both model checking and automated theorem proving. For purposes of comparison. the tools are both applied to a suite of sampIe protocols with known laws. including the protocol used in an earlier study to provide a baseline. We then suggest a heuristic for combining the two approaches to provide a more complete analysis than either approach can provide alone.

Subject Categories:

  • Computer Systems Management and Standards

Distribution Statement:

APPROVED FOR PUBLIC RELEASE