bend-osdev-aes

Releases (1)

• 0.1.0.0 indexed

Definitions (138)

aes.bend

• def aes.xt
• def aes.gmul.go
• def aes.gmul
• def aes.inv.goa := a^2 * x, n times: from a = x, six times gives x^127
• def aes.invthe multiplicative inverse, x^254 (0 for 0)
• def aes.rotl
• def aes.isboxthe inverse S-box: the inverse affine map, then the inverse
• def aes.mask_weach byte's low 8 bits
• def aes.mask

LAWS.bend

• law aes_round_tripAES (aes.bend): decryption undoes encryption, for every key (every value of CmAesKey, whatever its number of rounds and round keys: AES-128, AES-192 and AES-256 among them) and every block
• law aes128_fips197_c1FIPS 197 Appendix C.1: the named default cipher (AES-128) encrypts one block

PROOF.bend

• def sp.blk16g
• def bx.ru32
• def ap.nth
• def ap.pick
• def ap.bridge
• def ap.e_sbl
• def ap.sbl
• def ap.e_sbi
• def ap.sbi
• def ap.ex2.l
• def ap.ex2.r
• def ap.ex2
• def ap.xtb
• def ap.m3b
• def ap.m9b
• def ap.m11b
• def ap.m13b
• def ap.m14b
• def ap.col00
• def ap.col01
• def ap.col02
• def ap.col03
• def ap.col10
• def ap.col11
• def ap.col12
• def ap.col13
• def ap.col20
• def ap.col21
• def ap.col22
• def ap.col23
• def ap.col30
• def ap.col31
• def ap.col32
• def ap.col33
• def ap.fin0
• def ap.fin1
• def ap.fin2
• def ap.fin3
• def ap.bb
• def ap.xorb
• def ap.bylo
• def ap.isb
• def ap.gx
• def ap.mx
• def ap.glo
• def ap.m9
• def ap.m11
• def ap.m13
• def ap.m14
• def ap.xg0
• def ap.xg
• def ap.imixg
• def ap.swap4
• def ap.trans
• def ap.row
• def ap.out0
• def ap.out1
• def ap.out2
• def ap.out3
• def ap.mixc
• def ap.rowb0
• def ap.rowb1
• def ap.rowb2
• def ap.rowb3
• def ap.mixcb
• def ap.ark2
• def ap.shift
• def ap.shm
• def ap.mm
• def ap.subl
• def ap.subi
• def ap.mixl
• def ap.mixi
• def ap.arkl
• def ap.ismask
• def ap.round_inv
• def ap.round_eq
• def ap.round_out
• def ap.last_inv
• def ap.last_eq
• def ap.last_out
• def ap.rounds_out
• def ap.rounds_inv
• def ap.cipher_out
• def ap.cipher_inv
• def ap.state_back
• def ap.in_mask
• def ap.out_in
• def ap.top