bend-osdev-pkcs7

Releases (1)

• 0.1.0.0 indexed

Definitions (68)

check.bend

• def err
• def res
• def backwhether r is m
• def bytes.gon pseudo-random bytes (a linear congruential generator)
• def msg
• def iv
• def main

LAWS.bend

• law pkcs7_round_tripUnpadding undoes padding, for every block size bs and message m: when bs is one the padding takes (1 to 255), unpad(pad(m)) is m; when it is not, both refuse alike (CmBadBlockSize)
• law pkcs7_pad_blocksA padded message is a whole number of blocks, for every block size and message
• law pkcs7_pad_emptyPKCS #7 (RFC 5652, 6.3): the empty message becomes a whole block of 16s; 15 bytes gain one 1
• law pkcs7_pad_15
• law pkcs7_unpad_15
• law pkcs7_unpad_zeroa last byte of 0, or one the bytes before it contradict, is bad padding
• law pkcs7_unpad_mixed

pkcs7.bend

• def pkcs7.filln bytes of value v
• def pkcs7.size_ok
• def pkcs7.pad.octm and its padding (on Octets, so that a long message is not walked as a list: Bend 2.0.37's runtime overflows its stack on deep structural recursion)
• def Pkcs7.pad.go
• def Pkcs7.padm padded to a whole number of bs-byte blocks
• def pkcs7.diff0 when every byte of xs is v
• def pkcs7.lastthe last byte, or d if there is none
• def pkcs7.strip
• def pkcs7.unpad.octthe value p of the last byte must be 1 to bs, and the last p bytes all p (on Octets of n bytes, so that only those p bytes become a list)
• def Pkcs7.unpad.go
• def Pkcs7.unpadm without its padding; m must be a non-empty whole number of blocks

PROOF.bend

• def pk.disc
• def pk.empty
• def pk.absurd
• def pk.sub_zero
• def pk.add_sub(L + k) - k is L
• def pk.le_step
• def pk.le_subq - r <= q
• def pk.sub_succr <= q gives (1 + q) - r = 1 + (q - r)
• def pk.le_trans
• def pk.le0
• def pk.lt0
• def pk.lt_le
• def pk.go_skip1 + m + x steps from (m, d, r) take one wrap and leave x
• def pk.sub_add_r(1 + m + r) - r = 1 + m
• def pk.mod_lethe remainder is at most q
• def pk.mod_pada + (1 + q - (a mod (1 + q))) is a multiple of 1 + q
• def pk.fill_len
• def pk.mask_fill
• def pk.drop_fill
• def pk.bbBEGIN GENERATED by gen/pkcs7_proof.py: bits a byte's byte is itself
• def pk.wselfa word XOR itself is zero, bit by bit
• def pk.xor_self
• def pk.diff_fillthe padding's difference from its own byte is 0
• def pk.u8.c7BEGIN GENERATED by gen/pkcs7_proof.py: u8 the values 224 to 255
• def pk.u8.c6the values 192 to 223
• def pk.u8.c5the values 160 to 191
• def pk.u8.c4the values 128 to 159
• def pk.u8.c3the values 96 to 127
• def pk.u8.c2the values 64 to 95
• def pk.u8.c1the values 32 to 63
• def pk.u8the values 0 to 31
• def pk.ugPkcs7.unpad's checks and its unpad.oct, with what they compute as arguments, so that each can be rewritten on its own
• def pk.k2
• def pk.k
• def pk.padthe padding of 1 + p1 bytes
• def pk.atits last byte, at L + p1 of m and it
• def pk.lenthe padded message's length
• def pk.octunpad.oct on m and a padding of 1 + p1 bytes (p1 below 255) gives m
• def pk.main2the round trip for a block size 1 + q (q below 255) and a padding of 1 + p1 bytes, p1 <= q, that makes whole blocks
• def pk.hm1 + L + (q - L mod (1 + q)) is a multiple of 1 + q
• def pk.main
• def pk.rt
• def pk.blocks