Item Details

Print View

A Method for Examining Cryptographic Protocols

Tjaden, Brett C
Format
Thesis/Dissertation; Online
Author
Tjaden, Brett C
Advisor
Wulf, William
Abstract
In this dissertation we present a powerful, general, extensible, and formal methodology that automatically examines cryptographic protocols. Our approach is to specify a protocol, its assumptions, and a statement of failure in a notation that allows us to give a formal semantic definition of the protocol and its failure conditions. We then use deductive program synthesis to try to automatically modify the protocol so that the failure condition is achieved. If this last step succeeds, we have found a weakness in the protocol and we can then give a step-by-step description of an attack to the user. Given an adequate set of axioms and enough time, our method will find any attack that exists for a given protocol and failure condition. Even if our methodology does not discover a flaw in the amount of time it is given to run, we can make a concrete statement about the minimum length of a constructive proof for any attack that might exist on the protocol (for the given failure condition and axiom set) as a result of its analysis. A preliminary implementation of our methodology has had great success in finding both known and previously unknown flaws in a significant number of published protocols. This system also helped us to discover and demonstrate an important new class of attacks based on the interaction of two or more cryptographic protocols.
Published
University of Virginia, Department of Computer Science, PhD, 1997
Published Date
1997-05-30
Degree
PhD
Rights
All rights reserved (no additional license for public reuse)
Collection
Libra ETD Repository

Availability

Read Online