[OTR-dev] Finite-State Analysis of OTR V2

Andrew S. Morrison asm at CS.Stanford.EDU
Tue Mar 21 17:32:20 EST 2006

We've completed our finite-state analysis of OTR V2. The paper outlining
our results, including attacks we've discovered and potential solutions
may be downloaded from


We modeled OTR using Murphi
(http://verify.stanford.edu/dill/murphi.html). Instructions for installing
Murphi can be found at http://sprout.stanford.edu/dill/murphi.html#Getting
. The model may be downloaded from


To run the model, first install Murphi, then decompress
MurphiOTR-1.0.tar.gz and edit the Makefile to point to the correct
location of Murphi. You may then run `make` to compile two programs;
otrake and otrdata. otrake is a model of the authenticated key exchange
while otrdata is a model of the data exchange protocol. Setting the
various flags at the top of otrake.m and otrdata.m will show the attacks
we've discovered and give a trace of the violating path.

My partner Joe Bonneau and I would love to hear feedback from everyone
about the analysis and argue about if the attacks are actually possible or
not. One attack we've discovered is strong enough to force a version 3 of
the protocol, we believe. We'd love to be involved in any discussion
leading to that, and update the model when the time comes.

Andrew S. Morrison
asm at cs.stanford.edu
(650) 575 9261
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: not available
URL: <http://lists.cypherpunks.ca/pipermail/otr-dev/attachments/20060321/e9044534/attachment.pgp>

More information about the OTR-dev mailing list