Refuting security proofs for tripartite key exchange with model checker in planning problem setting

Author

Choo, Kim-Kwang Raymond

Author_Institution

Sch. of Comput. & Inf. Technol., Western Sydney Univ., NSW

fYear

0

fDate

0-0 0

Lastpage

308

Abstract

We encode a simplified version of the Canetti and Krawczyk (2001) formalism using asynchronous product automata (APA). We then use a model checker tool, simple homomorphism verification tool (SHVT), to perform state-space analysis on our automata in the setting of planning problem. As a case study, we revisit two tripartite key exchange protocols of Hitchcock, Boyd, and Gonzalez Nieto (2004), which carry claimed security proofs in the Canetti and Krawczyk (2001) model. We refute their proofs of security by pointing out previously unpublished flaws in the protocols using SHVT. We then point out corresponding flaws in the refuted proofs

Keywords

formal specification; security of data; Canetti-Krawczyk formalism; asynchronous product automata; model checker tool; planning problem; security proofs; simple homomorphism verification tool; state-space analysis; tripartite key exchange protocols; Automata; Computational complexity; Computer errors; Computer security; Cryptographic protocols; Information security; Intelligent systems; Laboratories; Public key cryptography; Technology planning;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Security Foundations Workshop, 2006. 19th IEEE

Conference_Location

Venice

ISSN

1063-6900

Print_ISBN

0-7695-2615-2

Type

conf

DOI

10.1109/CSFW.2006.26

Filename

1648726