diff options
| -rw-r--r-- | sof-dhcr.spthy | 21 |
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) ]-> [] |