bend-osdev-crypto

Releases (1)

• 0.1.0.0 indexed

Definitions (678)

mac.bend

• def CrMac.verify_tagwhether t is m's tag, comparing every byte
• def CrMac.compute_withthe tag of m under a raw key

modes.bend

• def cr.blks.rev_onto
• def cr.ecb
• def cr.ecb.go
• def CrEcb.encrypt_blocks
• def CrEcb.decrypt_blocks
• def cr.cbc.enc
• def cr.cbc.dec
• def cr.cbc.enc.go
• def cr.cbc.dec.go
• def CrCbc.encrypt_blocksCBC on blocks: the last ciphertext block of one call is the IV of the next, so a message may arrive a block at a time
• def CrCbc.decrypt_blocks
• def cr.pick_n
• def cr.pick_cur
• def cr.pick_acc
• def cr.chunksthe whole n-byte pieces of xs, last first (cur: the piece being filled, reversed, i bytes long)
• def cr.cons_ma block onto a list of blocks, None if either is missing
• def cr.blocks_of.gothe pieces (last first) as blocks, in order, onto acc
• def cr.divides
• def cr.blocks_of.some
• def cr.blocks_of.ok
• def CrModes.blocks_ofA byte string of whole blocks as its blocks (CrNotBlockMultiple otherwise)
• def cr.octets_of.go
• def CrModes.octets_ofThe bytes of a list of blocks
• def cr.iv.pick
• def cr.ivan IV of one block (CrBadIvLength otherwise)
• def CrEcb.encrypt
• def CrEcb.decrypt
• def CrCbc.encrypt
• def CrCbc.decrypt
• type CrCtrStatethe state: the key schedule, the next counter block (its bytes), and the keystream bytes left over from the last block
• def cr.ctr.sum
• def cr.ctr.carry
• def cr.ctr.add1one added to a number given by its bytes, least significant first (rs), the result most significant first, onto acc
• def cr.ctr.incthe next counter block
• def cr.ctr.block
• def cr.head
• def cr.tail
• def cr.ctr.next
• def CrCtr.nextThe keystream generator: the next keystream byte and the state after it
• def cr.ctr.start
• def CrCtr.startThe state for a raw key and an initial counter block of bsize bytes (CrBadIvLength for another length)
• def CrCtr.updateThe next piece of data, encrypted or decrypted, and the state after it

octets.bend

• def cr.oct.xorlxs xor ys, element by element, over xs's length (a missing element of ys counts as 0)
• def CrOct.xora xor b, byte by byte, over a's length (b's missing bytes count as 0)
• def cr.oct.rep
• def CrOct.repthe byte b, n times
• def cr.oct.rev
• def cr.oct.revs
• def cr.oct.flush
• def cr.oct.pieces.step
• def cr.oct.pieces.cur
• def cr.oct.pieces.i
• def cr.oct.pieces.gothe pieces of xs, last first: whole n-byte pieces, then what is left (cur: the piece being filled, reversed, i bytes long)
• def CrOct.piecesxs cut into pieces of n bytes, in order: every piece but the last has n bytes, the last 1 to n (no pieces for no bytes)

pbkdf2.bend

• def cr.pbkdf2.xorbytewise XOR of two tags (as long as the shorter)
• def cr.pbkdf2.chainacc xor U_(j+1) xor ...
• def cr.pbkdf2.blockT_i, with c the iteration count less one
• def cr.pbkdf2.head
• def cr.pbkdf2.tail
• def cr.pbkdf2.outn more bytes: the rest of the current block cur, then T_(i+1), T_(i+2), ...
• def CrPbkdf2.streamThe first n bytes of the derived key, under a prepared key k (the MAC's, from the password) and an iteration count c of at least 1, without the checks: T_1 || T_2 || ...
• def cr.pbkdf2.key
• def cr.pbkdf2.checked
• def cr.pbkdf2.fits
• def CrPbkdf2.pbkdf2DK = PBKDF2(P, S, c, dkLen) over the MAC (~K, ~key, ~compute) with hLen-byte tags (~hlen)
• def CrPbkdf2.deriveThe KDF interface's ~derive (secret, salt, info, length) for c iterations; info is unused

pcbc.bend

• def cr.pcbc.enc
• def cr.pcbc.dec
• def cr.pcbc.enc.go
• def cr.pcbc.dec.go
• def CrPcbc.encrypt_blocksPCBC on blocks, from the chaining value v (the IV for the first call)
• def CrPcbc.decrypt_blocks
• def cr.pcbc.last
• def CrPcbc.next_ivThe chaining value after the plaintext blocks ps encrypted to cs from v: the next call's v, so a message may arrive in pieces of whole blocks
• def CrPcbc.encryptPCBC on bytes: a message of whole blocks under a one-block IV (CrBadIvLength, CrNotBlockMultiple otherwise)
• def CrPcbc.decrypt

sign.bend

• type CrKeypairA secret key and its public key (open type)
• def CrSign.keypairThe key pair of a secret key's bytes
• def cr.sign.check
• def CrSign.verify_bytesWhether sig is valid for m under the public key with these bytes (False for a malformed key)

stream.bend

• def CrStream.cryptA stream cipher in one call: the data under a key and an IV
• def CrStream.keystreamThe next n keystream bytes (the data n zero bytes)
• type CrKsStepone keystream byte and the state after it
• type CrXorOutwhat CrXor.update answers: the state after the data, and the data encrypted (open type)
• def CrKsStep.k
• def CrKsStep.st
• def cr.ks.xsThe structural forms the proofs reason about: the data, byte by byte, and the state after it
• def cr.ks.after
• type CrKsRunThe loop that runs: tail-recursive, the output kept reversed, each keystream byte computed once
• def cr.rev_onto
• def cr.ks.go
• def cr.ks.out
• def CrXor.updateThe stream cipher of a keystream generator: m XORed with the next len(m) keystream bytes, and the state after them
• def CrXor.out_state
• def CrXor.out_data

vmac.bend

• type CrU128128-bit numbers (internal)
• def cr.vm.carry
• def cr.vm.u