proofs: Add ProVerif proofs for the Vanadium Authentication Protocol
and link to the design doc.
This work was done by Siddhartha Jayanti and Ankur Taly
(https://github.com/ankurtaly) in another repository. I'm just moving
them here.
Change-Id: I0a6ac77eca9e4bffd53ea70ea3590ecf5295ab48
diff --git a/designdocs/authentication.md b/designdocs/authentication.md
index 7c82eac..817310a 100644
--- a/designdocs/authentication.md
+++ b/designdocs/authentication.md
@@ -57,6 +57,12 @@
- If the Client is not happy with the blessing names presented by the Server,
it can abort the connection without ever revealing its blessings.
+### Correctness Proof
+
+The protocol along with the guarantees that it makes has been formalized in
+[ProVerif] to provide a proof of correctness. This formalization is available
+at https://github.com/vanadium/docs/tree/master/proofs/authentication
+
### Code pointers
Pointers to code in the reference implementation of the Vanadium APIs:
@@ -124,3 +130,4 @@
[`v.io/v23/security.Principal`]: https://godoc.org/v.io/v23/security#Principal
[`v.io/x/ref/runtime/internal/rpc/stream`]: https://godoc.org/v.io/x/ref/runtime/internal/rpc/stream
[NaCl/box]: https://godoc.org/golang.org/x/crypto/nacl/box
+[ProVerif]:http://prosecco.gforge.inria.fr/personal/bblanche/proverif/
diff --git a/proofs/authentication/README.md b/proofs/authentication/README.md
new file mode 100644
index 0000000..a9b007c
--- /dev/null
+++ b/proofs/authentication/README.md
@@ -0,0 +1,168 @@
+# Verifying the Vanadium Authentication Protocol
+
+This project defines a formalization of the [Vanadium authentication protocol][auth]
+and verifies the desired security properties for it using the automatic cryptographic protocol verifier [ProVerif][proverif].
+
+The authentication protocol is used during a [Vanadium RPC][rpc] for mutual
+authentication and setting up an encrypted channel for sending RPC data.
+More specifically, the protocol allows each end of an RPC to exchange [blessings]
+with the other end and verify that the other end possesses the private key corresponding
+to the public key to which its blessings are bound. At the end of the protocol,
+an encrypted channel is established between the two ends for performing the
+RPC. The blessings learned as part of the authentication may be used to
+authorize the RPC (e.g., by checking that the blessing name is present on
+a particular [access list][acl]).
+
+The design of the protocol is very similar to the [SIGMA-I][sigma] protocol from
+the literature. It involves a [Diffie-Hellman key exchange][ecdhe], followed by an
+exchange of blessings and private key possession proofs. However, the protocol
+differs from SIGMA-I in how this private key possession proof is represented. We
+refer the reader to the [design doc][auth] for a detailed specification of the
+protocol.
+
+Decades of research in protocol design has shown that manually assessing the
+security of a protocol is challenging as it is difficult to enumerate and
+examine all possible attack scenarios. There have been a number of instances
+of published protocols that intuitively seemed secure but had serious
+vulnerabilities, e.g., the [Needham-Schroeder protocol][needham]. The only way to
+guarantee security of a protocol is to formally specify it and mathematically
+prove its security properties.
+
+## ProVerif
+
+[ProVerif][proverif] is a tool for automatically analyzing properties of security
+protocols. It is capable of proving reachability properties, correspondence assertions,
+and observational equivalence properties of protocols. The ProVerif specification language
+is a variant of the [applied pi-calculus][applied-pi-calculus]. We refer the reader to the
+[ProVerif manual][proverif-manual] for the authoritative definition of the language.
+
+ProVerif analyzes protocols in the symbolic, [Dolev-Yao][dolev-yao] attacker model.
+In this model, the attacker controls the communication channel between the protocol
+participants and can read, modify, delete and inject messages. But the attacker
+cannot "break" cryptographic primitives and can only use them via their legitimate
+interfaces. For instance, the attacker can only decrypt those encrypted messages for
+which it knows the encryption key.
+
+ProVerif is sound but not complete. This means that if ProVerif confirms
+that a security property is true then the property is indeed true in the Dolev-Yao attacker
+model. However, not all true properties may be provable by ProVerif.
+
+## Protocol Formalization
+
+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.
+
+## 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
+ 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
+ session, where a session is defined by the session encryption key and
+ the public keys of the client's and server'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
+ 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
+ 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
+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
+proof of this statement remains to be shown.
+
+## Running the Verification
+
+### Installing ProVerif
+Running the verification requires installing the [ProVerif][proverif] tool.
+Instructions for installing the tool can be found [here][proverif-install]
+
+### Running ProVerif
+Once ProVerif is installed, please set the environment variable
+`PROVERIF` to point at the ProVerif binary.
+
+```
+export PROVERIF=<path to ProVerif binary>
+```
+
+The verification can be run using the following command.
+
+```
+$PROVERIF protocol.pv
+```
+
+### Intrepting the results
+The aforesaid command prints out a bunch of ProVerif messages (we recommend
+reading Section 3 of the [ProVerif manual][proverif-manual] to understand
+these messages) with the verification results for the various properties
+printed towards the end.
+
+A simple way of printing just the verification results is to run the following
+command:
+
+```
+$PROVERIF protocol.pv | grep RESULT
+```
+
+This command should print the following:
+
+(We add line numbers for ease of reading.)
+
+```
+1. RESULT not attacker(publicKey(privKeyServer[])) is false.
+
+2. RESULT not attacker(publicKey(privKeyClient[])) is true.
+
+3. RESULT not attacker(privKeyServer[]) is true.
+
+4. RESULT not attacker(privKeyClient[]) is true.
+
+5. RESULT not attacker(secretMessage[]) is true.
+
+6. RESULT event(termClient(k, pkc, pks)) ==> event(acceptsServer(k, pkc, pks)) is true.
+
+7. RESULT event(acceptsServer(k, pkc, pks)) ==> event(acceptsClient(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_
+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
+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
+is defined by the session encryption key and the public keys of
+the client's and server's blessings. This verifies the _mutual authentication_
+property.
+
+[auth]:https://github.com/vanadium/docs/blob/master/designdocs/authentication.md
+[rpc]:https://github.com/vanadium/docs/blob/master/concepts/rpc.md
+[acl]:https://github.com/vanadium/docs/blob/master/glossary.md#access-list
+[blessings]:https://github.com/vanadium/docs/blob/master/glossary.md#blessings
+[sigma]:http://webee.technion.ac.il/~hugo/sigma.html
+[ecdhe]:https://en.wikipedia.org/wiki/Elliptic_curve_Diffie%E2%80%93Hellman
+[proverif]:http://prosecco.gforge.inria.fr/personal/bblanche/proverif/
+[proverif-manual]:http://prosecco.gforge.inria.fr/personal/bblanche/proverif/manual.pdf
+[proverif-install]:http://prosecco.gforge.inria.fr/personal/bblanche/proverif/README
+[applied-pi-calculus]:http://crysys.hu/members/tvthong/pispi/applied.pdf
+[dolev-yao]:https://en.wikipedia.org/wiki/Dolev%E2%80%93Yao_model
+[needham]:https://en.wikipedia.org/wiki/Needham%E2%80%93Schroeder_protocol
diff --git a/proofs/authentication/protocol.pv b/proofs/authentication/protocol.pv
new file mode 100644
index 0000000..a543d7d
--- /dev/null
+++ b/proofs/authentication/protocol.pv
@@ -0,0 +1,313 @@
+(* Vanadium Authentication Protocol --------------------------------------------
+
+Informal Protocol Specification:
+C is Client, S is Server
+C : Client
+S : Server
+
+g : Diffie-Hellman Group generator
+x,y : exponents
+P_X : Public Key of X
+B_X : Blessing of X
+sign_X(M) : Private Key Signature of M by Principal X
+key(n) : A symmetric key generated with Diffie-Hellman secret n
+{M}_k : Message M encrypted with symmetric key k
+
+Protocol:
+
+C generates x, and S 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)
+
+We are interested in verifying the following correctness properties:
+
+(1) Mutual Authentication
+ Server only authenticates a session once the client 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.
+
+(2) Channel Secrecy
+ A message sent from Client to Server 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.
+
+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.
+------------------------------------------------------------------------------*)
+
+set predicatesImplementable = nocheck.
+set maxDepth = 20.
+set maxHyp = none.
+set ignoreTypes = true.
+set attacker = active.
+set keyCompromise = none.
+set simplifyDerivation = true.
+set abbreviateDerivation = true.
+set explainDerivation = true.
+set reconstructTrace = true.
+set unifyDerivation = true.
+set reconstructDerivation = true.
+set displayDerivation = true.
+set traceBacktracking = true.
+set traceDisplay = short.
+set verboseClauses = none.
+set abbreviateClauses = true.
+set removeUselessClausesBeforeDisplay = true.
+set verboseEq = true.
+set verboseRules = false.
+set verboseRedundant = false.
+
+(* DiffieHellmanGroup ----------------------------------------------------------
+ Defines a group type G that facilitates the running of the Diffie-Hellman
+ protocol.
+------------------------------------------------------------------------------*)
+
+type G. (*Diffie-Hellman Group*)
+type Exponent. (*Diffie-Hellman Group Exponents*)
+
+const g:G [data]. (*The generator of G, publicly known*)
+
+(* Type Conversion -----------------------------------------------------------*)
+fun gToBitstring(G):bitstring.
+
+(* Group Definition ---------------------------------------------------------*)
+fun exp(G, Exponent):G.
+
+(* Associativity of group multiplication abstracted *)
+equation
+ forall x:Exponent, y:Exponent;
+ exp(exp(g, x), y) = exp(exp(g, y), x).
+
+(* Symmetric key crypto primitives ---------------------------------------------
+ Symmetric key encryption and decryption primitives.
+------------------------------------------------------------------------------*)
+
+type SymmetricKey.
+
+fun generateKey(bitstring):SymmetricKey.
+
+(* symmetricEncrypt(msg, key): Encrypt 'msg' using symmetric key 'key' *)
+fun symmetricEncrypt(bitstring, SymmetricKey):bitstring.
+
+(* symmetricDecrypt(ciphertext, key): Decrypt 'ciphertext' using symmetric key 'key' *)
+fun symmetricDecrypt(bitstring, SymmetricKey):bitstring
+reduc
+ forall key:SymmetricKey, message:bitstring;
+ symmetricDecrypt(symmetricEncrypt(message, key), key) = message.
+
+(* Public key crypto primitives ------------------------------------------------
+ Signing and verification primitives.
+------------------------------------------------------------------------------*)
+
+(* publicKey(PrivateKey):Corresponding PublicKey *)
+fun publicKey(bitstring):bitstring.
+
+(* sign(message, PrivateKey):signed message bitstring
+ Signed message cannot be decrypted. *)
+fun sign(bitstring, bitstring):bitstring.
+
+(* verifySignature(PublicKey, plaintext, signed) *)
+pred verifySignature(bitstring, bitstring, bitstring).
+clauses
+ forall privateKey:bitstring, msg:bitstring;
+ verifySignature(publicKey(privateKey), msg, sign(msg, privateKey)).
+
+(* Tuples and Hashing ---------------------------------------------------------
+ Defines the arbitrary length bitstring tuple and associated functions.
+------------------------------------------------------------------------------*)
+
+const null:bitstring [data]. (*Empty Tuple*)
+
+(* t(Tuple, bitstring): bitstring representation of tuple concatenation *)
+fun t(bitstring, bitstring):bitstring [data].
+
+(* hash(item): a truly one-way hash function on item *)
+fun hash(bitstring):bitstring.
+
+(* Certificate -----------------------------------------------------------------
+ A Vanadium Certificate:
+ A tuple (Name, PublicKey, Caveats, Signature)
+------------------------------------------------------------------------------*)
+
+(* certificate(Name, PublicKey, Caveats, Signature) *)
+fun certificate(bitstring, bitstring, bitstring, bitstring):bitstring [data].
+
+(* Blessing --------------------------------------------------------------------
+ A Vanadium Blessing:
+ An arbitrary length tuple/list of Certificates
+------------------------------------------------------------------------------*)
+
+(* publicKeyBlessing(blessing): Returns the public key of last certificate of the
+ certificate chain represented by 'blessing'. *)
+fun publicKeyBlessing(bitstring):bitstring
+reduc forall blessing:bitstring, nm:bitstring, pk:bitstring,
+ cavs:bitstring, sgn:bitstring;
+ publicKeyBlessing(t(blessing, certificate(nm, pk, cavs, sgn))) = pk.
+
+(* verifyBlessing(blessing): Returns whether the certificate chain represented by
+ 'blessing' is cryptographically valid. *)
+pred verifyBlessing(bitstring).
+clauses
+ forall nm:bitstring, pk:bitstring, cavs:bitstring, sgn:bitstring;
+ verifySignature(pk, hash(t(t(t(null, nm), pk), cavs)), sgn)
+ -> verifyBlessing(t(null, certificate(nm, pk, cavs, sgn)));
+ forall b:bitstring,
+ nm:bitstring, pk:bitstring, cavs:bitstring, sgn:bitstring;
+ verifySignature(
+ publicKeyBlessing(b),
+ hash(t(hash(b), hash(t(t(t(null, nm), pk), cavs)))),
+ sgn
+ ) &&
+ verifyBlessing(b)
+ -> verifyBlessing(t(b, certificate(nm, pk, cavs, sgn))).
+
+(* newSelfBlessing(privateKey): Returns a new blessing with a single certificate
+ self-signed by the provided 'privateKey'. *)
+letfun newSelfBlessing(privKey:bitstring) =
+ new nm:bitstring;
+ new cavs:bitstring;
+ let pubKey = publicKey(privKey) in
+ let contentHash = hash(t(t(t(null, nm), pubKey), cavs)) in
+ let signature = sign(contentHash, privKey) in
+ let cert = certificate(nm, pubKey, cavs, sign(contentHash, privKey)) in
+ t(null, cert).
+
+(* bless(pubKey, withBlessing, withPrivKey): Returns a new blessing with a
+ certificate for 'pubKey' chained on to certificate chain represented by
+ 'withBlessing'. *)
+letfun bless(pubKey:bitstring, withBlessing:bitstring, withPrivKey:bitstring) =
+ new nm:bitstring;
+ new cavs:bitstring;
+ let contentHash = hash(t(t(t(null, nm), pubKey), cavs)) in
+ let signature = sign(hash(t(hash(withBlessing), contentHash)), withPrivKey) in
+ let cert = certificate(nm, pubKey, cavs, signature) in
+ t(withBlessing, cert).
+
+(* Authentication Protocol ----------------------------------------------------
+ Formalizes the Vanadium authentication protocol.
+------------------------------------------------------------------------------*)
+
+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, g_x:G, g_y:G, signature:bitstring) =
+ verifySignature(pubKey, hash(t(t(tag, gToBitstring(g_x)), gToBitstring(g_y))), signature).
+
+(* Public communication channel. *)
+free c:channel.
+free serverTag:bitstring.
+free clientTag:bitstring.
+free messageTag:bitstring.
+
+event acceptsServer(SymmetricKey, bitstring, bitstring).
+event acceptsClient(SymmetricKey, bitstring, bitstring).
+event termClient(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) =
+ new x:Exponent;
+ let g_x = exp(g, x) in
+ out(c, g_x);
+ in(c, 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).
+
+(* 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
+ if (
+ verifyBlessing(blessingClient) &&
+ verifyChannelBinding(pubKeyClient, clientTag, g_x, g_y, clientChBinding) &&
+ pubKeyClient = pubKeyExpected (* Verify if the client's blessings are authorized. *)
+ ) then
+ event acceptsServer(key, pubKeyClient, publicKeyBlessing(blessing));
+ (* Send secret message. *)
+ out(c, symmetricEncrypt(t(messageTag, secretMessage), key)).
+
+(* Protocol Process *)
+let authProtocol(
+ blessingClient:bitstring,
+ privKeyClient:bitstring,
+ blessingServer:bitstring,
+ privKeyServer:bitstring,
+ secretMessage:bitstring) =
+ let pubKeyClient = publicKeyBlessing(blessingClient) in
+ let pubKeyServer = publicKeyBlessing(blessingServer) in
+ client(blessingClient, privKeyClient, pubKeyServer) |
+ server(blessingServer, privKeyServer, pubKeyClient, 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.
+------------------------------------------------------------------------------*)
+
+free privKeyClient:bitstring [private].
+free privKeyServer:bitstring [private].
+free secretMessage:bitstring [private].
+
+let authProtocolInstance() =
+ 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) .
+
+(* 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 *)
+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 *)
+
+(* 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 *)
+
+(* 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 *)
+
+process authProtocolInstance()
\ No newline at end of file
