Encoding separation for mac logs in UF1CMA

Consider the case where AEAD.encrypt is called with a nonce n, where n is fresh for the aead table, but exists in the prf_table with an unused mac. This is, of course, the case enabled by Plan A which was excluded by Plan B and arises when decrypt precedes encrypt.

Assume we have the invariant initially.

In the course of encrypt, we call CMA.mac, which modifies the mac log associated with nonce n.

In order to re-establish the invariant, we have to show that this assignment does not disturb the state of any other mac log.

Intuitively, what we need is a separation property that ensures that all mac logs in the prf table are pairwise distinct. One way to do this is to explicitly refine the type of a prf table with an double quantifier, saying that, well, every pair of mac entries have distinct mac logs. As you can imagine, we want to avoid this double quantifier.

So, here's our proposed change to Crypto.Symmetric.UF1CMA.

1. Recall that CMA.id is a pair of an id and a nonce.

2. Let's index the type of a mac entry with its id

type log (i:id) = (j:UInt128.t{j=snd i} * option (text * tag))

Notice that beyond the indexing, we actually want to change the representation of mac log entries to contain their associated nonce.

3. log_cmp, the pre-order on mac logs is essentially unchanged. Note, we don't have to say anything about the evolution of the first component of a log entry, since it is a singleton type.

  match snd a, snd b with
  | Some (l,t) , Some (l',t') -> l == l' /\ t == t'
  | None, _                   -> True
  | _                         -> False

4. Now, we build the type of CMA.state to include these indexed logs.

let log_ref (r:erid) (i:id) = if mac_log then ideal_log r i else unit

let ilog (#r:erid) (#i:id) (l:log_ref r i{mac_log}) : Tot (ideal_log r i) = l

noeq type state (i:id) =
  | State:
    #region: erid ->
    r: MAC.elemB i{Buffer.frameOf (MAC.as_buffer r) == region} ->
    s: wordB_16{frameOf s == region /\ disjoint (MAC.as_buffer r) s} ->
    log: log_ref region i ->
    state i

Let's see now how this helps us restore the AEAD invariant.

We know that in AEAD.encrypt, the call to CMA.mac only changes the mac log associated to the input nonce n, i.e., in the current state it contains a pair whose first component is (id, n).

Every other mac log in the table is a reference that contains in the current state a pair whose first component is (id, n'), for some n' <> n, and hence must be separate from the particular mac entry that we just modified.

More concretely, the following lemma is now provable in F*:

val lemma_mac_log_framing
  (#i:id)
  (nonce_1:Cipher.iv (alg i){safeId i})
  (nonce_2:Cipher.iv (alg i){nonce_1 <> nonce_2})
  (mac_st_1:CMA.state (i, nonce_1))
  (mac_st_2:CMA.state (i, nonce_2){CMA.(mac_st_2.region) = CMA.(mac_st_1.region)})
  (h0 h1:mem) : Lemma
  (requires (m_contains (CMA.(ilog mac_st_1.log)) h0  /\ 
             m_contains (CMA.(ilog mac_st_2.log)) h0  /\
	     HS.modifies (Set.as_set [CMA.(mac_st_1.region)]) h0 h1 /\
             HS.modifies_ref (CMA.(mac_st_1.region)) !{HS.as_ref (as_hsref (CMA.(ilog mac_st_1.log)))} h0 h1))
  (ensures  (m_sel h0 (CMA.(ilog mac_st_2.log)) = m_sel h1 (CMA.(ilog mac_st_2.log))))
let lemma_mac_log_framing #i nonce_1 nonce_2 mac_st_1 mac_st_2 h0 h1 = ()