src/crypto/kex.bend

bend-collections-laws-crypto@1.0.0.0 · 66 lines · 9 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/curve25519/field.bend as F
4
5# Key exchange: X25519 (RFC 7748). Keys and secrets are 32-byte lists of U32
6# values below 256; malformed input is rejected as a value (None).
7#
8#   generate_keypair(seed)   the secret is the 32-byte seed (clamped inside
9#                            X25519), the public key X25519(secret, 9)
10#   generate_keypair_os()    the same from 32 bytes of IO.random_u32
11#   shared_secret(sk, pk)    X25519(sk, pk); None when either input is
12#                            malformed or the result is all zero (a
13#                            small-order peer key, RFC 7748 section 6.1)
14#
15# Correctness against RFC 7748 is proved (spec/crypto/kex.bend,
16# proofs/crypto/curve25519). The ladder is branch-free on secrets; Bend
17# has no timing model, so constant time is by construction, not proved.
18
19type Keypair is Data:
20  Keypair{secret: List<&2, U32>, public: List<&2, U32>}
21
22def keypair_of(+seed: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, Keypair>:
23  match m:
24    case None{}:
25      None{}
26    case Some{pk}:
27      Some{Keypair{seed, pk}}
28
29def generate_keypair(+seed: List<&2, U32>) -> Maybe<&2, Keypair>:
30  keypair_of(seed, X.x25519(seed, X.base()))
31
32# 32 bytes from 8 words, little-endian
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 nonzero(ss: List<&2, U32>, z: Bool) -> Maybe<&2, List<&2, U32>>:
52  match z:
53    case True{}:
54      None{}
55    case False{}:
56      Some{ss}
57
58def shared_of(m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
59  match m:
60    case None{}:
61      None{}
62    case Some{+ss}:
63      nonzero(ss, U32.is_eq(F.sum_all(ss, 0), 0))
64
65def shared_secret(+sk: List<&2, U32>, +pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
66  shared_of(X.x25519(sk, pk))