Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication
The authors formally analyze the family of entity authentication proto-cols defined by the ISO/IEC 9798 standard and find numerous weaknesses, both old and new, including some that violate even the most basic authentication guarantees. They analyze the cause of these weaknesses, propose repaired versions of the protocols, and provide automated, machine-checked proofs of the correctness of the resulting protocols. From an engineering perspective, they propose two design principles for security protocols that suffice to prevent all the weaknesses. Moreover, they show how modern verification tools can be used for falsification and certified verification of security standards.