LAWS_padded.bend

bend-osdev-cbc@0.1.0.0 · 23 lines · 1 definition

1# CBC with PKCS #7 padding (cbc.bend's encrypt_padded and decrypt_padded):
2# decryption undoes encryption for every message, of any length. The law
3# rests on LAWS.bend's cbc_round_trip and bend-osdev-pkcs7's laws, so it is
4# in a pair of its own (CONVENTIONS.md, Laws): a proof that uses only the
5# block and byte round trips takes in none of pkcs7's proofs.
6import Base
7import bend-osdev-bytes@0.1.1.0/bytes.bend as B
8import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
9import bend-osdev-cbc@0.1.0.0/cbc.bend as C
10
11# for every cipher and key with inv (as LAWS.bend's laws take it), every
12# 16-byte IV and every message: encryption succeeds and decryption gives the
13# message back
14law cbc_padded_round_trip:
15  for ~K: Data
16  for ~enc: K -> M.CmBlock -> M.CmBlock
17  for ~dec: K -> M.CmBlock -> M.CmBlock
18  for +k: K
19  for inv: @xs: List<&2, M.CmBlock> -> {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs : List<&2, M.CmBlock>}
20  for +iv: B.Octets
21  for +m: B.Octets
22  for hi: {B.Octets.len(iv) == 16n : Nat}
23  {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.Cbc.encrypt_padded(~K, ~enc, k, iv, m), c => C.Cbc.decrypt_padded(~K, ~dec, k, iv, c)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}