(* Vanadium Authentication Protocol --------------------------------------------

Informal Protocol Specification:
D is Dialer, A is Acceptor
D         : Dialer
A         : Acceptor

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:

D generates x, and A generates y

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
    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 dialer's and acceptor's blessings.

(2) Channel Secrecy
    A 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 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.
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 [data].

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

(* Type Conversion -----------------------------------------------------------*)
fun keyToBitstring(SymmetricKey):bitstring [data].

(* 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, binding:bitstring) =
   sign(hash(t(tag, binding)), privKey).

letfun verifyChannelBinding(pubKey:bitstring, tag:bitstring, binding:bitstring, signature:bitstring) =
   verifySignature(pubKey, hash(t(tag, binding)), 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 *)

free acceptorTag:bitstring.
free dialerTag:bitstring.
free messageTag:bitstring.

event acceptsAcceptor(SymmetricKey, bitstring, bitstring).
event acceptsDialer(SymmetricKey, bitstring, bitstring).
event termDialer(SymmetricKey, bitstring, 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(outCh, g_x) | 
   in(inCh, g_y:G);
   let key = generateKey(gToBitstring(exp(g_y, x))) in
   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)).

(* 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(blessing) &&
      verifyChannelBinding(pubKey, tag, binding, chBinding)
   ) then
   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(aToDCh, symmetricEncrypt(t(messageTag, secretMessage), key)).

(* Protocol Process *)
let handshake(
    blessingDialer:bitstring,
    privKeyDialer:bitstring,
    blessingAcceptor:bitstring,
    privKeyAcceptor:bitstring,
    secretMessage:bitstring) =
   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 dialer and
   acceptor blessings and formalizes the desired correctness properties -- mutual
   authentication, channel secrecy and dialer privacy.
------------------------------------------------------------------------------*)

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) .

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

(* Channel Secrecy *)
query attacker(secretMessage).  (* Desired ProVerif output: not attacker(secretMessage) is true *)
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 *)

process handshakeInstance()