[Verifpal] Authentication Fails on AEAD

Angèle Bossuat 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 
auth query.

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 
(tok||n), which
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, 
meaning the
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 --------------

principal Alice[
    knows private K,skA,tok
    pkA = G^skA

principal Bob[
    knows private K,skB,tok
    pkB = G^skB
    generates n
    sigB = SIGN(skB,n)
    encB = AEAD_ENC(K,CONCAT(n,sigB),nil)

Alice -> Bob : [pkA]

Bob -> Alice : [pkB],encB

principal Alice[
    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

principal Bob[
    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 mailing list