Formal analysis and verification of password protocols
Sreekanth Malladi, Jim Alves-Foss · 2004
Cryptographic protocol analysis has been carried out vigorously over the last decade. Several papers have been published that describe formal analysis techniques to analyze and verify protocols. However, password protocols (which are a special class of cryptographic protocols) remained largely ignored. The issue here is that many analysis and protection techniques for cryptographic protocols are inapplicable for password protocols, since they enable guessing attacks. In this dissertation, we present newly found attacks called multi-protocol guessing attacks on password protocols which are possible in the absence of techniques to prevent protocol-interactions. We explain the development of a new constraint-based analysis tool to automatically find type-flaw and multi-protocol guessing attacks that can exist in the absence of techniques to prevent type-flaws and protocol-interactions. We formally prove that most type-flaw guessing attacks can be prevented by retaining type-tags inside all encryptions except password encryptions. We demonstrate that well-established results on preventing type-flaw attacks cannot prevent attacks arising due to type-flaws in constructed keys and function applications such as hashing and signatures. We also show that the proof methodology adopted itself is flawed since it proves that type-tagging is effective in the presence of any set of inference rules which is untrue. Finally, we prove that a new scheme that we call NUT (Non-Unifiability of Terms) is strong enough to prevent type-flaw attacks even in the presence of constructed keys and function applications. Our proof avoids the flaws in previous attempts by carefully pointing out exactly why and how it is valid only under those sets of inference rules which decompose a set of terms to add subterms of those terms.