AVISPA Test Code for the Mobile Password Authentication (MP-Auth) Protocol

MP-Auth has been analyzed using the Automated Validation of Internet Security Protocols and Applications (AVISPA) formal analysis tool (many thanks to Paul H. Drielsma of ETH-Zurich). Test code is available here (for comments on the code, see the TechReport). The AVISPA web interface can be used to test this model. No attacks have been found against MP-Auth using AVISPA.