[OTR-dev] Protocol Analysis

[Ian Goldberg]

On Thu, Jan 19, 2006 at 12:55:44PM -0800, Andrew S. Morrison wrote:
> Myself and a partner are considering doing a formal security analysis of
> OTR over the next 3 months as part of a security protocols course at
> Stanford University.
> 
> We will be modeling the system and using a formal analysis system such as
> Murphi or PRISM to analyze the OTR protocol. Does anyone on the list know
> if such a thing has been done previously? If so, are there any papers from
> the analysis that I could read? Also, would anyone be willing to talk with
> me for a few minutes about OTR and some of the design decisions?

Very cool.  There was a paper in the last WPES analysing the previous
OTR protocol, which is what caused the protocol to change.  ;-)  It
wasn't a formal analysis, though.

I'd certainly be happy to talk with you; email <otr at cypherpunks.ca>,
and we can do it off-list.  [This week's a little busy for me, though.]

   - Ian