(* Encrypt-then-MAC example *) param n. type mkey [bounded]. type mkeyseed [fixed]. type key [fixed]. type keyseed [fixed]. type seed [fixed]. type macs [bounded]. fun k2b(key):bitstring [compos]. (* Shared-key encryption (CPA Stream cipher) *) proba Penc. expand IND_CPA_sym_enc(keyseed, key, bitstring, bitstring, seed, kgen, enc, dec, injbot, Z, Penc). (* The function Z returns for each bitstring, a bitstring of the same length, consisting only of zeroes. *) const Zk:bitstring. forall y:key; Z(k2b(y)) = Zk. (* Mac *) proba Pmac. expand UF_CMA_mac(mkeyseed, mkey, bitstring, macs, mkgen, mac, verify, Pmac). (* Queries *) query secret1 k''. query secret k''. channel cA, cB, start, c. let QA = ! i <= n in(cA, ()); new k' : key; new r'' : seed; let m = enc(k2b(k'), k, r'') in out(cA, (m, mac(m, mk))). let QB = ! i' <= n in(cB, (m':bitstring, ma:macs)); if verify(m', mk, ma) then let injbot(k2b(k'':key)) = dec(m', k) in out(cB, ()). process in(start, ()); new r: keyseed; let k = kgen(r) in new r': mkeyseed; let mk = mkgen(r') in out(c, ()); (QA | QB)