Verifying and Fixing Password Authentication Protocol

Password authentication protocol (PAP) is widely used in the wireless fidelity point-to-point protocol to authenticate an identity and password for a peer. This paper uses a new knowledge-based framework to verify the PAP protocol and a fixed version. Flaws are found in both the original and the fixed versions. A new enhanced protocol is provided and the security of it is proved. The whole process is implemented in a mechanical reasoning platform, Isabelle. It only takes a few seconds to find flaws in the original and the fixed protocol and to verify that the enhanced version of the PAP protocol is secure