src/crypto/sign.bend

bend-collections-laws-crypto@1.0.0.0 · 69 lines · 10 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/ed25519.bend as E
4
5# Signatures: Ed25519 (RFC 8032). Keys and signatures are byte lists (U32
6# values below 256) of the RFC lengths; malformed ones are rejected as
7# values.
8#
9#   generate_keypair(seed)   secret = the 32-byte seed, public = [s]B
10#   generate_keypair_os()    the same from 32 bytes of IO.random_u32
11#   sign(sk, msg)            the 64-byte signature, None for a bad key
12#   verify(pk, msg, sig)     True iff sig is valid (cofactorless check,
13#                            non-canonical S >= L rejected)
14#
15# Correctness against RFC 8032 is proved (spec/crypto/sign.bend,
16# proofs/crypto/ed25519). Scalar multiplication and scalar arithmetic are
17# branch-free on secrets; Bend has no timing model, so constant time is by
18# construction, not proved.
19
20type Keypair is Data:
21  Keypair{secret: List<&2, U32>, public: List<&2, U32>}
22
23def keypair_if(+seed: List<&2, U32>, ok: Bool) -> Maybe<&2, Keypair>:
24  match ok:
25    case True{}:
26      Some{Keypair{seed, E.public_key(seed)}}
27    case False{}:
28      None{}
29
30def generate_keypair(+seed: List<&2, U32>) -> Maybe<&2, Keypair>:
31  keypair_if(seed, X.valid_bytes(32n, seed))
32
33def word_bytes(+w: U32, rest: List<&2, U32>) -> List<&2, U32>:
34  Con{U32.and(w, 255), Con{U32.and(U32.shrn(w, 8n), 255), Con{U32.and(U32.shrn(w, 16n), 255), Con{U32.shrn(w, 24n), rest}}}}
35
36def random_bytes(n: Nat, acc: List<&2, U32>) -> IO(List<&2, U32>):
37  match n:
38    case 0n:
39      IO.pure(List<&2, U32>, acc)
40    case 1n+m:
41      do IO<List<&2, U32>>:
42        w : U32 <- IO.try(U32, IO.random_u32())
43        rest : List<&2, U32> <- random_bytes(m, acc)
44        return word_bytes(w, rest)
45
46def generate_keypair_os() -> IO(Maybe<&2, Keypair>):
47  do IO<Maybe<&2, Keypair>>:
48    seed : List<&2, U32> <- random_bytes(8n, Nil{})
49    return generate_keypair(seed)
50
51def sign_if(+sk: List<&2, U32>, +msg: List<&2, U32>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
52  match ok:
53    case True{}:
54      Some{E.sign_raw(sk, msg)}
55    case False{}:
56      None{}
57
58def sign(+sk: List<&2, U32>, +msg: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
59  sign_if(sk, msg, X.valid_bytes(32n, sk))
60
61def verify_if(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, ok: Bool) -> Bool:
62  match ok:
63    case True{}:
64      E.verify_raw(pk, msg, sig)
65    case False{}:
66      False{}
67
68def verify(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
69  verify_if(pk, msg, sig, Bool.and(X.valid_bytes(32n, pk), X.valid_bytes(64n, sig)))