bend-osdev-cipher-modes

Releases (1)

• 0.1.0.0 indexed

Definitions (444)

LAWS.bend

• law cbc_blocks_round_tripCBC on blocks: decryption undoes encryption, for every key, IV and message
• law cbc_round_tripCBC on bytes: for every 16-byte IV and every message of whole blocks, encryption succeeds and decryption gives the message back
• law xts_blocks_round_tripXTS on blocks: decryption undoes encryption, for every data key and every starting tweak (T_0 = Xts.tweak(k2, i), so every k2 and i are covered)
• law cmac_streamingCMAC in pieces: the state after a ++ b is the state after a, then b, for every cipher, key and state (so start, update ..
• law xts_round_tripXTS on bytes, with ciphertext stealing: for every 16-byte sequence number and every data unit of at least 16 bytes, encryption succeeds and decryption gives the data unit back
• law ccm_round_tripCCM: decryption accepts what encryption produced and gives the message back, for every cipher, key, tag length, nonce, associated data and message; when the parameters are refused, both refuse alike
• law block_octets_round_tripA block written as Octets reads back as the same block, for every block
• law aes128_fips197_c1FIPS 197 Appendix C.1: the named default cipher (AES-128) encrypts one block
• law aes_bad_key_lengtha key of a length AES-128 and AES-256 do not have is refused
• law cbc_sp800_38a_f21_block1NIST SP 800-38A Appendix F.2.1, CBC-AES128: its first block
• law cbc_not_whole_blocksthe byte layer refuses a message that is not whole blocks, and a short IV
• law cbc_short_iv
• 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
• law xts_shorta data unit shorter than a block is refused
• law xts_sectorthe sequence number of sector n: n little-endian, zero-filled to 16 bytes
• law ccm_bad_tag_lengtha tag of odd length, and a nonce of 6 bytes, are refused
• law ccm_bad_nonce_length
• law cmac_rfc4493_k1RFC 4493 section 4: the AES-CMAC subkey K1

PROOF.bend

• def bx.bool
• def bx.word
• def bx.u32
• def bx.blockxor(a, xor(a, b)) == b on blocks
• def bits.word_bytes
• def bits.byte0_word
• def bits.byte1_word
• def bits.byte2_word
• def bits.byte3_word
• def bits.byte_b0
• def bits.byte_b1
• def bits.byte_b2
• def bits.byte_b3
• def bits.byte_byte
• def sp.cons_blocks
• def sp.cons_tail
• def sp.eta
• def sp.disc
• def sp.absurd
• def sp.absurd_tail
• def sp.snd_go
• def sp.mod16
• def bo.disc
• def bo.empty
• def bo.absurd
• def li.mask_mask
• def li.take_append
• def li.drop_append
• def li.mask_append
• def li.mask_drop
• def li.mask_take
• def li.len_append
• def li.len_drop
• def li.len_take
• def na.add_sub
• def na.lt_le
• def sp.hd
• def sp.tl
• def sp.blksplitting the bytes of a block gives the block back
• def sp.mask_blkthe bytes of a block are bytes: masking changes nothing
• def sp.blk16the block of 16 bytes, as bytes again
• def sp.join_splita masked list is its blocks and its tail joined back
• def sp.mod_taila list of whole blocks splits with no tail
• def sp.blk16gthe bytes of the block of any 16 values are those values, masked
• def sp.tail_shortthe tail of a split has fewer than 16 bytes
• def sp.tail_maskedthe tail of a masked split is masked
• def sp.nonemptya byte string of at least 16 bytes has a first block
• def sp.short_splitfewer than 16 bytes are all tail
• def sp.bb16a block of exactly 16 bytes gives them back, masked
• def sp.block_bytesthe block of a block's bytes is the block
• def sp.split_join
• def sp.mask_join
• def oc.maskedEvery Octets is masked: to_list(o) = to_list(of_list(to_list(o))) = mask(to_list(o))
• def oc.len
• def oc.mod
• def cbcp.iva 16-byte IV is the block of its bytes
• def tr.add_succ
• def tr.add_zero
• def tr.rr
• def tr.append_eq
• def tr.len_go
• def tr.len_eq
• def tr.split_fin
• def tr.split_fin_cons
• def tr.split_fin_nil
• def tr.split_go
• def tr.split_eq
• def tr.join_go
• def tr.join_eq
• def tr.cbc_enc_go
• def tr.cbc_enc_eq
• def tr.cbc_dec_go
• def tr.cbc_dec_eq
• def tr.xts_enc_go
• def tr.xts_enc_eq
• def tr.xts_dec_go
• def tr.xts_dec_eq
• def tr.init_go