~/bend-docscommunity

proofs/crypto/aead/laws.bend open laws/TODOs

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

6 imports
import Base
import ../../../src/crypto/aead.bend as A
import ../../../src/crypto/aead/chacha20poly1305.bend as CP
import ../../../spec/crypto/chacha.bend as RC
import ../../../spec/crypto/chacha20poly1305.bend as R
import ../../../spec/crypto/aes/gcm.bend as G

Laws

law chacha20poly1305.seal openits proof in laws_crypto.bend does not pass the checker (fails)source · line 29 · 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) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}

law chacha20poly1305.open openits proof in laws_crypto.bend does not pass the checker (fails)source · line 36 · raw

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

law xchacha20poly1305.seal openits proof in laws_crypto.bend does not pass the checker (fails)source · line 43 · 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) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.xseal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}

law xchacha20poly1305.open openits proof in laws_crypto.bend does not pass the checker (fails)source · line 50 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.open(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.XCHACHA20_POLY1305{}, key, nonce, aad, data) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.xopen(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}

law aes128gcm.seal openits proof in laws_crypto.bend does not pass the checker (fails)source · line 57 · raw

@+key:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 16n : Nat} -> @+nonce:List<&2, U32> -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.seal(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.AES_128_GCM{}, key, nonce, aad, pt) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}

law aes128gcm.open openits proof in laws_crypto.bend does not pass the checker (fails)source · line 66 · raw

@+key:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 16n : Nat} -> @+nonce:List<&2, U32> -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.open(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.AES_128_GCM{}, key, nonce, aad, data) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}

law aes256gcm.seal openits proof in laws_crypto.bend does not pass the checker (fails)source · line 75 · raw

@+key:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 32n : Nat} -> @+nonce:List<&2, U32> -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.seal(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.AES_256_GCM{}, key, nonce, aad, pt) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}

law aes256gcm.open openits proof in laws_crypto.bend does not pass the checker (fails)source · line 84 · raw

@+key:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 32n : Nat} -> @+nonce:List<&2, U32> -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.open(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.AES_256_GCM{}, key, nonce, aad, data) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}

law chacha20poly1305.encrypt openits proof in laws_crypto.bend does not pass the checker (fails)source · line 94 · raw

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

The per-algorithm checked ChaCha20-Poly1305 API agrees with the facade.

law chacha20poly1305.decrypt openits proof in laws_crypto.bend does not pass the checker (fails)source · line 101 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.decrypt(key, nonce, aad, data) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.decrypt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.CHACHA20_POLY1305{}, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}

law xchacha20poly1305.encrypt openits proof in laws_crypto.bend does not pass the checker (fails)source · line 108 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.xencrypt(key, nonce, aad, pt) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.encrypt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.XCHACHA20_POLY1305{}, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}

law xchacha20poly1305.decrypt openits proof in laws_crypto.bend does not pass the checker (fails)source · line 115 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.xdecrypt(key, nonce, aad, data) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.decrypt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.XCHACHA20_POLY1305{}, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}

law encrypt.valid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 124 · 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 encrypt.invalid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 134 · raw

@+alg:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.Alg -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.valid(alg, key, nonce) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.encrypt(alg, key, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}

law decrypt.valid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 143 · 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 decrypt.invalid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 153 · raw

@+alg:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.Alg -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.valid(alg, key, nonce) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.decrypt(alg, key, nonce, aad, data) == None{} : Maybe<&2, List<&2, U32>>}

law roundtrip openits proof in laws_crypto.bend does not pass the checker (fails)source · line 165 · 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} -> {decrypt_sealed(alg, key, nonce, aad, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.encrypt(alg, key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}

decrypt(encrypt(x)) == Some(x).

law forgery openits proof in laws_crypto.bend does not pass the checker (fails)source · line 177 · 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 == expected_tag(alg, key, nonce, aad, ct) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.decrypt(alg, key, nonce, aad, List.append(&2, U32, ct, t)) == None{} : Maybe<&2, List<&2, U32>>}

ciphertext || t is rejected for every 16-byte t other than the tag of the ciphertext under this key, nonce and aad.

law seal_layout openits proof in laws_crypto.bend does not pass the checker (fails)source · 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} -> &ct:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.encrypt(alg, key, nonce, aad, pt) == Some{List.append(&2, U32, ct, expected_tag(alg, key, nonce, aad, ct))} : Maybe<&2, List<&2, U32>>}

What encrypt returns is a ciphertext followed by its expected tag.

law decrypt_sound openits proof in laws_crypto.bend does not pass the checker (fails)source · line 205 · 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.decrypt(alg, key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.encrypt(alg, key, nonce, aad, p) == Some{data} : Maybe<&2, List<&2, U32>>}

Decryption is sound: whatever decrypt accepts is exactly what encrypt produces for the returned plaintext (so every accepted input is the honest ciphertext of its plaintext under this key, nonce and aad).

Definitions

def expected_tag source · line 14 · raw

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

The tag the specification computes over ciphertext ct: decrypt accepts ct || t exactly for this t.

def decrypt_sealed source · line 22 · 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 applied to what encrypt returned (None stays None).