proofs/authentication/protocol.pv

(* 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()