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