https://dannyvanheumen.nl/post/simple-asymmetric-ake/ Timelessness Timelessnessless? * Home * About * Posts (c) 2024. All rights reserved. A simple, asymmetric AKE Sat, Mar 23, 2024 A simple, (as-of-yet unidentified) asymmetric Authenticated Key Exchange Contents * Introduction * The Design * Protocol + Insights * Analysis * Symbolic prover + Open issue * Changelog In an experiment, I came across a need for a simple authenticated key exchange. It started as a stop-gap measure that is just a key exchange, no considerations for any kind of attacker. Just the minimal working solution with standard building blocks. From there, I extended the solution to protect against an attacker. I am still somewhat expecting to have either missed an (obvious) error or have failed to identify a known, documented AKE. Introduction The use-case is a user and a "service-provider" (of some kind, in my case a device). The device only responds to requests, performs computations in a separate computing environment and is, in this particular case, connected by USB port. There is sensitive information involved. The device, however, does not have storage capability. Everything is based on and initiated through the input of the user that interacts with the device. Initiative lies with the user; all risk lies with the judgement of the user whether or not the session is established correctly. From the device's perspective, it only needs to act on requests, we can assume that if the user is willing to interact with it, it must be safe to respond. Or from a different perspective: if the user is willing to send their security-sensitive information, then it must be okay to do perform the computation and respond. A confidential session that additionally guarantees the (only) other party is the one that initiated the session, is all that is needed. This party supplies the data, and receives the results. From the user's perspective, there are additional concerns: the user must be ensured that the device is the actual device that it expects, i.e. there can be no mistaken identity, and they must be sure that communication is secure, if they decide to continue after establishing a secure session, i.e. performing the AKE to completion. The Design requirements: * A two-party secure session is established between client and device, * Protected against MitM, * Ephemeral session-keys, * Device gets authenticated, * Client does not require authentication, * No need for a session ID, prerequisite: no (assumptions on) client's identity: The device starts off with only its own program state, needed for its own (internal) operation. Any data that device works with, is provided by client. This has the benefit that it cannot mistakenly expose sensitive data or mistake the identity of a user upon establishing a session. The device works with whatever data the initiator of the session provides. Client is only (implicitly) authenticated in that the secure session ensures that only the other party is able to communicate within the established session. prerequisite: session-scoped state: The device's state must be session-scoped, such that no data is leaked between sessions or spills over into next session, if applicable. Protocol The following is built on top of a Diffie-Hellman Key Exchange, with minimal practical adaptations to make it work in situations with an attacker. The protocol is proved for a passive attacker, with an attempt to prove for an active attacker currently stalled because of technical issues. with: * prefix pk_ indicating public key, and * prefix sk_ indicating secret/private key * digest = HASH(key, content) * ciphertext = ENCRYPT(key, plaintext) * plaintext = DECRYPT(key, ciphertext) * signature = SIGN(secret_key, content) * VALIDATE(public_key, signature, content) Precondition an identity pk_identity acquired at an earlier time. User Device ======================================================================== knows `pk_identity` knows `sk_identity`, `pk_identity` generates `sk_user`, `pk_user` User ----------------------------[pk_user]----------------------> Device generates `sk_device`, `pk_device` sessionkey = HASH(pk_user^sk_device, pk_device) signature = SIGN(sk_identity, pk_user) enc_sig = ENCRYPT(sessionkey, signature) User <----------------------[pk_device,enc_sig]------------------ Device sessionkey = HASH(pk_device^sk_user, pk_device) proof = DECRYPT(sessionkey, enc_sig) VALIDATE(pk_identity, proof, pk_user) Execution concludes successfully when the proof validates successfully. Any corruption results in failure to validate the signature. Given that all risk lies with the user, anything other than successful validation is reason for termination. After successful execution: * a confidential session is established with a shared, ephemeral session-key, * we are assured that pk_device is authentic, * we are assured that pk_user was received unchanged, * we are assured this is the authentic device, i.e. ownership over identity proved. Failed execution: * received pk_user is invalid/corrupted * received pk_device is invalid/corrupted * sessionkey cannot be produced due to pk_device * validation of pk_user fails due to: + proof is not authentic signature: o incorrect sessionkey o due to corrupted enc_sig o signature over corrupted pk_user + device does not own sk_identity Note: the protocol does not reflect the use of a prefix/context to prevent use of signature for other than identification. This may need to be considered when used. Insights * User's D-H public key doubles as challenge-nonce, therefore there is no opportunity to swap out the nonce for one with a known signature, and not freely selectable because that requires a corresponding private key. * The challenge-response signature is encrypted with established session-key, thus preventing (raw) replay of the response-message. * Device's D-H public key, additionally, is used as input in keyed-hash, with D-H's resulting shared secret as key. Consequently, both shared secret and device's public key are fixed. In a two-party set-up, user's public key must therefore also be fixed if one expects to compute the same shared secret. * Given that there is no persistence and client is expected to initiate and provide data, device needs only to rely on a secure session to keep data confidential. Analysis At this time, I have not completed a full analysis of the protocol. The following is, thusfar, based on intuition and informal reasoning, directed by the notions of the eCK security-model, and later (partially) confirmed by results of a symbolic prover. Security properties for authenticated key exchange according to the extended Canetti-Krawczyk (eCK) model. * (Implicit) Key Agreement + client/device: by virtue of establishing a two-party secure session using ephemeral key exchange. * Key Confirmation + client: by implication of successful signature validation against pk_user. + device: by implication of client following up. * Known Key Security + Session keys are fully based on random data, with contributions from both parties. * Security against Unknown Key Share attacks + Only 2 participants in the key exchange. Proper use of D-H prevents MitM. Only two parties involved, therefore no need to share or otherwise relay keys. + device: assume that any counterpart in established secure session is valid. Further made acceptable by the fact that all data is provided by counterpart in session. Proper key exchange prevents interference from any third-party. + client: no need to share keys. Each session is freshly established. Sessions are always between one device and one client. * Security against Key Compromise Impersonation (KCI) attacks + The Identity keypair is only used for signing the challenge-nonce that is sent to the client. Therefore, there is no opportunity where a signature can be misinterpreted. * Forward Secrecy + The AKE is initiated with inputs based on random data, with the pre-shared identity public key being the only exception. Granted, the eCK model is (presumably) followed in spirit rather than strictly, as this is an asymmetric AKE and, for example, in case of Key Confirmation device does not get concrete confirmation. The requirements are such that this is not problem in practice. Symbolic prover The following Verifpal proof-script passes for a passive attacker. A session established by client with device is successful if the protocol is completed without failure. Note, though, that at the moment of completion, only client knows the results and whether it is safe to continue. This is okay, because client must be convinced that device is authentic and communication is secure, before requesting device's services and sending data. The Verifpal proof-script: attacker[passive] principal Device[ knows private identity_secret identity = G^identity_secret ] // Assume knowledge of identity public key prior to initiation of the AKE. // (Modeled here as a guarded/guaranteed transfer: '[identity]') Device -> User: [identity] principal User[ generates dhe_user_secret dhe_user_public = G^dhe_user_secret ] // Initiation of a secure session. User -> Device: dhe_user_public principal Device[ generates dhe_device_secret dhe_device_public = G^dhe_device_secret ss_device = dhe_user_public^dhe_device_secret sessionkey_device = HASH(ss_device, dhe_device_public) signature = SIGN(identity_secret, dhe_user_public) proof_encrypted = ENC(sessionkey_device, signature) ] Device -> User: dhe_device_public,proof_encrypted principal User[ ss_user = dhe_device_public^dhe_user_secret sessionkey_user = HASH(ss_user, dhe_device_public) proof = DEC(sessionkey_user, proof_encrypted) _ = SIGNVERIF(identity, dhe_user_public, proof)? ] queries[ confidentiality? identity_secret confidentiality? dhe_device_secret confidentiality? dhe_user_secret confidentiality? ss_device confidentiality? ss_user confidentiality? sessionkey_device confidentiality? sessionkey_user freshness? dhe_user_secret freshness? dhe_device_secret freshness? ss_device freshness? ss_user freshness? sessionkey_device freshness? sessionkey_user equivalence? ss_user, ss_device equivalence? sessionkey_user, sessionkey_device equivalence? proof, signature // Authentication-queries provide no significance with a passive attacker. authentication? User -> Device: dhe_user_public authentication? Device -> User: dhe_device_public authentication? Device -> User: proof_encrypted ] The current issue with the "active attacker" analysis, is that the symbolic prover will prematurely fail on successful manipulation of the intermediate values, such as ss_device, ss_user, etc. The argument is that confidentiality is broken. The queries should be performed after the protocol completes (success)fully. SIGNVERIF(identity, dhe_user_public, proof)?, a checked (?) verification statement, should fail for any manipulation of dhe_user_public as the signature is validated against the original /authentic dhe_user_public generated by client. However, it does not. Therefore it proceeds to list all the violations of confidentiality of intermediate variables that are the possible as a result of corrupting the transferred dhe_user_public. By my (informal) reasoning, if an attacker corrupts any data, client's final signature validation must fail. Therefore, if final validation succeeds, authentic data must have been used and an attacker did not manipulate the established secure session. Open issue The issue is reported to Verifpal. Unfortunately, at the time of writing, there has not been any follow-up yet. A reduced sample is used to further narrow down the problem as part of the email conversation. The protocol, when analyzed for an active attacker, produces a result that need never happen. The claim is: with a nil (corrupted) public key, a nil message, and a nil signature, the validation would pass. This is correct of course. However, given that client itself generates pk_user, there is no need to insert any received (potentially corrupted) value. Therefore, the failing case need never occur. Changelog This article will receive updates, if necessary. * 2024-03-23 Typos, formatting. * 2024-03-23 Initial version.