tree b409a574857390916f5ed02a214796c9ed8d33ef
parent 1e2d389ca4b641c832fb7a96edb5566619f7ceb6
author Ankur Taly <ataly@ataly-linux.mtv.corp.google.com> 1452288043 -0800
committer Ankur Taly <ataly@ataly-linux.mtv.corp.google.com> 1452288047 -0800

docs/proof": Strengthen authenticity property.

The current formalization of the authentication protocol involves
both the dialer and acceptor taking in the expected public key of the
other end as an input, and then verifying that the blessings received
during the protocol are for these public keys. This check is more of an
"authorization" check and is not strictly needed for proving the
authenticity property.

This CL gets rid of the "expected public key" check from the acceptor
thus allowing the acceptor to accept a connection from any dialer ---
this is indeed the case in practice. (The dialer still retains the
expected public key check, more on this below.)

Now we change the authenticity property to say that if the acceptor
accepts a connection with the dialer's public key then the dialer must
have accepted a connection with the acceptor's public key, and vice
versa. Note that we allow the acceptor to accept a connection with a
public key different from the dialer (e.g., an attacker may open his own
connection to the acceptor).

The dialer still needs to perform the expected public key check in order
to achieve the dialer privacy goal. Essentially, if the dialer does not
employ a peer authorization check then it may reveal its blessings to
the attacker.

Change-Id: I05ba88813996ab630dcc80a3a3696020ea9a4607