Check out the new USENIX Web site.

Home About USENIX Events Membership Publications Students
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.


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.

Last changed: 15 April 2002 aw
Conference Index