Accession Number:

ADA374576

Title:

Toward Compositional Analysis of Security Protocols Using Theorem Proving

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

2000-01-01

Pagination or Media Count:

29.0

Abstract:

Complex security protocols require a formal approach to ensure their correctness. The protocols are frequently composed of several smaller, simpler components. We would like to take advantage of the compositional nature of such protocols to split the large verification task into separate and more manageable pieces. Various formalisms have been used successfully for reasoning about large protocol compositions by hand. However hand proofs are prone to error. Automated proof systems can help make the proofs more rigorous. The goal of our work is to develop an automated proof environment for compositional reasoning about systems. This environment would combine the power of compositional reasoning with the rigor of mechanically-checked proofs. The hope is that the resulting system would be useful in verification of security protocols of real-life size and complexity. Toward this goal we present results of a case study in compositional verification of a private communication protocol with the aid of automated proof tool IsabelleIOA.

Subject Categories:

  • Computer Systems Management and Standards

Distribution Statement:

APPROVED FOR PUBLIC RELEASE