scimp_key_neg_key_erasure.pv

(*

Formal analysis of the Silent Cirlce Instant Messaging Protocol (SCIMP).

Author:        Sebastian Verschoor
Email:         s.r.verschoor@student.tue.nl
Last modified: <2015-10-08 14:52:40>

This file checks that if key material gets compromised after rekeying, 
this does not compromise old key material.

The description for the protocol was taken from the protocol description at:
https://github.com/SilentCircle/silent-text/tree/master/Documentation
A more informal description is given at:
https://silentcircle.com/scimp-protocol

Proverif version used: 1.90 (retrieved at 2015-07-06)

*** Short protocol description ***

Initiator Alice (A)
Responder Bob (B)
ECDHE-exchange using a fixed base point G
Alice and Bob share the cached secret cs

A      : skI    := random()
         pkI    := skI * G
A  -> B: commit  = (#pkI, MAC(cs, (#pkI, "Initiator")))
      B: skR    := random()
         pkR    := skR * G
A <-  B: dh1     = (pkR, MAC(cs, (#pkR, "Responder")))
A      : validate hcsr (= MAC in dh1); or abort
         kdk2   := MAC(MAC(htotal, Z), (CONSTS, context, cs))
                   where htotal  = #(commit, dh1, pkI)
                         Z       = skI * pkR
                         context = (A, B, htotal)
         extract from kdk2 and session variables:
           ksnd, krcv, maci, macr, sasi, cs1, isnd, ircv
A  -> B: dh2     = (pkI, maci)
      B: validate pkI with #pkI of commit; or abort
         validate hcsi (= MAC in commit); or abort
         kdk2   := MAC(MAC(htotal, Z), (CONSTS, context, NULL))
                   where htotal  = #(commit, dh1, pkI)
                         Z       = skR * pkI
                         context = (A, B, htotal)
         extract from kdk2 and session variables:
           krcv, ksnd, macr, maci, sasr, cs1, ircv, isnd
A <-  B: commit  = macr

*)

(*** Types ***)

type mac_key.
type secret_key.
type nonce.
type point.
type scalar.
type identity.

fun mk2bs(mac_key)    : bitstring       [data, typeConverter].
fun bs2mk(bitstring)  : mac_key         [data, typeConverter].
fun sk2bs(secret_key) : bitstring       [data, typeConverter].
fun bs2sk(bitstring)  : secret_key      [data, typeConverter].
fun pt2bs(point)      : bitstring       [data, typeConverter].
fun bs2n (bitstring)  : nonce           [data, typeConverter].
fun sk2mk(secret_key) : mac_key         [data, typeConverter].
fun mk2sk(mac_key)    : secret_key      [data, typeConverter].


(*** Functions ***)

fun increment(bitstring) : bitstring [data].

fun splitFst(bitstring) : bitstring.
fun splitSnd(bitstring) : bitstring.
reduc forall x:bitstring;
      unsplit(splitFst(x), splitSnd(x)) = x.

fun getCS(identity, identity) : bitstring [private].
equation forall x:identity, y:identity;
         getCS(x, y) = getCS(y, x).

(* Cryptographic functions *)

fun hash(bitstring) : bitstring.

(* Message authentication code (MAC) *)
fun mac(mac_key, bitstring) : bitstring.

(* Key derivation function (KDF) *)
reduc forall key:mac_key, context:bitstring, label:bitstring;
      kdf(key, label, context) = mac(key, (label, context)).

(* Symmetric encryption/decryption *)
fun sym_enc(secret_key, nonce, bitstring) : bitstring.
fun sym_dec(secret_key, nonce, bitstring) : bitstring.
equation forall k:secret_key, n:nonce, m:bitstring;
         sym_dec(k, n, sym_enc(k, n, m)) = m.
equation forall k:secret_key, n:nonce, m:bitstring;
         sym_enc(k, n, sym_dec(k, n, m)) = m.

(* Authenticated Encryption with Additional Data *)
letfun aead_enc(k:secret_key, n:nonce, header:bitstring, plaintext:bitstring) =
       let tag = mac(sk2mk(k), (n, header, plaintext)) in
       sym_enc(k, n, (plaintext, tag)).
letfun aead_dec(k:secret_key, n:nonce, header:bitstring, ciphertext:bitstring) =
       let (plaintext:bitstring, tag:bitstring) = sym_dec(k, n, ciphertext) in
       let (=tag) = mac(sk2mk(k), (n, header, plaintext)) in
       plaintext.


(* Diffie-Hellman-Merkle key exchange
 * Proverif does not care about the underlying group, so there is no need to
 * encode ECDH any different.
 *)
const Base : point [data].
fun mult(scalar, point) : point.

equation forall x:scalar, y:scalar;
         mult(x, mult(y, Base)) = mult(y, mult(x, Base)).


(*** Communication channels ***)

(* Public channel over which the protocol is executed. Usually the internet. *)
free ch:channel.

(*** Constants ***)

(* Null (replacement for cached secret when there is none) *)
const Null            : bitstring [data].

(* String constants *)
const InitStr         : bitstring [data]. (* "Initiator" *)
const RespStr         : bitstring [data]. (* "Responder" *)
const MasterStr       : bitstring [data]. (* "MasterSecret" *)
const AlgId           : bitstring [data]. (* "SCimp-ENHANCE" *)

(* Labels for key derivation *)
const InitMasterLabel : bitstring [data]. (* "InitiatorMasterKey" *)
const RespMasterLabel : bitstring [data]. (* "ResponderMasterKey" *)
const InitMACLabel    : bitstring [data]. (* "InitiatorMACkey" *)
const RespMACLabel    : bitstring [data]. (* "ResponderMACkey" *)
const SasLabel        : bitstring [data]. (* "SAS" *)
const CsLabel         : bitstring [data]. (* "RetainedSecret" *)
const InitIndexLabel  : bitstring [data]. (* "InitiatorInitialIndex" *)
const RespIndexLabel  : bitstring [data]. (* "ResponderInitialIndex" *)
const MsgKeyLabel     : bitstring [data]. (* "MessageKey" *)

(* Identity of an adversary *)
const Compromised : identity [data].

(*** Queries ***)

(* Hint for the prover *)
not attacker(new ski).
not attacker(new skr).

(* Queries for confidentiality *)
free csInitFlag, csRespFlag : bitstring [private].
query attacker(csInitFlag); attacker(csRespFlag).

(* Query reachability: check for typos. This should result in
   not attacker(....HasTypo[]) is false. *)
free initHasTypo, respHasTypo : bitstring [private].
query attacker(initHasTypo); attacker(respHasTypo).


(*** Processes ***)

(* Role of the initiator *)
let processInitiator(init:identity, resp:identity, cs:bitstring) =
  (* Commit *)
  new ski : scalar;
  let pki    = mult(ski, Base) in
  let hpki   = hash(pt2bs(pki)) in
  let hcsi   = mac(bs2mk(cs), hash((pki, InitStr))) in
  let commit = (hpki, hcsi) in
  out(ch, commit);

  (* DH1 *)
  in(ch, dh1:bitstring);
  let (pkr:point, hcsr:bitstring) = dh1 in
  if hcsr = mac(bs2mk(cs), hash((pkr, RespStr))) then

  (* DH2 *)
  let z       = mult(ski, pkr) in
  let htotal  = hash((commit, dh1, pki)) in
  let kdk     = bs2mk(mac(bs2mk(htotal), pt2bs(z))) in
  let context = (init, resp, htotal) in
  let sessId  = hash((init, resp)) in
  let kdk2    = bs2mk(mac(kdk, (MasterStr, AlgId, context, cs))) in
  let ksnd    = kdf(kdk2, InitMasterLabel, context) in
  let krcv    = kdf(kdk2, RespMasterLabel, sessId) in
  let sas     = kdf(kdk2, SasLabel,        context) in
  let cs1     = kdf(kdk2, CsLabel,         context) in
  let isnd    = kdf(kdk2, InitIndexLabel,  sessId) in
  let ircv    = kdf(kdk2, RespIndexLabel,  sessId) in
  let macr    = kdf(kdk2, RespMACLabel,    context) in
  let maci    = kdf(kdk2, InitMACLabel,    context) in
  out(ch, (pki, maci));

  (* Confirm *)
  in(ch, =macr);

  (* Compromise key material *)
  out(ch, kdk2);
  
  (* Publish secret values to test secrecy *)
  out(ch, sym_enc(bs2sk(cs), bs2n(Null), csInitFlag))

  (* Check for typos *)
  ; out(ch, initHasTypo)

  .

(* Role of the responder *)
let processResponder(init:identity, resp:identity, cs:bitstring) =
  (* Commit *)
  in(ch, commit:bitstring);
  let (hpki:bitstring, hcsi:bitstring) = commit in

  (* DH1 *)
  new skr : scalar;
  let pkr  = mult(skr, Base) in
  let hpkr = hash(pt2bs(pkr)) in
  let hcsr = mac(bs2mk(cs), hash((pkr, RespStr))) in
  let dh1  = (pkr, hcsr) in
  out(ch, dh1);

  (* DH2 *)
  in(ch, (pki:point, maci:bitstring));
  let (=hpki) = hash(pt2bs(pki)) in
  if hcsi = mac(bs2mk(cs), hash((pki, InitStr))) then

  (* Confirm *)
  let z       = mult(skr, pki) in
  let htotal  = hash((commit, dh1, pki)) in
  let kdk     = bs2mk(mac(bs2mk(htotal), pt2bs(z))) in
  let context = (init, resp, htotal) in
  let sessId  = hash((init, resp)) in
  let kdk2    = bs2mk(mac(kdk, (MasterStr, AlgId, context, cs))) in
  let ksnd    = kdf(kdk2, RespMasterLabel, sessId) in
  let krcv    = kdf(kdk2, InitMasterLabel, context) in
  let sas     = kdf(kdk2, SasLabel,        context) in
  let cs1     = kdf(kdk2, CsLabel,         context) in
  let (=maci) = kdf(kdk2, InitMACLabel,    context) in
  let macr    = kdf(kdk2, RespMACLabel,    context) in
  let isnd    = kdf(kdk2, RespIndexLabel,  sessId) in
  let ircv    = kdf(kdk2, InitIndexLabel,  sessId) in
  out(ch, macr);

  (* Compromise key material *)
  out(ch, kdk2);
  
  (* Publish secret values to test secrecy *)
  out(ch, sym_enc(bs2sk(cs), bs2n(Null), csRespFlag))

  (* Check for typos *)
  ; out(ch, respHasTypo)

  .


(*** Main ***)

process
  (* Allow arbitrary many protocol runs *)
  !
  (* Let the adversary decide who will engage in rekeying *)
  in(ch, (init:identity, resp:identity));
  (* Get their cached secret *)
  let cs = getCS(init, resp) in
  
  processInitiator(init, resp, cs) |
  processResponder(init, resp, cs)