proofs/crypto/chacha/involution.bend checks

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

5 imports

import Base
import ../../../spec/crypto/chacha.bend as R
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ./stream.bend as T

Laws

law wxor_inv provedsource · line 16 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Word.xor(n, Word.xor(n, a, b), b) == a : Word(n)}

law u32_xor_inv provedsource · line 34 · raw

@+a:U32 -> @+b:U32 -> {U32.xor(U32.xor(a, b), b) == a : U32}

law length_append provedsource · line 46 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> {List.length(&2, U32, List.append(&2, U32, xs, ys)) == Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}

law le_add provedsource · line 57 · raw

@+p:Nat -> @+l:Nat -> @+k:Nat -> @+h:{Nat.is_le(p, l) == True{} : Bool} -> {Nat.is_le(p, Nat.add(k, l)) == True{} : Bool}

law xor_length provedsource · line 69 · raw

@+xs:List<&2, U32> -> @+ks:List<&2, U32> -> @+h:{Nat.is_le(List.length(&2, U32, xs), List.length(&2, U32, ks)) == True{} : Bool} -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xor_bytes(xs, ks)) == List.length(&2, U32, xs) : Nat}

law xor_twice provedsource · line 82 · raw

@+xs:List<&2, U32> -> @+ks:List<&2, U32> -> @+h:{Nat.is_le(List.length(&2, U32, xs), List.length(&2, U32, ks)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xor_bytes(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xor_bytes(xs, ks), ks) == xs : List<&2, U32>}

law ks_length provedsource · line 107 · raw

@+fuel:Nat -> @+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> {Nat.is_le(fuel, List.length(&2, U32, ks(fuel, r, kb, c, nb))) == True{} : Bool}

law xor_append provedsource · line 126 · raw

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

law enc_ks provedsource · line 141 · raw

@+fuel:Nat -> @+xs:List<&2, U32> -> @+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.encrypt_blocks(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.blocks(fuel, xs), r, kb, c, nb) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xor_bytes(xs, ks(fuel, r, kb, c, nb)) : List<&2, U32>}

law encrypt_xor provedsource · line 177 · raw

@+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.encrypt_rounds(r, kb, c, nb, pt) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xor_bytes(pt, ks(List.length(&2, U32, pt), r, kb, c, nb)) : List<&2, U32>}

law encrypt_length provedsource · line 189 · raw

@+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> @+pt:List<&2, U32> -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.encrypt_rounds(r, kb, c, nb, pt)) == List.length(&2, U32, pt) : Nat}

The ciphertext is as long as the plaintext.

law involution provedsource · line 203 · raw

@+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.encrypt_rounds(r, kb, c, nb, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.encrypt_rounds(r, kb, c, nb, pt)) == pt : List<&2, U32>}

Definitions

def ks source · line 102 · raw

@fuel:Nat -> @+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> List<&2, U32>

The keystream of fuel blocks from counter c.