proofs/crypto/mac/proof.bend

bend-collections-laws-crypto@1.0.0.0 · 39 lines · 1 definition

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/mac.bend as MAC
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/subtle.bend as Subtle
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hmac.bend as Spec
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend as SubtleSpec
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/laws.bend as SubtleLaws
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/proof.bend as SubtleProof
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/mac/hmac.bend as P
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/mac/laws.bend as Laws
10
11# Gate for src/crypto/mac.bend: `bend proofs/crypto/mac/proof.bend`.
12# Sign: hmac.bend (the key block, then the two hashes through the proved
13# SHA-256). Verify: subtle.eq is list equality (proofs/crypto/subtle).
14
15def Laws.Sign.correct(key, msg):
16  P.sign_correct(key, msg)
17
18def Laws.Sign.length(key, msg):
19  P.sign_len(key, msg)
20
21def Laws.Verify.value(key, msg, tag):
22  %P.sign_correct(key, msg) : {Subtle.eq(MAC.sign(key, msg), tag) == SubtleSpec.equal(_, tag) : Bool}
23  SubtleLaws.Eq.value(MAC.sign(key, msg), tag)
24
25def Laws.Verify.accepts(key, msg):
26  SubtleLaws.Eq.refl(MAC.sign(key, msg))
27
28def Laws.Verify.sound(key, msg, tag, h):
29  Equal.sym(List<&2, U32>, MAC.sign(key, msg), tag, SubtleLaws.Eq.sound(MAC.sign(key, msg), tag, h))
30
31def rejects(+key: List<&2, U32>, +msg: List<&2, U32>, +tag: List<&2, U32>, ne: {tag != MAC.sign(key, msg) : List<&2, U32>}, +b: Bool, +eb: {MAC.verify(key, msg, tag) == b : Bool}) -> {MAC.verify(key, msg, tag) == False{} : Bool}:
32  match b:
33    case True{}:
34      Empty.absurd({MAC.verify(key, msg, tag) == False{} : Bool}, ne(Laws.Verify.sound(key, msg, tag, eb)))
35    case False{}:
36      eb
37
38def Laws.Verify.rejects(key, msg, tag, ne):
39  rejects(key, msg, tag, ne, MAC.verify(key, msg, tag), {==})