~/bend-docscommunity

proofs/crypto/aead/sound.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend as Sound

9 imports
import Base
import ../../../spec/crypto/chacha.bend as RC
import ../../../spec/crypto/chacha20poly1305.bend as R
import ../../../spec/crypto/subtle.bend as RS
import ../../../spec/crypto/aes/gcm.bend as G
import ../../lib/logic.bend as L
import ../chacha/involution.bend as V
import ../aes/aead.bend as AD
import ./subtle_eq.bend as SE

Laws

law none_some provedsource · line 21 · raw

@+p:List<&2, U32> -> @+h:{None{} == Some{p} : Maybe<&2, List<&2, U32>>} -> Empty

law some_inj provedsource · line 29 · raw

@+x:List<&2, U32> -> @+p:List<&2, U32> -> @+h:{Some{x} == Some{p} : Maybe<&2, List<&2, U32>>} -> {x == p : List<&2, U32>}

law prefix_suffix provedsource · line 40 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {List.append(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.prefix(n, xs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.suffix(n, xs)) == xs : List<&2, U32>}

law take_drop provedsource · line 52 · raw

@+xs:List<&2, U32> -> @+n:Nat -> {List.append(&2, U32, List.take(&2, U32, xs, n), List.drop(&2, U32, xs, n)) == xs : List<&2, U32>}

law c_tag provedsource · line 69 · raw

@+ok:Bool -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> @+t:List<&2, U32> -> @+p:List<&2, U32> -> @+hok:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/subtle.equal(t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.tag(key, nonce, aad, ct)) == ok : Bool} -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.open_tag(ok, key, nonce, ct) == Some{p} : Maybe<&2, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.seal(key, nonce, aad, p) == List.append(&2, U32, ct, t) : List<&2, U32>}

law c_len provedsource · line 96 · raw

@+short:Bool -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> @+p:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.open_len(short, key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.seal(key, nonce, aad, p) == data : List<&2, U32>}

law chacha_sound provedsource · line 118 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> @+p:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.open(key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.seal(key, nonce, aad, p) == data : List<&2, U32>}

Whatever opens to p is the sealing of p.

law g_tag provedsource · line 135 · raw

@+ok:Bool -> @+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @+t:List<&2, U32> -> @+p:List<&2, U32> -> @+hok:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/subtle.equal(t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.tag(nk, nr, key, iv, aad, c)) == ok : Bool} -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.accept(ok, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, c, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.inc32(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.j0(iv)))) == Some{p} : Maybe<&2, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.seal(nk, nr, key, iv, aad, p) == List.append(&2, U32, c, t) : List<&2, U32>}

law g_len provedsource · line 165 · raw

@+short:Bool -> @+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+input:List<&2, U32> -> @+p:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.open_split(nk, nr, key, iv, aad, input, List.length(&2, U32, input), short) == Some{p} : Maybe<&2, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.seal(nk, nr, key, iv, aad, p) == input : List<&2, U32>}

law gcm_sound provedsource · line 188 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+input:List<&2, U32> -> @+p:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.open(nk, nr, key, iv, aad, input) == Some{p} : Maybe<&2, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.seal(nk, nr, key, iv, aad, p) == input : List<&2, U32>}

Definitions

def csa source · line 66 · raw

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

def gsa source · line 132 · raw

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