Title :
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
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;
Conference_Titel :
Computer Security Foundations Workshop, 2000. CSFW-13. Proceedings. 13th IEEE
Conference_Location :
Cambridge
Print_ISBN :
0-7695-0671-2
DOI :
10.1109/CSFW.2000.856927
