spec/crypto/kex.bend

bend-collections-laws-crypto@1.0.0.0 · 33 lines · 5 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/curve25519/x25519.bend as S
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/kex.bend as K
5
6# The contract of src/crypto/kex.bend (X25519 key exchange, RFC 7748).
7# `one` is the symbolic 1 of spec/crypto/curve25519/field.bend.
8#
9#   clause          statement
10#   Kex.public      generate_keypair(seed) has the public key X25519(seed, 9)
11#   Kex.shared      shared_secret(sk, pk) is X25519(sk, pk), or None when it
12#                   is all zero (RFC 7748 section 6.1)
13#   Kex.reject      malformed input gives None
14
15def base() -> List<&2, U32>:
16  [9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
17   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
18
19def unless_zero(ss: List<&2, U32>, z: Bool) -> Maybe<&2, List<&2, U32>>:
20  match z:
21    case True{}:
22      None{}
23    case False{}:
24      Some{ss}
25
26def Kex.public(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> Type:
27  {K.generate_keypair(seed) == Some{K.Keypair{seed, S.x25519(one, seed, base())}} : Maybe<&2, K.Keypair>}
28
29def Kex.shared(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +pk: List<&2, U32>, +hs: {FS.tight(sk) == True{} : Bool}, +hp: {FS.tight(pk) == True{} : Bool}) -> Type:
30  {K.shared_secret(sk, pk) == unless_zero(S.x25519(one, sk, pk), Nat.is_eq(FS.value(S.x25519(one, sk, pk)), 0n)) : Maybe<&2, List<&2, U32>>}
31
32def Kex.reject(+sk: List<&2, U32>, +pk: List<&2, U32>, +h: {Bool.and(FS.tight(sk), FS.tight(pk)) == False{} : Bool}) -> Type:
33  {K.shared_secret(sk, pk) == None{} : Maybe<&2, List<&2, U32>>}