bend-osdev-aead

Releases (1)

• 0.1.0.0 indexed

Definitions (226)

aead.bend

• type AdSplitA ciphertext and its tag, split from the bytes of both (the tag the last tlen bytes; CrTooShort for fewer than tlen bytes)
• def ad.split.pick
• def AdTag.split
• def AdTag.jointhe ciphertext with its tag appended
• def AdTag.is_eqWhether two tags are equal, every byte compared (no early exit)

aegis128.bend

• type AdAegisStThe state (internal)
• def ad.ae.update
• def ad.ae.zthe keystream block S1 xor S4 xor (S2 and S3)
• def ad.ae.c0const0 and const1 (the Fibonacci sequence mod 256)
• def ad.ae.c1
• def ad.ae.init.go
• def ad.ae.init
• def ad.ae.absorbthe state after the associated data's 16-byte pieces (the last zero-padded)
• type AdAegisRunThe message, a byte at a time (internal): the state, the keystream bytes left of the current block, the current block's plaintext bytes so far (last first) and how many
• def ad.ae.run0
• def ad.ae.rev
• def ad.ae.tail
• def ad.ae.head
• def ad.ae.step.pick
• def ad.ae.stepthe run after the plaintext byte x
• def ad.ae.zheadthe next keystream byte
• def ad.ae.flush.pick
• def ad.ae.flushthe state after the last, short block (zero-padded)
• def ad.ae.eout
• def ad.ae.eafter
• def ad.ae.dout
• def ad.ae.dafter
• type AdAegisOutThe loops that run (tail calls): the run after the bytes, and the output
• def ad.ae.ego
• def ad.ae.dgo
• def ad.ae.fin.goFinalization: the tag from the state after the message, and the lengths
• def ad.ae.tag
• def ad.ae.w64n as a 64-bit word, counted up (W64.from_nat divides by 2^32, a literal the checker would expand when a proof meets it)
• def ad.ae.bitsthe bit length of n bytes as 8 little-endian bytes
• def ad.ae.s3
• def ad.ae.final
• type AdAegisKeyAn AEGIS-128 key: the key block and the AES S-box (opaque)
• def ad.ae.key.pick
• def ad.ae.key
• def AdAegis128.keya 16-byte key
• def ad.ae.startthe run before the message: the state after the key, nonce and associated data
• def ad.ae.sealed
• def ad.ae.seal.go
• def ad.ae.nonce
• def ad.ae.seal
• def AdAegis128.sealp sealed under a 16-byte nonce: the ciphertext and the 16-byte tag
• def ad.ae.tag_of.of
• def ad.ae.tag_of.go
• def AdAegis128.tag_ofThe tag open expects for the ciphertext c (without its tag)
• def ad.ae.plain.of

LAWS.bend

• law aegis128_round_trip
• law aegis128_tampera tag of 16 bytes other than the one AEGIS-128 computes for the ciphertext is refused, under a 16-byte nonce
• law aesround_rfc10032RFC 10032, Appendix A.1: AESRound(000102..0f, 101112..1f) = 7a7b4e5638782546a8c0477a3b813f43
• law authenc_round_trip_if
• law authenc_tampera tag of tlen bytes other than the computed one is refused, and the cipher never runs
• law essiv_round_trip_if
• law essiv_aead_round_trip_if
• law seqiv_round_trip_if
• law echainiv_round_trip_if

PROOF.bend

• def byte_xor_byteBEGIN GENERATED by gen/proof.py: bits the low byte of a XOR depends only on the low byte of its first operand
• def be32_lena word's big-endian bytes are four
• def byte_bytea byte masked again is itself
• def bool_xx
• def word_xx
• def u32_xx
• def byte_xx
• def nat_add_zero
• def nat_add_succ
• def nat_sub_zero
• def nat_sub_add
• def nat_lt_zero
• def nat_lt_add
• def len_append
• def mask_len
• def olen_ofthe length of a list made Octets
• def olen_appendthe length of a joined string
• def split_joinA ciphertext joined with its tag splits back into the two
• def is_eq_refl
• def seqiv_r
• def echainiv_r
• def fit_len
• def au_tag_lenevery tag has tlen bytes
• def authenc_r
• def ego_ref
• def dgo_ref
• def dec_enc_afterdecryption runs through the states encryption ran through, and gives the message's bytes back
• def dec_enc_out
• def mask_eoutthe ciphertext's bytes are bytes, and as many as the message's
• def len_eout
• def blk_lenevery tag has 16 bytes
• def tag_len
• def fin_len
• def seal_ok
• def seal_bad
• def open_ok
• def nonce_ok
• def seal_go_eq
• def tag_of_eq
• def plain_eq
• def aegis_rt