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

[Andrew S. Morrison]

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

	http://www.stanford.edu/~amo/otr_analysis.pdf

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

	http://www.stanford.edu/~amo/MurphiOTR-1.0.tar.gz

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>