loading...
Refuting Security Proofs for Tripartite Key Exchange with Model Checker in Planning Problem Setting
Venice, Italy July 05-July 07
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.2619th IEEE Computer Security Foundatio ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Kim-Kwang Raymond Choo, "Refuting Security Proofs for Tripartite Key Exchange with Model Checker in Planning Problem Setting," Computer Security Foundations Workshop, IEEE, pp. 297-308, 19th IEEE Computer Security Foundations Workshop (CSFW'06), 2006.
 
 
BibTex
x
 
@article{ 10.1109/CSFW.2006.26,
author = {Kim-Kwang Raymond Choo},
title = {Refuting Security Proofs for Tripartite Key Exchange with Model Checker in Planning Problem Setting},
journal ={Computer Security Foundations Workshop, IEEE},
volume = {0},
year = {2006},
issn = {1063-6900},
pages = {297-308},
doi = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.26},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer Security Foundations Workshop, IEEE
TI - Refuting Security Proofs for Tripartite Key Exchange with Model Checker in Planning Problem Setting
SN - 1063-6900
SP297
EP308
A1 - Kim-Kwang Raymond Choo,
PY - 2006
KW - null
VL - 0
JA - Computer Security Foundations Workshop, IEEE
ER -
 
Kim-Kwang Raymond Choo, University of Western Sydney, Australia
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 statespace 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 Gonz?alez 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.
Citation:
Kim-Kwang Raymond Choo, "Refuting Security Proofs for Tripartite Key Exchange with Model Checker in Planning Problem Setting," csfw, pp.297-308, 19th IEEE Computer Security Foundations Workshop (CSFW'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.