def xtsp.steal

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1519
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/xts.bend as T

1519# Ciphertext stealing undoes itself: the last whole block p and a tail tl
1520# (masked, fewer than 16 bytes), encrypted by steal_c and steal_t and
1521# decrypted by dsteal, come back as p's bytes and then tl
1522def xtsp.steal(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, ~inv: @k: K -> @b: M.CmBlock -> {dec(k, enc(k, b)) == b : M.CmBlock}, +k: K, +p: M.CmBlock, tl: List<&2, U32>, +t: M.CmBlock) -> {B.mask(tl) == tl : List<&2, U32>} -> {Nat.is_lt(B.len(tl), 16n) == True{} : Bool} -> {T.xts.dsteal(~K, ~dec, k, T.xts.steal_c(~K, ~enc, k, p, tl, t), T.xts.steal_t(~K, ~enc, k, p, tl, t), t) == M.cm.bytes_onto(p, tl) : List<&2, U32>}:
1523  match tl:
1524    case Nil{}:
1525      hm => hl => %Equal.sym(M.CmBlock, T.xts.bdec(~K, ~dec, k, T.xts.benc(~K, ~enc, k, p, t), t), p, xtsp.blk(~K, ~enc, ~dec, ~inv, k, p, t)) : {M.cm.bytes_of(_) == M.cm.bytes_onto(p, Nil{}) : List<&2, U32>}
1526        {==}
1527    case Con{+h, +r}:
1528      +hm => +hl => %Equal.sym(M.CmBlock, T.xts.bdec(~K, ~dec, k, T.xts.benc(~K, ~enc, k, M.cm.block_of(B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))), T.Xts.mul_alpha(t)), T.Xts.mul_alpha(t)), M.cm.block_of(B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))), xtsp.blk(~K, ~enc, ~dec, ~inv, k, M.cm.block_of(B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))), T.Xts.mul_alpha(t))) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, M.cm.block_of(B.append(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), B.drop(B.len(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))), M.cm.bytes_of(_)))), t), B.take(B.len(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))), M.cm.bytes_of(_))) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
1529              %Equal.sym(Nat, B.len(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))), B.len(Con{h, r}), li.len_take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))(na.lt_le(B.len(Con{h, r}), 16n)(hl))) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, M.cm.block_of(B.append(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), B.drop(_, M.cm.bytes_of(M.cm.block_of(B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))))))), t), B.take(_, M.cm.bytes_of(M.cm.block_of(B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))))))) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
1530              %Equal.sym(List<&2, U32>, M.cm.bytes_of(M.cm.block_of(B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))))), B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))), xtsp.ppY(Con{h, r}, T.xts.benc(~K, ~enc, k, p, t), hm, hl)) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, M.cm.block_of(B.append(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), B.drop(B.len(Con{h, r}), _))), t), B.take(B.len(Con{h, r}), _)) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
1531              %Equal.sym(List<&2, U32>, B.take(B.len(Con{h, r}), B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))), Con{h, r}, li.take_append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, M.cm.block_of(B.append(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), B.drop(B.len(Con{h, r}), B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))))), t), _) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
1532              %Equal.sym(List<&2, U32>, B.drop(B.len(Con{h, r}), B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))), B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), li.drop_append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, M.cm.block_of(B.append(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), _)), t), Con{h, r}) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
1533              %Equal.sym(List<&2, U32>, B.append(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)), BL.take_drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, M.cm.block_of(_), t), Con{h, r}) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
1534              %Equal.sym(M.CmBlock, M.cm.block_of(M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), T.xts.benc(~K, ~enc, k, p, t), sp.block_bytes(T.xts.benc(~K, ~enc, k, p, t))) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, _, t), Con{h, r}) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
1535              %Equal.sym(M.CmBlock, T.xts.bdec(~K, ~dec, k, T.xts.benc(~K, ~enc, k, p, t), t), p, xtsp.blk(~K, ~enc, ~dec, ~inv, k, p, t)) : {M.cm.bytes_onto(_, Con{h, r}) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
1536        {==}
Uses (29)

Used by (1)

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