Formal Specification and Verification for S/KEY Against Dictionary Attack
Il-Gon Kim, Choi Jin-Young · Jeongbo gwahaghoe nonmunji. so'peuteuweeo mich eung'yong · 2004
S/KEY system was proposed to guard against intruder's password replay attack. But S/KEY system has vulnerability that if an attacker derive passphrase from his dictionary file, he can acquire one-time password required for user authentication. In this paper, we propose a correct S/KEY system mixed with EKE to solve the problem. Also, we specify a new S/KEY system with Casper and CSP, verify its secrecy and authentication requirements using FDR model checking tool.