~/bend-docscommunity

spec/crypto/aes/gcm.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as Gcm

5 imports
import Base
import ../../../src/crypto/aes/types.bend as T
import ./poly.bend as P
import ./aes.bend as AES
import ../subtle.bend as Eq

Definitions

def byte_bits source · line 14 · raw

@x:U32 -> List<&2, Bool>

The bits of a byte, the most significant (leftmost) first.

def string_bits source · line 19 · raw

@xs:List<&2, U32> -> List<&2, Bool>

def bits_bytes source · line 27 · raw

@bs:List<&2, Bool> -> List<&2, U32>

The byte whose bits, leftmost first, are the next eight of a bit string.

def word_of source · line 35 · raw

@n:Nat -> @bs:List<&2, Bool> -> Word(n)

The first n bits of a bit string, zero-filled.

def block source · line 48 · raw

@xs:List<&2, U32> -> Word(128n)

Bit i of a block (bit 0 the leftmost) is the coefficient of x^i, and f(x) = 1 + x + x^2 + x^7 + x^128: x^128 = 1 + x + x^2 + x^7 (R = 11100001 || 0^120).

def block_bytes source · line 51 · raw

@w:Word(128n) -> List<&2, U32>

def low source · line 54 · raw

Word(128n)

def mul source · line 58 · raw

@x:Word(128n) -> @y:Word(128n) -> Word(128n)

X * Y: the polynomial product reduced modulo f.

def ghash source · line 63 · raw

@+h:Word(128n) -> @x:List<&2, U32> -> @y:Word(128n) -> Word(128n)

def int32 source · line 73 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> @+d:U32 -> U32

inc_32: the rightmost 32 bits, as an integer, plus one modulo 2^32.

def str32 source · line 76 · raw

@w:U32 -> List<&2, U32>

def inc32 source · line 81 · raw

@x:List<&2, U32> -> List<&2, U32>

def ciph source · line 89 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x:List<&2, U32> -> List<&2, U32>

CIPH_K on a 16-byte block.

def xor_bytes source · line 93 · raw

@x:List<&2, U32> -> @k:List<&2, U32> -> List<&2, U32>

X xor K over the length of X (MSB_len(X) of K when X is the shorter).

def gctr source · line 100 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x:List<&2, U32> -> @+cb:List<&2, U32> -> List<&2, U32>

def zeros source · line 110 · raw

@n:Nat -> List<&2, U32>

def pad source · line 115 · raw

@+x:List<&2, U32> -> List<&2, U32>

X || 0^v, v = 128*ceil(len(X)/128) - len(X): zero bytes complete the last 16-byte block.

def octets source · line 125 · raw

@width:Nat -> @+n:Nat -> List<&2, U32>

[n]_(8*width), most significant byte first.

def len64 source · line 133 · raw

@+xs:List<&2, U32> -> List<&2, U32>

[len(X)]_64: the bit length of X.

def hash_key source · line 137 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> Word(128n)

Algorithm 4, J0 = IV || 0^31 || 1 for a 96-bit IV.

def j0 source · line 140 · raw

@+iv:List<&2, U32> -> List<&2, U32>

def tag source · line 143 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> List<&2, U32>

def seal source · line 148 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @pt:List<&2, U32> -> List<&2, U32>

GCM-AE_K(IV, P, A) = (C, T), returned as C || T.

def accept source · line 152 · raw

@ok:Bool -> @p:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def open_checked source · line 159 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @t:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def open_split source · line 164 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+input:List<&2, U32> -> @+n:Nat -> @short:Bool -> Maybe<&2, List<&2, U32>>

GCM-AD_K(IV, C, A, T), the input being C || T: FAIL (None) unless T is the tag of C.

def open source · line 171 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+input:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def aes_seal source · line 176 · raw

@+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @pt:List<&2, U32> -> List<&2, U32>

GCM over AES with the key's own Nk and Nr (FIPS 197 Figure 4).

def aes_open source · line 179 · raw

@+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+input:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def aes_tag source · line 182 · raw

@+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> List<&2, U32>