src/crypto/aes/gcm.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/gcm.bend as Gcm

4 imports

import Base
import ./types.bend as T
import ./aes.bend as A
import ../subtle.bend as Subtle

Types

type Block source · line 16 · raw

Data

B

@w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> Block

type Acc source · line 19 · raw

Data

Acc
```
@z:Block -> @v:Block -> Acc
```

Definitions

def zero source · line 22 · raw

Block

def mulx source · line 26 · raw

@v:Block -> Block

V * x: the block shifted one bit toward x^127, x^128 = R.

def add_masked source · line 35 · raw

@+bit:U32 -> @z:Block -> @v:Block -> Block

Z xor (V and (0 - bit)), bit being 0 or 1.

def step source · line 42 · raw

@+bit:U32 -> @acc:Acc -> Acc

def mul_byte source · line 48 · raw

@+a:U32 -> @acc:Acc -> Acc

The eight bits of a byte, the most significant first.

def mul_bytes source · line 54 · raw

@xs:List<&2, U32> -> @acc:Acc -> Acc

def acc_z source · line 61 · raw

@acc:Acc -> Block

def unpack source · line 67 · raw

@z:Block -> List<&2, U32>

The 16 bytes of a block, and the block of 16 bytes (big-endian words).

def word source · line 75 · raw

@q:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> U32

def pack source · line 82 · raw

@s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.State -> Block

An AES state as a block: its columns are the words.

def xor_bytes source · line 87 · raw

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

def absorb source · line 95 · raw

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

(Y xor X) * H for a 16-byte X.

def zeros source · line 98 · raw

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

def ghash source · line 102 · raw

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

GHASH_H over the bytes, a last partial block padded with zero bytes.

def octets source · line 112 · raw

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

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

def lengths source · line 120 · raw

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

[len(A)]_64 || [len(C)]_64, in bits.

def counter source · line 127 · raw

@+n0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+c:U32 -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.State

The counter block: the 96-bit nonce (three words) and a 32-bit counter.

def keystream source · line 130 · raw

@+sched:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule -> @+n0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+c:U32 -> List<&2, U32>

def gctr source · line 133 · raw

@+sched:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule -> @+xs:List<&2, U32> -> @+n0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+c:U32 -> List<&2, U32>

def hash_key source · line 143 · raw

@+sched:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule -> Block

def tag source · line 148 · raw

@+sched:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule -> @+n0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> List<&2, U32>

The tag of ciphertext c: GHASH over A || 0^v || C || 0^u || lengths, encrypted with the counter block J0 = nonce || 1.

def seal_core source · line 153 · raw

@+sched:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule -> @+n0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+aad:List<&2, U32> -> @pt:List<&2, U32> -> List<&2, U32>

C || T; the counter of the first data block is 2 (inc32(J0)).

def accept source · line 157 · raw

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

def open_checked source · line 165 · raw

@+sched:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule -> @+n0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @t:List<&2, U32> -> Maybe<&2, List<&2, U32>>

The plaintext when t is the tag of c; None otherwise (compared in constant time).

def open_split source · line 168 · raw

@+sched:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule -> @+n0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+aad:List<&2, U32> -> @+input:List<&2, U32> -> @+n:Nat -> @short:Bool -> Maybe<&2, List<&2, U32>>

def open_core source · line 175 · raw

@+sched:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule -> @+n0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+n2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/types.Quad -> @+aad:List<&2, U32> -> @+input:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def seal_nonce source · line 181 · raw

@+sched:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule -> @nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def open_nonce source · line 188 · raw

@+sched:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule -> @nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+input:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def seal_key source · line 195 · raw

@m:Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def open_key source · line 202 · raw

@m:Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+input:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def schedule_if source · line 209 · raw

@ok:Bool -> @+key:List<&2, U32> -> Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule>

def schedule_of source · line 217 · raw

@+width:Nat -> @+key:List<&2, U32> -> Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/aes/aes.Schedule>

The expanded key when the key has the given length.