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

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

3 imports

import Base
import ../../../src/crypto/chacha/chacha20.bend as I
import ../../../spec/crypto/chacha.bend as R

Laws

law block_rounds openits proof in laws_crypto.bend does not pass the checker (fails)source · line 15 · raw

@+r:Nat -> @+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.block_rounds(r, key, counter, nonce) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.block_rounds(r, key, counter, nonce) : List<&2, U32>}

chacha20_block with r double rounds.

law encrypt_rounds openits proof in laws_crypto.bend does not pass the checker (fails)source · line 23 · raw

@+r:Nat -> @+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.encrypt_rounds(r, key, counter, nonce, plaintext) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.encrypt_rounds(r, key, counter, nonce, plaintext) : List<&2, U32>}

chacha20_encrypt with r double rounds.

law hchacha_rounds openits proof in laws_crypto.bend does not pass the checker (fails)source · line 32 · raw

@+r:Nat -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.hchacha_rounds(r, key, nonce) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.hchacha_rounds(r, key, nonce) : List<&2, U32>}

HChaCha20 with r double rounds, and at twenty rounds.

law hchacha20 openits proof in laws_crypto.bend does not pass the checker (fails)source · line 38 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.hchacha20_unchecked(key, nonce) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.hchacha20(key, nonce) : List<&2, U32>}

law xencrypt openits proof in laws_crypto.bend does not pass the checker (fails)source · line 44 · raw

@+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.xencrypt_unchecked(key, counter, nonce, plaintext) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xencrypt(key, counter, nonce, plaintext) : List<&2, U32>}

XChaCha20.

law chacha20_block.valid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 53 · raw

@+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 32n : Nat} -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.chacha20_block(key, counter, nonce) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.block(key, counter, nonce)} : Maybe<&2, List<&2, U32>>}

law chacha20_block.invalid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 61 · raw

@+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> @+h:{Bool.and(Nat.is_eq(List.length(&2, U32, key), 32n), Nat.is_eq(List.length(&2, U32, nonce), 12n)) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.chacha20_block(key, counter, nonce) == None{} : Maybe<&2, List<&2, U32>>}

law chacha20.valid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 68 · raw

@+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 32n : Nat} -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.chacha20(key, counter, nonce, plaintext) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.encrypt(key, counter, nonce, plaintext)} : Maybe<&2, List<&2, U32>>}

law chacha20.invalid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 77 · raw

@+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+h:{Bool.and(Nat.is_eq(List.length(&2, U32, key), 32n), Nat.is_eq(List.length(&2, U32, nonce), 12n)) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.chacha20(key, counter, nonce, plaintext) == None{} : Maybe<&2, List<&2, U32>>}

law hchacha20.valid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 85 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 32n : Nat} -> @+hn:{List.length(&2, U32, nonce) == 16n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.hchacha20(key, nonce) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.hchacha20(key, nonce)} : Maybe<&2, List<&2, U32>>}

law hchacha20.invalid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 92 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+h:{Bool.and(Nat.is_eq(List.length(&2, U32, key), 32n), Nat.is_eq(List.length(&2, U32, nonce), 16n)) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.hchacha20(key, nonce) == None{} : Maybe<&2, List<&2, U32>>}

law xchacha20.valid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 98 · raw

@+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+hk:{List.length(&2, U32, key) == 32n : Nat} -> @+hn:{List.length(&2, U32, nonce) == 24n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.xchacha20(key, counter, nonce, plaintext) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xencrypt(key, counter, nonce, plaintext)} : Maybe<&2, List<&2, U32>>}

law xchacha20.invalid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 107 · raw

@+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+h:{Bool.and(Nat.is_eq(List.length(&2, U32, key), 32n), Nat.is_eq(List.length(&2, U32, nonce), 24n)) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.xchacha20(key, counter, nonce, plaintext) == None{} : Maybe<&2, List<&2, U32>>}

law involution openits proof in laws_crypto.bend does not pass the checker (fails)source · line 118 · raw

@+r:Nat -> @+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.encrypt_rounds(r, key, counter, nonce, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.encrypt_rounds(r, key, counter, nonce, plaintext)) == plaintext : List<&2, U32>}

Decryption is encryption: applying the cipher twice is the identity.

law xinvolution openits proof in laws_crypto.bend does not pass the checker (fails)source · line 126 · raw

@+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.xencrypt_unchecked(key, counter, nonce, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.xencrypt_unchecked(key, counter, nonce, plaintext)) == plaintext : List<&2, U32>}

law encrypt_length openits proof in laws_crypto.bend does not pass the checker (fails)source · line 134 · raw

@+r:Nat -> @+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.encrypt_rounds(r, key, counter, nonce, plaintext)) == List.length(&2, U32, plaintext) : Nat}

The ciphertext is as long as the plaintext.

law block_length openits proof in laws_crypto.bend does not pass the checker (fails)source · line 143 · raw

@+r:Nat -> @+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.block_rounds(r, key, counter, nonce)) == 64n : Nat}

The block function's output has 64 bytes, HChaCha20's 32.

law hchacha_length openits proof in laws_crypto.bend does not pass the checker (fails)source · line 150 · raw

@+r:Nat -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.hchacha_rounds(r, key, nonce)) == 32n : Nat}