def ccmp.main

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1850
import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL
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

1850# decryption accepts what encryption produced, whatever the parameter checks answer
1851def ccmp.main(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +nonce: B.Octets, +aad: B.Octets, +p: B.Octets, r: Result<&2, &2, M.CmError, Unit>) -> {CC.ccm.checks(m, B.len(B.Octets.to_list(nonce)), B.len(B.Octets.to_list(p))) == r : Result<&2, &2, M.CmError, Unit>} -> {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, CC.ccm.e2(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p), r), c => CC.Ccm.decrypt.ref(~K, ~enc, k, m, nonce, aad, c)) == Result.map(&2, &2, M.CmError, B.Octets, B.Octets, c => p, CC.ccm.e2(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p), r)) : Result<&2, &2, M.CmError, B.Octets>}:
1852  match r:
1853    case Fail{e}:
1854      h => {==}
1855    case Done{+u}:
1856      +h => +hm = ccmp.tag_le(m, B.len(B.Octets.to_list(nonce)), B.len(B.Octets.to_list(p)), u, h)
1857        +leb = ccmp.len_eb(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p), hm)
1858        # decryption reads the ciphertext back, masked
1859        %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))))), B.mask(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), BL.octets_to_of(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))))) : {CC.ccm.d2(~K, ~enc, Nat.is_le(m, B.len(_)), k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), _) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1860        # which it already is
1861        %Equal.sym(List<&2, U32>, B.mask(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))), ccmp.mask_eb(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))) : {CC.ccm.d2(~K, ~enc, Nat.is_le(m, B.len(_)), k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), _) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1862        # it is longer than the tag
1863        %Equal.sym(Nat, B.len(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), Nat.add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m), leb) : {CC.ccm.d2(~K, ~enc, Nat.is_le(m, _), k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1864        # 
1865        %Equal.sym(Bool, Nat.is_le(m, Nat.add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m)), True{}, na.le_add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m)) : {CC.ccm.d2(~K, ~enc, _, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1866        # its body is as long as the message
1867        %Equal.sym(Nat, B.len(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), Nat.add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m), leb) : {CC.ccm.d3(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))), CC.ccm.checks(m, B.len(B.Octets.to_list(nonce)), Nat.sub(_, m))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1868        # 
1869        %Equal.sym(Nat, Nat.sub(Nat.add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m), m), B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), na.sub_add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m)) : {CC.ccm.d3(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))), CC.ccm.checks(m, B.len(B.Octets.to_list(nonce)), _)) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1870        # 
1871        %Equal.sym(Nat, B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), B.len(B.Octets.to_list(p)), ccmp.len_xcp(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), p)) : {CC.ccm.d3(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))), CC.ccm.checks(m, B.len(B.Octets.to_list(nonce)), _)) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1872        # so its checks pass as encryption's did
1873        %Equal.sym(Result<&2, &2, M.CmError, Unit>, CC.ccm.checks(m, B.len(B.Octets.to_list(nonce)), B.len(B.Octets.to_list(p))), Done{u}, h) : {CC.ccm.d3(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))), _) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1874        # the body and the tag apart
1875        %Equal.sym(Nat, B.len(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), Nat.add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m), leb) : {CC.ccm.open(M.cm.ct_eq(M.cm.xor_bytes(B.drop(Nat.sub(_, m), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.take(Nat.sub(_, m), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))))))), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.take(Nat.sub(_, m), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))))))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1876        # 
1877        %Equal.sym(Nat, Nat.sub(Nat.add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m), m), B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), na.sub_add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m)) : {CC.ccm.open(M.cm.ct_eq(M.cm.xor_bytes(B.drop(_, B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.take(_, B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))))))), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.take(_, B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))))))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1878        # 
1879        %Equal.sym(List<&2, U32>, B.take(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), li.take_append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))) : {CC.ccm.open(M.cm.ct_eq(M.cm.xor_bytes(B.drop(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(_)))), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(_))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1880        # 
1881        %Equal.sym(List<&2, U32>, B.drop(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), li.drop_append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))) : {CC.ccm.open(M.cm.ct_eq(M.cm.xor_bytes(_, M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))))))), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1882        # CTR undoes itself: the plaintext
1883        %Equal.sym(List<&2, U32>, CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))))), B.Octets.to_list(p), ccmp.xxp(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), p)) : {CC.ccm.open(M.cm.ct_eq(M.cm.xor_bytes(M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), _)), _) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1884        # the received tag, unmasked from S_0
1885        %Equal.sym(List<&2, U32>, M.cm.xor_bytes(M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), B.mask(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))), li.xor_xor(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))(ccmp.le_tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p), hm))) : {CC.ccm.open(M.cm.ct_eq(_, CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))), B.Octets.to_list(p)) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1886        # 
1887        %Equal.sym(List<&2, U32>, B.mask(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), ccmp.mask_tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))) : {CC.ccm.open(M.cm.ct_eq(_, CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))), B.Octets.to_list(p)) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1888        # matches the tag recomputed
1889        %Equal.sym(Bool, M.cm.ct_eq(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))), True{}, ccmp.ct_refl(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)))) : {CC.ccm.open(_, B.Octets.to_list(p)) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1890        # 
1891        %Equal.sym(B.Octets, B.Octets.of_list(B.Octets.to_list(p)), p, BL.octets_of_to(p)) : {Done{_} == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
1892        {==}
Uses (50)

Used by (1)

bend-osdev-cipher-modes@0.1.0.0/LAWS:ccm_round_trip