Title :
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
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;
Conference_Titel :
Computer Security Foundations Workshop, 2006. 19th IEEE
Conference_Location :
Venice
Print_ISBN :
0-7695-2615-2
DOI :
10.1109/CSFW.2006.26
