(FWD) analysis of DH variants

[Roger Dingledine <arma@mit.edu>]

This is a followup to the earlier thread about PFS for the onionskin
handshakes: http://archives.seul.org/or/dev/Sep-2003/msg00028.html

My favorite is Variant 1.

I'll put it on the todo list. :)
--Roger

----- Forwarded message from "Catherine A. Meadows" <meadows@itd.nrl.navy.mil> -----

From: "Catherine A. Meadows" <meadows@itd.nrl.navy.mil>
Date: Wed, 15 Oct 2003 18:34:43 -0400 (EDT)
To: arma@mit.edu, syverson@itd.nrl.navy.mil
Cc: meadows@itd.nrl.navy.mil
Subject: analysis of DH variants

Hi Roger, Paul:

This is to let you know that I've finished the NRL Protocol Analyzer
analysis of the four variants Roger sent to Paul earlier.  All of them
passed both for perfect forward secrecy and for authentication of the
responders DH key half to the initiator.

A little more detail:  I pretty much used the traditional Dolev-Yao
model, where
we assume the existence of an intruder
who can read, intercept, modify traffic, create its own messages, and
who may be in league with one or more dishonest principals. 
I also included an optional event that describes the
compromise of a session key belonging to the initiator, which takes
place after the initiator has accepted the key, and another optional
event describing the compromise of a principal's private key, which can
take place any time.
  
I then had two requirements:

1.  It should be impossible for an intruder to learn a key that
has been accepted by an honest initiator for communication with an
honest responder unless:
  a. the key was compromised, or;
  b. the responder's private key was compromised prior to the initiator's
accepting the key

2. If an honest initiator accepts two halves X and Y of
a Diffie-Hellman key exchange for communication with an honest
responder then either the following two events must have previously occurred in
sequence:
   a. The initiator initiated contact with the responder using X
   b. The responder responded to the initiator's key half X with its own
   key half Y
or the responder's private key was compromised prior to the initiator's
accepting the key.

Although these properties don't exactly match up to the notions
of unilateral entity authentication and unilateral key authentication
(with perfect forward secrecy),
I think it should be straightforward to show that it implies them. 

In response to Roger's question as to why public key encryption doesn't
appear in the standard DH examples:  I've never seen any discussion
of it, but my assumption has always been that because the reasoning behind
the use of public key encryption (as opposed to signatures) for authentication
is rather round-about, people prefer to avoid it in favor of a more
straightforward approach that is easier to get right.  But I don't
know of any other reason for avoiding it.  And I have seen it in places;
for example, it is one of the options in IKE version 1.  There's also the
famous example of the Needham-Schroeder Public Key protocol, which, although
it doesn't use DH, does use public key for authentication.  It has
a well-known security flaw which was undiscovered for 15 years, and that
may have been one of the things to put people off the technique.

Cathy


----- End forwarded message -----