proofs/crypto/aead/proof.bend checks

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

13 imports

import Base
import ../../../src/crypto/aead.bend as A
import ../../../src/crypto/aead/chacha20poly1305.bend as CP
import ../../../src/crypto/aesgcm.bend as GCM
import ../../../spec/crypto/chacha.bend as RC
import ../../../spec/crypto/chacha20poly1305.bend as R
import ../../../spec/crypto/aes/aes.bend as S
import ../../../spec/crypto/aes/gcm.bend as G
import ../../lib/nat.bend as N
import ./laws.bend as Laws
import ./chacha20poly1305.bend as C
import ../aes/api.bend as AE
import ./sound.bend as SD

Laws

law when_same provedsource · line 47 · raw

@+ok:Bool -> @+x:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.when(ok, x) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.when_open(ok, Some{x}) : Maybe<&2, List<&2, U32>>}

law when_open_same provedsource · line 57 · raw

@+ok:Bool -> @+r:Maybe<&2, List<&2, U32>> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.when_open(ok, r) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.when_open(ok, r) : Maybe<&2, List<&2, U32>>}

law valid_true provedsource · line 81 · raw

@+alg:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.Alg -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.key_size(alg) : Nat} -> @+hn:{List.length(&2, U32, nonce) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.nonce_size(alg) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.valid(alg, key, nonce) == True{} : Bool}

law encrypt_valid provedsource · line 98 · raw

@+alg:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.Alg -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.key_size(alg) : Nat} -> @+hn:{List.length(&2, U32, nonce) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.nonce_size(alg) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.encrypt(alg, key, nonce, aad, pt) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.seal(alg, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}

law decrypt_valid provedsource · line 121 · raw

@+alg:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.Alg -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.key_size(alg) : Nat} -> @+hn:{List.length(&2, U32, nonce) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.nonce_size(alg) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.decrypt(alg, key, nonce, aad, data) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.open(alg, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}

law ds_open provedsource · line 152 · raw

@+alg:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.Alg -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+m:Maybe<&2, List<&2, U32>> -> @+hk:{List.length(&2, U32, key) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.key_size(alg) : Nat} -> @+hn:{List.length(&2, U32, nonce) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.nonce_size(alg) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aead/laws.decrypt_sealed(alg, key, nonce, aad, m) == open_sealed(alg, key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}

law os128 provedsource · line 167 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+m:Maybe<&2, List<&2, U32>> -> {open_sealed(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.AES_128_GCM{}, key, nonce, aad, m) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/api.open128(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}

law os256 provedsource · line 179 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+m:Maybe<&2, List<&2, U32>> -> {open_sealed(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.AES_256_GCM{}, key, nonce, aad, m) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/api.open256(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}

law open_seal provedsource · line 191 · raw

@+alg:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.Alg -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.key_size(alg) : Nat} -> @+hn:{List.length(&2, U32, nonce) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.nonce_size(alg) : Nat} -> {open_sealed(alg, key, nonce, aad, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.seal(alg, key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}

law open_forged provedsource · line 225 · raw

@+alg:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.Alg -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> @+t:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.key_size(alg) : Nat} -> @+hn:{List.length(&2, U32, nonce) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.nonce_size(alg) : Nat} -> @+ht:{List.length(&2, U32, t) == 16n : Nat} -> @ne:(@_:{t == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aead/laws.expected_tag(alg, key, nonce, aad, ct) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.open(alg, key, nonce, aad, List.append(&2, U32, ct, t)) == None{} : Maybe<&2, List<&2, U32>>}

law layout_cp provedsource · line 261 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.seal(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.CHACHA20_POLY1305{}, key, nonce, aad, pt) == sapp(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.encrypt_ct(key, nonce, pt), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.tag(key, nonce, aad, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.encrypt_ct(key, nonce, pt))) : Maybe<&2, List<&2, U32>>}

law layout_x provedsource · line 272 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.seal(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.XCHACHA20_POLY1305{}, key, nonce, aad, pt) == sapp(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.encrypt_ct(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.xkey(key, nonce), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.xnonce(nonce), pt), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.tag(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xsubkey(key, nonce), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xnonce(nonce), aad, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.encrypt_ct(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.xkey(key, nonce), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.xnonce(nonce), pt))) : Maybe<&2, List<&2, U32>>}

law open_sound provedsource · line 312 · raw

@+alg:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.Alg -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> @+p:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.key_size(alg) : Nat} -> @+hn:{List.length(&2, U32, nonce) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.nonce_size(alg) : Nat} -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.open(alg, key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.seal(alg, key, nonce, aad, p) == Some{data} : Maybe<&2, List<&2, U32>>}

Definitions

def open_sealed source · line 147 · raw

@+alg:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.Alg -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @m:Maybe<&2, List<&2, U32>> -> Maybe<&2, List<&2, U32>>

decrypt after encrypt is open after seal (on valid lengths).

def sapp source · line 258 · raw

@+ct:List<&2, U32> -> @+t:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def gct source · line 289 · raw

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

def smaybe source · line 309 · raw

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