[Verifpal] Authentication Fails on AEAD

Nadim Kobeissi nadim at symbolic.software
Fri Dec 4 16:27:50 CET 2020

Dear Angèle,

This analysis result appears to be completely correct to me. The ASSERT call occurs after Bob decrypts enca. So yes, the protocol does not finish its run, but Bob still manages to use the non-authentic enca before the protocol is aborted! Hence the result.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On Dec 2, 2020, at 10:39 AM, Angèle Bossuat via Verifpal <verifpal at lists.symbolic.software> wrote:
> 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 other's
> 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 ASSERT/SIGNVERIF, how
> 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 it...
> Any thoughts ?
> -
> Angèle
> <testAuth.vp>
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal

More information about the Verifpal mailing list