AVISPA Test Code for the Instant Messaging and Key Exchange (IMKE) Protocol

IMKE 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 with comments are available in IMKE-simple (partial model) and IMKE (complete model). The AVISPA web interface can be used to test these models. No attacks have been found against IMKE using AVISPA.