|
Second USENIX Workshop on Electronic Commerce
Verifying Cryptographic Protocols for Electronic Commerce
Dr. Randall W. Lichota, Hughes Technical Services Company
Dr. Grace L. Hammonds, AGCS, Inc.
Dr. Stephen H. Brackin, Arca Systems, Inc.
Abstract
This paper describes the Convince toolset for detecting common errors
in cryptographic protocols, protocols of the sort used in electronic
commerce. We describe using Convince to analyze confidentiality,
authentication, and key distribution in a recently developed protocol
proposed for incorporation into a network bill-payment system, a
public-key version of the Kerberos authentication protocol. Convince
incorporates a "belief logic" formalism into a theorem-proving
environment that automatically proves whether a protocol can meet its
goals. Convince allows an analyst to model a protocol using a tool
originally designed for Computer-Aided Software Engineering (CASE).
View the full text of this paper in
ASCII (44,443 Bytes) and
POSTSCRIPT (790,719 Bytes) form.
To Become a USENIX Member, please see our
Membership Information.
|
Need help? Use our Contacts page.
Conference Index