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
diff --git a/proofs/authentication/README.md b/proofs/authentication/README.md
index c6cb98f..f2bd9f6 100644
--- a/proofs/authentication/README.md
+++ b/proofs/authentication/README.md
@@ -134,9 +134,9 @@
5. RESULT not attacker(secretMessage[]) is true.
-6. RESULT event(termDialer(k, pkc, pks)) ==> event(acceptsAcceptor(k, pkc, pks)) is true.
+6. RESULT event(termDialer(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) ==> event(acceptsAcceptor(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) is true.
-7. RESULT event(acceptsAcceptor(k, pkc, pks)) ==> event(acceptsDialer(k, pkc, pks)) is true.
+7. RESULT event(acceptsAcceptor(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) ==> event(acceptsDialer(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) is true.
```
The first two messages respectively state that the attacker learns the
diff --git a/proofs/authentication/protocol.pv b/proofs/authentication/protocol.pv
index 661666f..d7ed92b 100644
--- a/proofs/authentication/protocol.pv
+++ b/proofs/authentication/protocol.pv
@@ -31,15 +31,15 @@
key and the public key of the dialer's and acceptor's blessings.
(2) Channel Secrecy
- A message sent from dialer to acceptor on the established
+ Any message sent from dialer to acceptor on the established
encrypted channel is not revealed to the attacker.
(3) Dialer Privacy
- The dialer's public Key is never revealed to the attacker.
+ The dialer's public key is never revealed to the attacker.
The acceptor reveals its blessing to any dialer that wants to talk to it,
-therefore the acceptor's public Key is not a secret. We verify that the
-acceptor's Public Key can be obtained by the attacker.
+therefore the acceptor's public key is not a secret. We verify that the
+acceptor's public key can be obtained by the attacker.
------------------------------------------------------------------------------*)
set predicatesImplementable = nocheck.
@@ -96,7 +96,7 @@
(* Type Conversion -----------------------------------------------------------*)
fun keyToBitstring(SymmetricKey):bitstring [data].
-(* symmetricEncrypt(msg, key): Encrypt 'msg' using symmetric key 'key' *)
+(* symmetricEncrypt(msg, key): Authenticated encryption of 'msg' using symmetric key 'key' *)
fun symmetricEncrypt(bitstring, SymmetricKey):bitstring.
(* symmetricDecrypt(ciphertext, key): Decrypt 'ciphertext' using symmetric key 'key' *)
@@ -249,7 +249,7 @@
) then
out(retCh, pubKey).
-(* dialHandshake process which takes as input the blessings and private key to
+(* Dialer process which takes as input the blessings and private key to
be used during authentication, the expected public key of the acceptor
(used for authorizing the acceptor's blessings). *)
let dialHandshake(blessing:bitstring, privKey:bitstring, pubKeyExpected:bitstring) =
@@ -262,26 +262,23 @@
new retCh2:channel;
readRemoteAuth(aToDCh, key, remoteBnd, acceptorTag, retCh2) |
in(retCh2, pubKeyAcceptor:bitstring);
-
- (* Verify acceptor blessings and public key (peer authorization) *)
- if (pubKeyAcceptor = pubKeyExpected) then
event acceptsDialer(key, publicKeyBlessing(blessing), pubKeyAcceptor);
-
+
(* Send auth message *)
+ if (pubKeyAcceptor = pubKeyExpected) then
let signedBinding = signedChannelBinding(privKey, dialerTag, localBnd) in
out(dToACh, symmetricEncrypt(t(blessing, signedBinding), key));
- (* Receive secret message. *)
- in(aToDCh, secretMsg:bitstring);
- let t(tag:bitstring, msg:bitstring) = symmetricDecrypt(secretMsg, key) in
+ (* Receive auth success confirmation. *)
+ in(aToDCh, msg:bitstring);
+ let t(tag:bitstring, pubKey:bitstring) = symmetricDecrypt(msg, key) in
if tag = messageTag then
+ if pubKey = publicKeyBlessing(blessing) then
event termDialer(key, publicKeyBlessing(blessing), pubKeyAcceptor).
(* Acceptor process which takes as input the blessings and private key to
- be used during authentication, and the expected public key of the
- dialer (used for authorizing the dialer's blessings), , and a secret
- message to be sent on the channel once authentication succeeds *)
-let acceptHandshake(blessing:bitstring, privKey:bitstring, pubKeyExpected:bitstring, secretMessage:bitstring) =
+ be used during authentication. *)
+let acceptHandshake(blessing:bitstring, privKey:bitstring) =
(* Setup *)
new retCh:channel;
setup(aToDCh, dToACh, retCh) |
@@ -292,29 +289,24 @@
let acceptorAuth = t(blessing, signedBinding) in
out(aToDCh, symmetricEncrypt(acceptorAuth, key));
- (* Receive auth mesage *)
+ (* Receive auth message *)
new retCh2:channel;
readRemoteAuth(dToACh, key, remoteBnd, dialerTag, retCh2) |
in(retCh2, pubKeyDialer:bitstring);
-
- (* Verify dialer blessings and public key (peer authorization) *)
- if (pubKeyDialer = pubKeyExpected) then
event acceptsAcceptor(key, pubKeyDialer, publicKeyBlessing(blessing));
- (* Send secret message. *)
- out(aToDCh, symmetricEncrypt(t(messageTag, secretMessage), key)).
+ (* Send auth success confirmation. *)
+ out(aToDCh, symmetricEncrypt(t(messageTag, pubKeyDialer), key)).
(* Protocol Process *)
let handshake(
blessingDialer:bitstring,
privKeyDialer:bitstring,
blessingAcceptor:bitstring,
- privKeyAcceptor:bitstring,
- secretMessage:bitstring) =
- let pubKeyDialer = publicKeyBlessing(blessingDialer) in
+ privKeyAcceptor:bitstring) =
let pubKeyAcceptor = publicKeyBlessing(blessingAcceptor) in
dialHandshake(blessingDialer, privKeyDialer, pubKeyAcceptor) |
- acceptHandshake(blessingAcceptor, privKeyAcceptor, pubKeyDialer, secretMessage) .
+ acceptHandshake(blessingAcceptor, privKeyAcceptor) .
(* Authentication Protocol Instance --------------------------------------------
Instantiates the Vanadium authentication protocol for specific dialer and
@@ -324,30 +316,28 @@
free privKeyDialer:bitstring [private].
free privKeyAcceptor:bitstring [private].
-free secretMessage:bitstring [private].
let handshakeInstance() =
new rootPrivKey:bitstring;
let rootBlessing = newSelfBlessing(rootPrivKey) in
let blessingDialer = bless(publicKey(privKeyDialer), rootBlessing, rootPrivKey) in
let blessingAcceptor = bless(publicKey(privKeyAcceptor), rootBlessing, rootPrivKey) in
- handshake(blessingDialer, privKeyDialer, blessingAcceptor, privKeyAcceptor, secretMessage) .
+ handshake(blessingDialer, privKeyDialer, blessingAcceptor, privKeyAcceptor) .
(* Authenticity *)
-query k:SymmetricKey, pkc:bitstring, pks:bitstring;
- event(acceptsAcceptor(k, pkc, pks)) ==> event(acceptsDialer(k, pkc, pks)).
- (* Desired ProVerif output: event(acceptsAcceptor(k,pkc,pks)) ==> event(acceptsDialer(k,pkc,pks)) is true *)
-query k:SymmetricKey, pkc:bitstring, pks:bitstring;
- event(termDialer(k, pkc, pks)) ==> event(acceptsAcceptor(k, pkc, pks)).
- (* Desired ProVerif output: event(termDialer(k,pkc,pks)) ==> event(acceptsAcceptor(k,pkc,pks)) is true *)
+query k:SymmetricKey;
+ event(acceptsAcceptor(k, publicKey(privKeyDialer), publicKey(privKeyAcceptor))) ==> event(acceptsDialer(k, publicKey(privKeyDialer), publicKey(privKeyAcceptor))).
+ (* Desired ProVerif output: event(acceptsAcceptor(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) ==> event(acceptsDialer(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) is true *)
+query k:SymmetricKey;
+ event(termDialer(k, publicKey(privKeyDialer), publicKey(privKeyAcceptor))) ==> event(acceptsAcceptor(k, publicKey(privKeyDialer), publicKey(privKeyAcceptor))).
+ (* Desired ProVerif output: event(termDialer(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) ==> event(acceptsAcceptor(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) is true *)
-(* Channel Secrecy *)
-query attacker(secretMessage). (* Desired ProVerif output: not attacker(secretMessage) is true *)
+(* Channel Secrecy and Dialer Privacy*)
query attacker(privKeyDialer). (* Desired ProVerif output: not attacker(privKeyDialer) is true *)
query attacker(privKeyAcceptor). (* Desired ProVerif output: not attacker(privKeyAcceptor) is true *)
-
-(* Dialer Privacy *)
query attacker(publicKey(privKeyDialer)). (* Desired ProVerif output: not attacker(publicKey(privKeyDialer)) is true *)
-query attacker(publicKey(privKeyAcceptor)). (* Desired ProVerif output: not attacker(publicKey(privKeyAcceptor)) is true *)
+
+(* Lack of Acceptor Privacy *)
+query attacker(publicKey(privKeyAcceptor)). (* Desired ProVerif output: not attacker(publicKey(privKeyAcceptor)) is false *)
process handshakeInstance()
\ No newline at end of file
