def ccmp.mask_tag

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1833

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-cipher-modes@0.1.0.0/ccm.bend as CC

1833def ccmp.mask_tag(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +l: Nat, +nv: List<&2, U32>, +av: List<&2, U32>, +pv: List<&2, U32>) -> {B.mask(CC.ccm.tag(~K, ~enc, k, m, l, nv, av, pv)) == CC.ccm.tag(~K, ~enc, k, m, l, nv, av, pv) : List<&2, U32>}:
1834  %Equal.sym(List<&2, U32>, B.mask(CC.ccm.tag(~K, ~enc, k, m, l, nv, av, pv)), B.take(m, B.mask(M.cm.bytes_of(CC.ccm.mac(~K, ~enc, k, m, l, nv, av, pv)))), li.mask_take(m, M.cm.bytes_of(CC.ccm.mac(~K, ~enc, k, m, l, nv, av, pv)))) : {_ == CC.ccm.tag(~K, ~enc, k, m, l, nv, av, pv) : List<&2, U32>}
1835  %Equal.sym(List<&2, U32>, B.mask(M.cm.bytes_onto(CC.ccm.mac(~K, ~enc, k, m, l, nv, av, pv), Nil{})), M.cm.bytes_onto(CC.ccm.mac(~K, ~enc, k, m, l, nv, av, pv), B.mask(Nil{})), sp.mask_blk(CC.ccm.mac(~K, ~enc, k, m, l, nv, av, pv), Nil{})) : {B.take(m, _) == CC.ccm.tag(~K, ~enc, k, m, l, nv, av, pv) : List<&2, U32>}
1836  {==}