Model points at infinity as malicious public keysHEADmaster

If the server doesn't check that the user's public key is an identity
element O (point at infinity), authentication breaks down.

Because O^x = O, no matter the verification secret, the final result
will be: h(<O, challenge, O, username>). Username is assumed to be
public information in the model, and the challenge is openly sent into
the network. What's supposed to prove authenticity of the client via its
secret key and identity, now becomes a trivial universal backdoor with
the server challenge acting as a direct invitiation.

1 files changed, 19 insertions, 2 deletions

diff --git a/sof-dhcr.spthy b/sof-dhcr.spthy
index 8d4d141..aed4559 100644
--- a/sof-dhcr.spthy
+++ b/sof-dhcr.spthy
@@ -19,9 +19,20 @@ 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, 'g'^~sk), !UserSecret($U, ~sk), Out('g'^~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) ]
 
 /* Client begins the authentication flow by sending the username.
  * Honest participants know the secret key they must use for this.
@@ -65,12 +76,18 @@ 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) ]
+  [ In(response)
+  , ServerPending(username, ck)
+  , !ConfiguredUser(username, pk)
+  , ValidPK(pk)
+  ]
 --[ Accepted(username, pk, challenge) ]->
   []