Item Details

A Formal Semantics for Evaluating Cryptographic Protocols

Yasinsac, Alec F
Format
Thesis/Dissertation; Online
Author
Yasinsac, Alec F
Advisor
Wulf, William
Abstract
Secure communication is largely dependent on effective application of cryptography. While cryptographic methods have been investigated to ensure confidence in the security of the encryption algorithm, many cryptographic schemes are vulnerable to attack because the protocols used to implement communication in a cryptographic environment do not meet their intended goals. Cryptographic protocols, like software, are very difficult to verify. Recent research is aimed at finding methods of verifying cryptographic protocols. Though no method has achieved widespread acceptance and use, the most prevalent class of cryptographic protocol evaluation techniques is based on application of epistemic logical systems to reason about the protocols. In this dissertation we present a methodology for verifying cryptographic protocols based on the classical program verification technique of Weakest Precondition reasoning [DIJK76] and a set of tools to automate application of the method. The methodology solves many problems of existing methods by formalizing the meaning of the messages in a protocol session and by including message sequencing in the protocol definition. The proposed method can also be combined with logical methods to construct a more thorough cryptographic protocol evaluation technique.
Date Received
20111206
Published
University of Virginia, Department of Computer Science, PHD (Doctor of Philosophy), 1996
Published Date
1996-01-01
Degree
PHD (Doctor of Philosophy)
Collection
Libra ETD Repository
Logo for In CopyrightIn Copyright

Availability

Read Online