This project defines a formalization of the Vanadium authentication protocol and verifies the desired security properties for it using the automatic cryptographic protocol verifier ProVerif.
The authentication protocol is used during a Vanadium 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).
The design of the protocol is very similar to the SIGMA-I protocol from the literature. It involves a Diffie-Hellman key exchange, 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 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. The only way to guarantee security of a protocol is to formally specify it and mathematically prove its security properties.
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. We refer the reader to the ProVerif manual for the authoritative definition of the language.
ProVerif analyzes protocols in the symbolic, 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.
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.
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 requires installing the ProVerif tool. Instructions for installing the tool can be found here
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
The aforesaid command prints out a bunch of ProVerif messages (we recommend reading Section 3 of the 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.