C3PO: a tool for automatic sound cryptographic protocol analysis

Author

Dekker, Anthony H.

Author_Institution

Defence Sci. & Technol Organ., Australian Nat. Univ., Manuka, ACT, Australia

fYear

2000

fDate

2000

Firstpage

77

Lastpage

87

Abstract

We present an improved logic for analysing authentication properties of cryptographic protocols, based on the SVO logic of Syverson and van Oorschot (1994). Such logics are useful in electronic commerce, among other areas. We have constructed this logic in order to simplify automation, and we describe an implementation using the Isabelle theorem-proving system, and a GUI tool based on this implementation. The tool is typically operated by opening a list of propositions intended to be true, and clicking one button. Since the rules form a clean framework, the logic is easily extensible. We also present in detail a proof of soundness, using Kripke possible-worlds semantics

Keywords

cryptography; electronic commerce; formal logic; formal verification; message authentication; protocols; software tools; GUI tool; Isabelle theorem-proving system; Kripke possible-worlds semantics; SVO logic; authentication properties; automatic sound cryptographic protocol analysis; cryptographic protocols; electronic commerce; proof of soundness; Authentication; Body sensor networks; Computer science; Cryptographic protocols; Cryptography; Design automation; Electronic commerce; Electronic mail; Graphical user interfaces; Logic;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Security Foundations Workshop, 2000. CSFW-13. Proceedings. 13th IEEE

Conference_Location

Cambridge

ISSN

1063-6900

Print_ISBN

0-7695-0671-2

Type

conf

DOI

10.1109/CSFW.2000.856927

Filename

856927