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