Finite Security Analysis of OTRv2

Summary

Off-the-Record messaging is a protocol for enabling secure, authenticated, deniable messaging with perfect forward secrecy, specifically over instant messaging networks. This analysis uncovers vulnerabilities in OTR and discusses appropriate fixes. The analysis is done using the model checker Murphi.

Project report: pdf

Presentation Slides: ppt, pdf

Source Files: download

Last updated: March 26, 2006.