spec/crypto/sign.bend

bend-collections-laws-crypto@1.0.0.0 · 32 lines · 6 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/sign.bend as SG
5
6# The contract of src/crypto/sign.bend (Ed25519 signatures, RFC 8032).
7# `one` is the symbolic 1 of spec/crypto/curve25519/field.bend.
8#
9#   clause          statement
10#   Sign.keypair    generate_keypair(seed) is the seed with the public key
11#                   public_key(seed) of spec/crypto/ed25519.bend
12#   Sign.sign       sign(sk, msg) is the RFC 8032 signature sign(sk, msg)
13#   Sign.verify     verify(pk, msg, sig) is the RFC 8032 verdict
14#   Sign.reject     a malformed seed, key or signature gives None / False
15
16def Sign.keypair(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> Type:
17  {SG.generate_keypair(seed) == Some{SG.Keypair{seed, SE.public_key(one, seed)}} : Maybe<&2, SG.Keypair>}
18
19def Sign.sign(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +msg: List<&2, U32>, +hs: {FS.tight(sk) == True{} : Bool}) -> Type:
20  {SG.sign(sk, msg) == Some{SE.sign(one, sk, msg)} : Maybe<&2, List<&2, U32>>}
21
22def Sign.verify(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, +hp: {FS.tight(pk) == True{} : Bool}, +hg: {FS.bytes_ok(64n, sig) == True{} : Bool}) -> Type:
23  {SG.verify(pk, msg, sig) == SE.verify(one, pk, msg, sig) : Bool}
24
25def Sign.reject_seed(+seed: List<&2, U32>, +h: {FS.tight(seed) == False{} : Bool}) -> Type:
26  {SG.generate_keypair(seed) == None{} : Maybe<&2, SG.Keypair>}
27
28def Sign.reject_key(+sk: List<&2, U32>, +msg: List<&2, U32>, +h: {FS.tight(sk) == False{} : Bool}) -> Type:
29  {SG.sign(sk, msg) == None{} : Maybe<&2, List<&2, U32>>}
30
31def Sign.reject(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, +h: {Bool.and(FS.tight(pk), FS.bytes_ok(64n, sig)) == False{} : Bool}) -> Type:
32  {SG.verify(pk, msg, sig) == False{} : Bool}