Revert "Model points at infinity as malicious public keys"HEADmaster

This reverts commit c48736a18976a8d1c62fec3dbfa5c8c4dce38bc6.

The authentication indeed breaks down if an identity element is provided
as a public key, but this is merely a specific variant of a more
general algebraic issue.

What actually matters is rejecting points at infinity when they appear
*as the result of the secret derivation* (the exponentiation), not
as the client public keys. This might happen whenever an element from
any non-prime subgroup is used in secret derivation.

All-zero shared secrets must be rejected. This is correct, robust, and
doesn't rely on enumeration of all possible "bad" curve points.

This is tricky to model because Tamarin's Diffie-Hellman primitives
assume prime-order group, but implementations usually aren't. In
particular, X25519 has a cofactor and thus small-order points that end
up as an identity element after multiplying them by a clamped scalar.

One such point is:
e0eb7a7c3b41b8ae1656e3faf19fc46ada098deb9c32b1fd866205165f49b800

Checks remain implicit in the model, but must be explicitly done in
real implementations.

1 files changed, 2 insertions, 19 deletions

diff --git a/sof-dhcr.spthy b/sof-dhcr.spthy
index aed4559..8d4d141 100644
--- a/sof-dhcr.spthy
+++ b/sof-dhcr.spthy
@@ -19,20 +19,9 @@ builtins: hashing, diffie-hellman
  * assumes both usernames and public keys to be nonsecret.
  */
 rule Setup:
-  let pk = 'g'^~sk
-  in
   [ Fr(~sk) ]
 --[ UserSecretKey($U, ~sk) ]->
-  [ !ConfiguredUser($U, pk), !UserSecret($U, ~sk), Out(pk), ValidPK(pk) ]
-
-/* User with an identity element as a certificate. Will render the
- * authentication meaningless as the shared secrets will also be identities.
- * It doesn't even matter what the user secret is.
- */
-rule SetupBad:
-  []
--->
-  [ !ConfiguredUser($U, DH_neutral) ]
+  [ !ConfiguredUser($U, 'g'^~sk), !UserSecret($U, ~sk), Out('g'^~sk) ]
 
 /* Client begins the authentication flow by sending the username.
  * Honest participants know the secret key they must use for this.
@@ -76,18 +65,12 @@ rule ClientResponse:
  *
  * - Client and server agree on the rest of the parameters: challenge, pk,
  *   username, exactly as they've been transmitted and seen.
- *
- * - Public key was valid, in particular, it wasn't the identity element.
  */
 rule ServerAuthFinish:
   let challenge = 'g'^ck
       response = h(<pk^ck, challenge, pk, username>)
   in
-  [ In(response)
-  , ServerPending(username, ck)
-  , !ConfiguredUser(username, pk)
-  , ValidPK(pk)
-  ]
+  [ In(response), ServerPending(username, ck), !ConfiguredUser(username, pk) ]
 --[ Accepted(username, pk, challenge) ]->
   []