[OTR-dev] OTR Formal Analysis Security Properties

[Ian Goldberg]

On Mon, Feb 13, 2006 at 06:04:46PM -0800, Andrew S. Morrison wrote:
> As mentioned awhile back, myself and a partner are working on a formal
> security analysis of OTR. Before we try to break it, I just wanted to send
> you what we're working on in terms of what security properties OTR claims
> to see if we're in agreement. Attached is a PDF of our working definitions
> for the properties that should hold on OTR. Do you guys agree or disagree
> on any of the definitions? Is anything missing? Are any of the claims too
> strong or weak? Thanks.

I took a quick look.

In the PFS definition, Mallory *is* allowed to be able to read _very
recent_ messages sent between Alice and Bob (i.e. messages sent with
keys Alice and/or Bob are still using).  So just saying Mallory cannot
read messages with timestamp t' < t isn't quite right, I think.

And a tiny nit, but I think you mean "principal" where you write
"principle".  ;-)

Otherwise, it looks pretty plausible.  I look forward to seeing the
results of your work!

   - Ian