[OTR-dev] Looking for the proof of security of original OTR protocol

[George Kadianakis]

> Hi OTRers,
>
> This is vmon from Internet (eQualit.ie/Cryptocat/Tor etc) ;).
>
> I am curious to know if there has been any publication or attempt to
> proof the security of the OTR protocol in terms of "provable security",
> reduction of OTR security to its primitives or even merely a precise
> mathematical definition and modeling of the various adversaries,
> addressed in the design of the protocol (Confidentiality, Authenticity,
> forward  secrecy and deniablitiy) and their computational resources.
>
> I would really appreciate if someone points me to such works. That
> would be a great help and a grand favor :)
>
>

I'm aware of two works that attempt to formalize and prove the security of
OTR:

- Mario Di Raimondo, Rosario Gennaro, and Hugo Krawczyk: "Secure
Off-the-Record Messaging"

- Joseph Bonneau , Andrew Morrison: "Finite-State Security Analysis of OTR
Version 2"