~/bend-docscommunity

proofs/crypto/aead/chacha20poly1305.bend checks

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

15 imports
import Base
import ../poly1305/mac.bend as PM
import ../../../src/crypto/chacha/chacha20.bend as CH
import ../../../src/crypto/aead/chacha20poly1305.bend as I
import ../../../src/crypto/subtle.bend as S
import ../../../spec/crypto/chacha.bend as RC
import ../../../spec/crypto/poly1305.bend as RP
import ../../../spec/crypto/subtle.bend as RS
import ../../../spec/crypto/chacha20poly1305.bend as R
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../chacha/stream.bend as T
import ../chacha/xchacha.bend as X
import ../chacha/involution.bend as V
import ./subtle_eq.bend as SE

Laws

law poly_key_eq provedsource · line 31 · raw

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

law mac_data_eq provedsource · line 41 · raw

@+aad:List<&2, U32> -> @+ct:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.mac_data(aad, ct) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.mac_data(aad, ct) : List<&2, U32>}

law tag_eq provedsource · line 49 · raw

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

law seal_eq provedsource · line 66 · raw

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

law open_tag_eq provedsource · line 80 · raw

@+ok:Bool -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+ct:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.open_tag(ok, key, nonce, ct) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.open_tag(ok, key, nonce, ct) : Maybe<&2, List<&2, U32>>}

law open_split_eq provedsource · line 93 · raw

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

law open_len_eq provedsource · line 108 · raw

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

law open_eq provedsource · line 130 · raw

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

law xkey_eq provedsource · line 140 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.xkey(key, nonce) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xsubkey(key, nonce) : List<&2, U32>}

law xnonce_eq provedsource · line 150 · raw

@+nonce:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.xnonce(nonce) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xnonce(nonce) : List<&2, U32>}

law xseal_eq provedsource · line 157 · raw

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

law xopen_eq provedsource · line 171 · raw

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

law length_append provedsource · line 187 · 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 prefix_append provedsource · line 195 · raw

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

law suffix_append provedsource · line 206 · raw

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

law add16_not_lt provedsource · line 217 · raw

@+a:Nat -> {Nat.is_lt(Nat.add(a, 16n), 16n) == False{} : Bool}

a + 16 is not below 16, and (a + 16) - 16 == a.

law add16_sub provedsource · line 225 · raw

@+a:Nat -> {Nat.sub(Nat.add(a, 16n), 16n) == a : Nat}

law open_append provedsource · line 234 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> @+t:List<&2, U32> -> @+ht:{List.length(&2, U32, t) == 16n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.open(key, nonce, aad, List.append(&2, U32, ct, t)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.open_split(key, nonce, aad, ct, t) : Maybe<&2, List<&2, U32>>}

Opening ct || t with a 16-byte t checks t against the tag of ct.

law roundtrip provedsource · line 273 · raw

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

Opening what was sealed gives the plaintext back (for every key, nonce, aad and plaintext list).

law open_tag_false provedsource · line 289 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> @+t:List<&2, U32> -> @ne:(@_:{t == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.tag(key, nonce, aad, ct) : List<&2, U32>} -> Empty) -> @+b:Bool -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/subtle.equal(t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.tag(key, nonce, aad, ct)) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.open_tag(b, key, nonce, ct) == None{} : Maybe<&2, List<&2, U32>>}

law forgery provedsource · line 307 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> @+t:List<&2, U32> -> @+ht:{List.length(&2, U32, t) == 16n : Nat} -> @ne:(@_:{t == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.tag(key, nonce, aad, ct) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.open(key, nonce, aad, List.append(&2, U32, ct, t)) == None{} : Maybe<&2, List<&2, U32>>}

Opening ciphertext || t fails for every 16-byte t that is not the tag of the ciphertext (under the key, nonce and aad given).

law iforgery provedsource · line 324 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> @+t:List<&2, U32> -> @+ht:{List.length(&2, U32, t) == 16n : Nat} -> @ne:(@_:{t == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.tag(key, nonce, aad, ct) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.open(key, nonce, aad, List.append(&2, U32, ct, t)) == None{} : Maybe<&2, List<&2, U32>>}

The implementation's tag is the specification's, so a t other than the implementation's tag is rejected by the implementation.

law iroundtrip provedsource · line 339 · raw

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

Definitions

def iseal source · line 63 · raw

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

def ospl source · line 116 · raw

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

def olen source · line 243 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+d:List<&2, U32> -> @short:Bool -> Maybe<&2, List<&2, U32>>

def osplit_at source · line 246 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+d:List<&2, U32> -> @+n:Nat -> Maybe<&2, List<&2, U32>>