Double BS-SPEKE is an doubly augmented PAKE

double-bs-speke.txt

Double BS-SPEKE

Double BS-SPEKE is BS-SPEKE but with 3DH vs Noise-KN to make it a doubly
augmented PAKE. Double BS-SPEKE is the best doubly augmented PAKE that I know
of. Only problem is there are no proofs, but it's not hard to take the SPEKE
proof, add the OPAQUE proof for OPRF, and it's obvious that the doubly augmented
change makes it doubly augmented. So if anyone knows how to formally state that
in a proof, that would be awesome to have. BS-SPEKE defined on multiplicative
groups can be found here:
https://gist.github.com/Sc00bz/ec1f5fcfd18533bf0d6bf31d1211d4b4

** Costs per step **
Double BS-SPEKE
C: H*i       ffI*iH****[iiii]         xi
S:    f**[ii]                f***[iii]

OPAQUE-3DH
C: Hx*[ii]            ffI*i***[iii]
S:        ffx***[iiii]

** Costs OPRF AKE **
Double BS-SPEKE
C: fHI**ii  fx***iiH*
S: f*i      f****i

OPAQUE-3DH
Costs OPRF AKE
C: fHI**ii  fx***i
S: f*i      fx***

*: Scalar point multiply
H: Hash to point which is Elligator or SWU (depending on implementation this may
   require a field invert if scalar point multiply needs affine points)
i: Field invert
I: Scalar invert
f: From bytes (field square root or free for Montgomery curves)
[ii...]: Field inverts that can be combined. Cost is 1 field invert and 3*(n-1)
         field multiplications.

Properties
Forward secrecy:     Yes
Not fragile:         Yes
Quantum annoying:    Yes
No precomputation:   Yes
Secure registration: Yes

** Registration **
Both have:
      idS = server identity
      hashToPoint() is Elligator or SWU
      G = standard generator
Client has:
      idC = client identity

C:    r = random()
C:    R = r * hashToPoint(H(password, idC, idS))
C->S: idC, R, settings
   S: Approve settings
   S: salt = random()
   S: R' = H(salt) * R
   S: b = random()
   S: B = b * G
C<-S: R', B
C:    BlindSalt = (1/r) * R'
C:    K_pw = pwKdf(password, BlindSalt, idC, idS, settings)
C:    p      = H(K_pw, pModifier)
C:    c      = H(K_pw, cModifier)
C:    s      = H(K_pw, sModifier)
C:    macKey = H(K_pw, macKeyModifier)
C:    P = hashToPoint(p)
C:    C = c * P
C:    regMac = MAC(macKey, B)
C:    a = random()
C:    A = a * G
C:    K_c = H(a * B [|| a * ServerPublicKey])
C:    encServerData = aead_encrypt(K_c, P || C || s || regMac)
C->S: A, encServerData
   S: K_s = H(b * A [|| serverPrivateKey * A])
   S: P || C || s || regMac = aead_decrypt(K_s, encServerData)
   S: store for idC: salt, settings, P, C, s, b (as reg), regMac

** Use **
Client and server have:
      idS = server identity
      hashToPoint() is Elligator or SWU
      G = standard generator
Client with password has:
      idC = client identity
      password
Client without password has:
      idC = client identity
      P = hashToPoint(p)
      c
      S = s * P
      Reg = reg * G (reg = registration private key)
      (Note p, c, and s are from the pwKdf())
Server has these for "idC":
      salt
      settings
      P = hashToPoint(p)
      C = c * P
      s
      reg = registration private key
      regMac = MAC(macKey, reg * G)
      (Note p, c, s, and macKey are from the pwKdf())

C:    r = random()
C:    R = r * hashToPoint(H(password, idC, idS))
C->S: idC, R
   S: R' = H(salt) * R
   S: b = random()
   S: B = b * P
C<-S: R', B, settings
C:    BlindSalt = (1/r) * R'
C:    K_pw = pwKdf(password, BlindSalt, idC, idS, settings)
C:    p      = H(K_pw, pModifier)
C:    c      = H(K_pw, cModifier)
C:    s      = H(K_pw, sModifier)
C:    macKey = H(K_pw, macKeyModifier)
C:    a = random()
C:    A = a * P
C:    K_c = H(idC, idS, A, B, a * B, c * B, s * A)
C:    verifierC = H(K_c, verifyCModifier)
C->S: A, verifierC[, encryptedDataC]
   S: K_s = H(idC, idS, A, B, b * A, b * C, s * A)
   S: Checks verifierC == H(K_s, verifyCModifier)
   S: verifierS = H(K_s, verifySModifier)
   S: sessionKey = H(K_s, sessionKeyModifier)
   S: encReg = aead_encrypt(sessionKey, reg || regMac)
C<-S: verifierS, encReg[, encryptedDataS]
C:    Checks verifierS == H(K_c, verifySModifier)
C:    sessionKey = H(K_c, sessionKeyModifier)
C:    reg || regMac = aead_encrypt(sessionKey, encReg)
Client with password does:
C:    Checks regMac == MAC(macKey, reg * G)
Client without password does:
C:    Checks Reg == reg * G

On success K_c == K_s, thus derived verifiers and encryption keys are the same.

When receiving a point, you must check it is valid and not a low order point.
When using random() to generate a scalar, you should generate a larger value and
modulo by one less than the order then add 1 or generate a value [1, order) with
rejection sampling. This makes sure it is uniformly distributed and not zero.
Similar should be done for H() when generating fields to avoid bad values. For
generating a scalar for X25519 you could just use X25519's clamping. Note that a
clamped scalar doesn't have full coverage and there is a theoretical info
leakage. If you observe 2^100 successful exchanges, then with 2^255 memory and
2^223 work you can eliminate less than 1 in 200 million password guesses
offline. Thus every 200 million online guesses you get one free (ie never will
happen, impossible, and you get a worthless attack). To "fix" this you could
generate a random number like this:
order = 2^252 + 27742317777372353535851937790883648493
r = 8 * random([1, (order - 1) / 2])
or
r = random([8, 8 * ((order - 1) / 2) + 7]) & ~7

For X25519, you'll want to have r be a multiple of 8 and swap r and 1/r. This is
so you multiply the point out of your control by a multiple of 8. So you can
check for zero. If the only functions available always clamp before scalar
multiplication then generate r and 1/r ("rInv") like this:
order   = 2^252 + 27742317777372353535851937790883648493
r       = clamp(random())
rInvPos = (r ^ (order - 2)) % (8 * order)
rInvNeg = 8 * order - rInvPos
rInv    = ((rInvPos >> 254) & 1) ? rInvPos : rInvNeg  // do bit select
if ((rInv >> 254) & 1) == 0 // "rInv != clamp(rInv)"
  // This happens <1 in 2^100
  // When both rInvPos and rInvNeg's 254th bit are 0
  restart

Note "H(salt) * R" vs "salt * R", this is so you don't need to store a large 
salt. A salt of just 128 to 256 bits is fine once expanded to the required
length.