"docs": Authentication protocol proof -- code correspondence
This CL updates the proof of our mutual authentication protocol
so that it corresponds to the Golang code in
https://vanadium.googlesource.com/release.go.x.ref/+/master/runtime/internal/flow/conn/auth.go
In particular, the protocol formalization in the proof is structured
similar to the code with two key helper functions "setup" and
"readRemoteAuth". Furthermore, following the convention in the code,
all occurrences of the words "client" and "server" are replaced with
"dialer" and "acceptor" respectively.
Change-Id: I40e61b022c3cd8d06abd8a1f9b2b8437298ec7d9
diff --git a/proofs/authentication/README.md b/proofs/authentication/README.md
index a9b007c..c6cb98f 100644
--- a/proofs/authentication/README.md
+++ b/proofs/authentication/README.md
@@ -52,34 +52,35 @@
The complete formalization of the authentication protocol along with all cryptographic
primitives, and Vanadium primitives (such as: certificates and blessings) is specified
in `protocol.pv`. The steps of the protocol are captured in the process
-`authProtocol` that is parametric on the blessing and private key of the client and
-the server.
+`handshake` that is parametric on the blessing and private key of the dialer and
+the acceptor. Dialer (aka client) is the initiator of the first handshake message
+and Acceptor (aka server) is the responder of the first handshake message.
## Security Properties
We verify three key properties of the authentication protocol.
-(1) _Mutual Authentication_: The client and server must agree on the
- established encryption key and each others blessings. This property
+(1) _Mutual Authentication_: The dialer and acceptor must agree on the
+ established encryption key and each others blessings. This property
is formalized as a pair of correspondence properties in ProVerif stating that a
- server accepts a session if and only if the client accepts the same
+ acceptor accepts a session if and only if the dialer accepts the same
session, where a session is defined by the session encryption key and
- the public keys of the client's and server's blessings.
+ the public keys of the dialer's and acceptor's blessings.
(2) _Channel Confidentiality_: The session encryption key established
is protected from attackers. This property is verified by checking
that a message encrypted under the session key and sent from the
- server to the client is not revealed to the attacker. This is specified
+ acceptor to the dialer is not revealed to the attacker. This is specified
as a reachability property in ProVerif.
-(3) _Client Privacy_: The client's public key is never revealed to the attacker. This
- is specified as a reachability property in ProVerif. The server's public key does get
+(3) _Dialer Privacy_: The dialer's public key is never revealed to the attacker. This
+ is specified as a reachability property in ProVerif. The acceptor's public key does get
revealed to the attacker, and we verify this using another reachability
property in ProVerif.
We verify security properties for an instantiation of the protocol process
-(`authProtocol`) with randomly chosen private keys for the client and server,
-and randomly chosen blessings of depth two for the client and server. We note
+(`authProtocol`) with randomly chosen private keys for the dialer and acceptor,
+and randomly chosen blessings of depth two for the dialer and acceptor. We note
that the depth of the blessings in the instantiation should not affect the
security properties, i.e., the verification should go through for arbitrary
depth blessings if it goes through for depth two blessings. However, a formal
@@ -123,35 +124,35 @@
(We add line numbers for ease of reading.)
```
-1. RESULT not attacker(publicKey(privKeyServer[])) is false.
+1. RESULT not attacker(publicKey(privKeyAcceptor[])) is false.
-2. RESULT not attacker(publicKey(privKeyClient[])) is true.
+2. RESULT not attacker(publicKey(privKeyDialer[])) is true.
-3. RESULT not attacker(privKeyServer[]) is true.
+3. RESULT not attacker(privKeyAcceptor[]) is true.
-4. RESULT not attacker(privKeyClient[]) is true.
+4. RESULT not attacker(privKeyDialer[]) is true.
5. RESULT not attacker(secretMessage[]) is true.
-6. RESULT event(termClient(k, pkc, pks)) ==> event(acceptsServer(k, pkc, pks)) is true.
+6. RESULT event(termDialer(k, pkc, pks)) ==> event(acceptsAcceptor(k, pkc, pks)) is true.
-7. RESULT event(acceptsServer(k, pkc, pks)) ==> event(acceptsClient(k, pkc, pks)) is true.
+7. RESULT event(acceptsAcceptor(k, pkc, pks)) ==> event(acceptsDialer(k, pkc, pks)) is true.
```
The first two messages respectively state that the attacker learns the
-public key of the server but not the client. This verifies the _client privacy_
+public key of the acceptor but not the dialer. This verifies the _dialer privacy_
property.
The next three messages respectively state that the attacker _does not_
-learn the private key of the server, the private key of the client, and
-the secret message sent by the server to the client over the established
+learn the private key of the acceptor, the private key of the dialer, and
+the secret message sent by the acceptor to the dialer over the established
encrypted channel. This verifies the _channel secrecy_ property.
The last two messages state two correspondence properties that
-together imply that a client accepts a certain session if and
-only if the server also accepts the same session, where a session
+together imply that a dialer accepts a certain session if and
+only if the acceptor also accepts the same session, where a session
is defined by the session encryption key and the public keys of
-the client's and server's blessings. This verifies the _mutual authentication_
+the dialer's and acceptor's blessings. This verifies the _mutual authentication_
property.
[auth]:https://github.com/vanadium/docs/blob/master/designdocs/authentication.md
diff --git a/proofs/authentication/protocol.pv b/proofs/authentication/protocol.pv
index a543d7d..661666f 100644
--- a/proofs/authentication/protocol.pv
+++ b/proofs/authentication/protocol.pv
@@ -1,9 +1,9 @@
(* Vanadium Authentication Protocol --------------------------------------------
Informal Protocol Specification:
-C is Client, S is Server
-C : Client
-S : Server
+D is Dialer, A is Acceptor
+D : Dialer
+A : Acceptor
g : Diffie-Hellman Group generator
x,y : exponents
@@ -15,31 +15,31 @@
Protocol:
-C generates x, and S generates y
+D generates x, and A generates y
-C ---> S: g^x
-S ---> C: g^y
-S ---> C: {B_S, sign_S(hash(S, g^x, g^y))}_key(g^xy)
-C ---> S: {B_C, sign_C(hash(C, g^x, g^y))}_key(g^xy)
-C ---> S: {M}_key(g^xy)
+D ---> A: g^x
+A ---> D: g^y
+A ---> D: {B_A, sign_A(hash("A", g^x, g^y))}_key(g^xy)
+D ---> A: {B_D, sign_D(hash("D", g^x, g^y))}_key(g^xy)
+D ---> A: {M}_key(g^xy)
We are interested in verifying the following correctness properties:
(1) Mutual Authentication
- Server only authenticates a session once the client has authenticated
+ Acceptor only authenticates a session once the dialer has authenticated
the same session, where a session is defined by the session encryption
- key and the public key of the client's and server's blessings.
+ key and the public key of the dialer's and acceptor's blessings.
(2) Channel Secrecy
- A message sent from Client to Server on the established
+ A message sent from dialer to acceptor on the established
encrypted channel is not revealed to the attacker.
-(3) Client Privacy
- The client's public Key is never revealed to the attacker.
+(3) Dialer Privacy
+ The dialer's public Key is never revealed to the attacker.
-The Server shows its blessing to any client that wants to talk to it,
-therefore the Server's Public Key is not a secret. We verify that the
-server's Public Key can be obtained by 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.
------------------------------------------------------------------------------*)
set predicatesImplementable = nocheck.
@@ -75,7 +75,7 @@
const g:G [data]. (*The generator of G, publicly known*)
(* Type Conversion -----------------------------------------------------------*)
-fun gToBitstring(G):bitstring.
+fun gToBitstring(G):bitstring [data].
(* Group Definition ---------------------------------------------------------*)
fun exp(G, Exponent):G.
@@ -93,6 +93,9 @@
fun generateKey(bitstring):SymmetricKey.
+(* Type Conversion -----------------------------------------------------------*)
+fun keyToBitstring(SymmetricKey):bitstring [data].
+
(* symmetricEncrypt(msg, key): Encrypt 'msg' using symmetric key 'key' *)
fun symmetricEncrypt(bitstring, SymmetricKey):bitstring.
@@ -193,121 +196,158 @@
(* Authentication Protocol ----------------------------------------------------
Formalizes the Vanadium authentication protocol.
------------------------------------------------------------------------------*)
+letfun signedChannelBinding(privKey:bitstring, tag:bitstring, binding:bitstring) =
+ sign(hash(t(tag, binding)), privKey).
-letfun signedChannelBinding(privKey:bitstring, tag:bitstring, g_x:G, g_y:G) =
- sign(hash(t(t(tag, gToBitstring(g_x)), gToBitstring(g_y))), privKey).
+letfun verifyChannelBinding(pubKey:bitstring, tag:bitstring, binding:bitstring, signature:bitstring) =
+ verifySignature(pubKey, hash(t(tag, binding)), signature).
-letfun verifyChannelBinding(pubKey:bitstring, tag:bitstring, g_x:G, g_y:G, signature:bitstring) =
- verifySignature(pubKey, hash(t(t(tag, gToBitstring(g_x)), gToBitstring(g_y))), signature).
+(* Public communication network. *)
+free dToACh:channel. (* channel simulating a network pipe from dialer to acceptor *)
+free aToDCh:channel. (* channel simulating a network pipe from acceptor to dialer *)
-(* Public communication channel. *)
-free c:channel.
-free serverTag:bitstring.
-free clientTag:bitstring.
+free acceptorTag:bitstring.
+free dialerTag:bitstring.
free messageTag:bitstring.
-event acceptsServer(SymmetricKey, bitstring, bitstring).
-event acceptsClient(SymmetricKey, bitstring, bitstring).
-event termClient(SymmetricKey, bitstring, bitstring).
+event acceptsAcceptor(SymmetricKey, bitstring, bitstring).
+event acceptsDialer(SymmetricKey, bitstring, bitstring).
+event termDialer(SymmetricKey, bitstring, bitstring).
-(* Client process which takes as input the blessings and private key to
- be used during authentication, the expected public key of the server
- (used for authorizing the server's blessings), and a secret message
- to be sent on the channel once authentication succeeds. *)
-let client(blessing:bitstring, privKey:bitstring, pubKeyExpected:bitstring) =
+let encrypter(key:SymmetricKey, inCh:channel, outCh:channel) =
+ in(inCh, msg:bitstring);
+ out(outCh, symmetricEncrypt(msg, key)).
+
+let decrypter(key:SymmetricKey, inCh:channel, outCh:channel) =
+ in(inCh, ctxt:bitstring);
+ let ptxt = symmetricDecrypt(ctxt, key) in
+ out(outCh, ptxt).
+
+(* Setup performs a Diffie-Hellman key exchange and returns the generated
+ symmetric key, the local and remote channel bindings on retCh. *)
+let setup(outCh:channel, inCh:channel, retCh:channel) =
new x:Exponent;
let g_x = exp(g, x) in
- out(c, g_x);
- in(c, g_y:G);
+ out(outCh, g_x) |
+ in(inCh, g_y:G);
let key = generateKey(gToBitstring(exp(g_y, x))) in
- in(c, serverAuth:bitstring);
- let t(blessingServer:bitstring, serverChBinding:bitstring) = symmetricDecrypt(serverAuth, key) in
- let pubKeyServer = publicKeyBlessing(blessingServer) in
- (* Verify server's authentication message and accept session with server if verification succeeeds. *)
- if (
- verifyBlessing(blessingServer) &&
- verifyChannelBinding(pubKeyServer, serverTag, g_x, g_y, serverChBinding) &&
- pubKeyServer = pubKeyExpected (* Verify if the server's blessings are authorized. *)
- ) then
- event acceptsClient(key, publicKeyBlessing(blessing), pubKeyServer);
- let clientChBinding = signedChannelBinding(privKey, clientTag, g_x, g_y) in
- let clientAuth = symmetricEncrypt(t(blessing, clientChBinding), key) in
- out(c, clientAuth);
- (* Receive secret message. *)
- in(c, encryptedMessage:bitstring);
- let t(tag:bitstring, msg:bitstring) = symmetricDecrypt(encryptedMessage, key) in
- if tag = messageTag then
- event termClient(key, publicKeyBlessing(blessing), pubKeyServer).
+ let localBnd = t(gToBitstring(g_x), gToBitstring(g_y)) in
+ let remoteBnd = t(gToBitstring(g_y), gToBitstring(g_x)) in
+ out(retCh, t(t(keyToBitstring(key), localBnd), remoteBnd)).
-(* Server process which takes as input the blessings and private key to
- be used during authentication, and the expected public key of the
- client (used for authorizing the client's blessings). *)
-let server(blessing:bitstring, privKey:bitstring, pubKeyExpected:bitstring, secretMessage:bitstring) =
- new y:Exponent;
- let g_y = exp(g, y) in
- in(c, g_x:G);
- out(c, g_y);
- let key = generateKey(gToBitstring(exp(g_x, y))) in
- let serverChBinding = signedChannelBinding(privKey, serverTag, g_x, g_y) in
- let serverAuth = symmetricEncrypt(t(blessing, serverChBinding), key) in
- out(c, serverAuth);
- in(c, clientAuth:bitstring);
- let t(blessingClient:bitstring, clientChBinding:bitstring) = symmetricDecrypt(clientAuth, key) in
- (* Verify client's authentication message and accept session with client if verification succeeeds. *)
- let pubKeyClient = publicKeyBlessing(blessingClient) in
+(* readRemoteAuth receives the auth message (blessings + signed channel binding) sent
+ by the remote end and verifies it. If verification succeeds, it returns the public
+ key of the remote end on retCh. *)
+let readRemoteAuth(inCh:channel, key: SymmetricKey, binding: bitstring, tag: bitstring, retCh:channel) =
+ in(inCh, auth:bitstring);
+ let t(blessing:bitstring, chBinding:bitstring) = symmetricDecrypt(auth, key) in
+ let pubKey = publicKeyBlessing(blessing) in
+ (* Verify authentication message and return pubKey only if verification succeeeds. *)
if (
- verifyBlessing(blessingClient) &&
- verifyChannelBinding(pubKeyClient, clientTag, g_x, g_y, clientChBinding) &&
- pubKeyClient = pubKeyExpected (* Verify if the client's blessings are authorized. *)
+ verifyBlessing(blessing) &&
+ verifyChannelBinding(pubKey, tag, binding, chBinding)
) then
- event acceptsServer(key, pubKeyClient, publicKeyBlessing(blessing));
+ out(retCh, pubKey).
+
+(* dialHandshake 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) =
+ (* Setup *)
+ new retCh1:channel;
+ setup(dToACh, aToDCh, retCh1) |
+ in(retCh1, t(t(keyToBitstring(key:SymmetricKey), localBnd:bitstring), remoteBnd:bitstring));
+
+ (* Receive auth mesage *)
+ 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 *)
+ 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
+ if tag = messageTag 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) =
+ (* Setup *)
+ new retCh:channel;
+ setup(aToDCh, dToACh, retCh) |
+
+ (* Send auth message *)
+ in(retCh, t(t(keyToBitstring(key:SymmetricKey), localBnd:bitstring), remoteBnd:bitstring));
+ let signedBinding = signedChannelBinding(privKey, acceptorTag, localBnd) in
+ let acceptorAuth = t(blessing, signedBinding) in
+ out(aToDCh, symmetricEncrypt(acceptorAuth, key));
+
+ (* Receive auth mesage *)
+ 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(c, symmetricEncrypt(t(messageTag, secretMessage), key)).
+ out(aToDCh, symmetricEncrypt(t(messageTag, secretMessage), key)).
(* Protocol Process *)
-let authProtocol(
- blessingClient:bitstring,
- privKeyClient:bitstring,
- blessingServer:bitstring,
- privKeyServer:bitstring,
+let handshake(
+ blessingDialer:bitstring,
+ privKeyDialer:bitstring,
+ blessingAcceptor:bitstring,
+ privKeyAcceptor:bitstring,
secretMessage:bitstring) =
- let pubKeyClient = publicKeyBlessing(blessingClient) in
- let pubKeyServer = publicKeyBlessing(blessingServer) in
- client(blessingClient, privKeyClient, pubKeyServer) |
- server(blessingServer, privKeyServer, pubKeyClient, secretMessage) .
+ let pubKeyDialer = publicKeyBlessing(blessingDialer) in
+ let pubKeyAcceptor = publicKeyBlessing(blessingAcceptor) in
+ dialHandshake(blessingDialer, privKeyDialer, pubKeyAcceptor) |
+ acceptHandshake(blessingAcceptor, privKeyAcceptor, pubKeyDialer, secretMessage) .
(* Authentication Protocol Instance --------------------------------------------
- Instantiates the Vanadium authentication protocol for specific client and
- server blessings and formalizes the desired correctness properties -- mutual
- authentication, channel secrecy and client privacy.
+ Instantiates the Vanadium authentication protocol for specific dialer and
+ acceptor blessings and formalizes the desired correctness properties -- mutual
+ authentication, channel secrecy and dialer privacy.
------------------------------------------------------------------------------*)
-free privKeyClient:bitstring [private].
-free privKeyServer:bitstring [private].
+free privKeyDialer:bitstring [private].
+free privKeyAcceptor:bitstring [private].
free secretMessage:bitstring [private].
-let authProtocolInstance() =
+let handshakeInstance() =
new rootPrivKey:bitstring;
let rootBlessing = newSelfBlessing(rootPrivKey) in
- let blessingClient = bless(publicKey(privKeyClient), rootBlessing, rootPrivKey) in
- let blessingServer = bless(publicKey(privKeyServer), rootBlessing, rootPrivKey) in
- authProtocol(blessingClient, privKeyClient, blessingServer, privKeyServer, secretMessage) .
+ let blessingDialer = bless(publicKey(privKeyDialer), rootBlessing, rootPrivKey) in
+ let blessingAcceptor = bless(publicKey(privKeyAcceptor), rootBlessing, rootPrivKey) in
+ handshake(blessingDialer, privKeyDialer, blessingAcceptor, privKeyAcceptor, secretMessage) .
(* Authenticity *)
query k:SymmetricKey, pkc:bitstring, pks:bitstring;
- event(acceptsServer(k, pkc, pks)) ==> event(acceptsClient(k, pkc, pks)).
- (* Desired ProVerif output: event(acceptsServer(k,pkc,pks)) ==> event(acceptsClient(k,pkc,pks)) is true *)
+ 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(termClient(k, pkc, pks)) ==> event(acceptsServer(k, pkc, pks)).
- (* Desired ProVerif output: event(termClient(k,pkc,pks)) ==> event(acceptsServer(k,pkc,pks)) is true *)
+ 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 *)
(* Channel Secrecy *)
query attacker(secretMessage). (* Desired ProVerif output: not attacker(secretMessage) is true *)
-query attacker(privKeyClient). (* Desired ProVerif output: not attacker(privKeyClient) is true *)
-query attacker(privKeyServer). (* Desired ProVerif output: not attacker(privKeyServer) is true *)
+query attacker(privKeyDialer). (* Desired ProVerif output: not attacker(privKeyDialer) is true *)
+query attacker(privKeyAcceptor). (* Desired ProVerif output: not attacker(privKeyAcceptor) is true *)
-(* Client Privacy *)
-query attacker(publicKey(privKeyClient)). (* Desired ProVerif output: not attacker(publicKey(privKeyClient)) is true *)
-query attacker(publicKey(privKeyServer)). (* Desired ProVerif output: not attacker(publicKey(privKeyServer)) 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 *)
-process authProtocolInstance()
\ No newline at end of file
+process handshakeInstance()
\ No newline at end of file
