[Verifpal] Authentication Fails on AEAD
abossuat at quarkslab.com
Wed Dec 2 10:39:52 CET 2020
Hello all !
I have stumbled upon an issue (that might not actually be one) with the
Attached is a minimal example of my problem, for some basic token protocol,
where Alice and Bob both know a token tok and symmetric key K, and each
public key. Bob sends Alice a nonce n, and Alice has to answer with
Bob checks is correct. Every message is also signed.
Problem : when trying to see if Alice's reply is authentic, verifpal
tells me that an
attacker could replace Alice's reply with Bob's original encryption of
n, and since it
decrypts successfully, it is considered an attack... even though the
ASSERT call to
check that Alice sent tok||n will fail, and so will the signature check,
protocol will not finish its run.
> if this is a normal behavior, i.e., if we should see this as an
attack even though Bob
will immediately see that the message is incorrect via the
can I check the authenticity of the message ? via several
confidentiality queries ?
the main issue is that I cannot directly use the auth query on the
signature, as it was
sent encrypted and thus Bob and Alice have a different variable name for
Any thoughts ?
-------------- next part --------------
knows private K,skA,tok
pkA = G^skA
knows private K,skB,tok
pkB = G^skB
sigB = SIGN(skB,n)
encB = AEAD_ENC(K,CONCAT(n,sigB),nil)
Alice -> Bob : [pkA]
Bob -> Alice : [pkB],encB
nA,sigB_A = SPLIT(AEAD_DEC(K,encB,nil))
_1 = SIGNVERIF(pkB,nA,sigB_A)
sigA = SIGN(skA,CONCAT(tok,nA))
encA = AEAD_ENC(K,CONCAT(tok,nA,sigA),nil)
Alice -> Bob : encA
tokAB,nAB,sigA_B = SPLIT(AEAD_DEC(K,encA,nil))
_2 = ASSERT(CONCAT(tokAB,nAB),CONCAT(tok,n))?
_3 = SIGNVERIF(pkA,CONCAT(tokAB,nAB),sigA_B)?
authentication? Alice->Bob: encA
More information about the Verifpal