[Verifpal] Counter-example problem

Fri Oct 14 08:36:41 UTC 2022

Dear Nadim,

Thank you for replying to my message, I greatly appreciate your help.

I have analyzed your remarks and I do not exclude that the protocol may have a weakness.

However, I am not convinced that "Manufacturer" can arbitrarily sign corrupted messages:

Yes pkAlice can be MITMed line 106. The whole protocol aims at making sure that this cannot be used to forge messages.
About the risk for Manufacturer to sign arbitrary values, the ASSERTs at lines 80 and 81 are supposed to avoid that. When I look at the Verifpal traces, I have the impression that these two asserts are not always taken into account.

As example here is another extract of the traces proposed by Verifpal. I highlighted in yellow some ASSERT that is supposed to fail yet, the protocol seems to continue:

Result • authentication? Alice -> Soc: newownershipproof — When:
…

SIGN(skman, uid0) is obtained:
            pkalice → G^nil ← mutated by Attacker (originally G^skalice)
            batchrootproof → SIGN(skman, HASH(HASH(uid0), HASH(uidn)))
            a_batchroot → HASH(HASH(uid0), HASH(uidn))
            bp1 → ASSERT(HASH(HASH(uid0), HASH(uidn)), HASH(HASH(uid0), HASH(uidn)))?
            bp2 → nil
            salt → nil ← mutated by Attacker (originally salt)
            newbatchroot → uid0 ← mutated by Attacker (originally HASH(HASH(uid0), HASH(salt)))
            newbatchrootproof → uid0 ← mutated by Attacker (originally SIGN(skalice, newbatchroot))
            bp3 → ASSERT(HASH(HASH(uid0), HASH(nil)), uid0)?
            bp4 → SIGNVERIF(G^skalice, uid0, uid0)?
            newownershipproof → SIGN(skman, uid0) ← obtained by Attacker
            bp5 → SIGNVERIF(G^skman, SIGN(skalice, HASH(HASH(uid0), HASH(salt))), SIGN(skman, uid0))?
…

nil is obtained:
            pkalice → G^nil ← mutated by Attacker (originally G^skalice)
            batchrootproof → SIGN(skman, HASH(HASH(uid0), HASH(uidn)))
            a_batchroot → HASH(HASH(uid0), HASH(uidn))
            bp1 → ASSERT(HASH(HASH(uid0), HASH(uidn)), HASH(HASH(uid0), HASH(uidn)))?
            bp2 → nil ← obtained by Attacker
            salt → nil ← mutated by Attacker (originally salt)
            newbatchroot → HASH(HASH(uid0), HASH(nil)) ← mutated by Attacker (originally HASH(HASH(uid0), HASH(salt)))
            newbatchrootproof → uid0 ← mutated by Attacker (originally SIGN(skalice, newbatchroot))
            bp3 → ASSERT(HASH(HASH(uid0), HASH(nil)), HASH(HASH(uid0), HASH(nil)))?
            bp4 → SIGNVERIF(G^skalice, HASH(HASH(uid0), HASH(nil)), uid0)?
            newownershipproof → SIGN(skman, uid0) ← mutated by Attacker (originally SIGN(skman, newbatchrootproof))
            bp5 → nil ← obtained by Attacker
            bp6 → ASSERT(HASH(HASH(uid0), HASH(nil)), HASH(HASH(uid0), HASH(nil)))?
            bp7 → nil ← obtained by Attacker
            bp8 → SIGNVERIF(G^nil, HASH(HASH(uid0), HASH(nil)), uid0)?
            newownershipproof (SIGN(skman, uid0)), sent by Attacker and not by Alice, is successfully used in SIGNVERIF(G^skman, uid0, SIGN(skman, uid0))? within Soc's state.

Best regards,

Maxime

ST Restricted
From: Nadim Kobeissi <nadim at symbolic.software>
Sent: mardi 11 octobre 2022 14:54
To: Maxime MERE <maxime.mere at st.com>
Cc: verifpal at lists.symbolic.software; Frédéric Jouault <frederic.jouault at eseo.fr>
Subject: Re: [Verifpal] Counter-example problem

Dear Maxime,

Apologies for the delay: I was on vacation in September and have since been catching up on things in October.

I am not at all certain, because I haven’t taken the time necessary to fully understand your relatively complex model, but I don’t think that Verifpal is giving you a false positive here. Have you taken into account the fact that...

  *   pkAlice can be MITMed when sent from Alice to SoC on line 103?
  *   Manufacturer can be made to sign arbitrary values using skMan on line 83, if the attacker MITMs newBatchRootProof on line 76 as it’s being transmitted from Alice to Manufacturer?
  *   The arbitrary signature obtained above can then be replayed across subsequent executions of the protocol?

These three issues above seem to me like they could be the source of authentication-type attacks. Again: it’s up to you to confirm this, but to me, this model does not necessarily describe a secure protocol.

Thank you for your patience,

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

On 15 Sep 2022, at 11:50 AM, Maxime MERE via Verifpal <verifpal at lists.symbolic.software<mailto:verifpal at lists.symbolic.software>> wrote:

Hi everyone,

I am a PhD student at ESEO in Angers, France and I’m currently working on a blockchain-based protocol to enable new System-on-Chip features for STMicroelectronics.
 As part of my research, I’ve modeled protocols with VerifPal, and I would like to share with you some issues I have in understanding the counter-examples that VerifPal gives me. Indeed, it seems to me that the found error is actually a false positive. I’ve tested my model with 0.26 and 0.27 versions but I have not tested on other versions.

I have copied below the trace given by VerifPal, and the corresponding code is attached to this message.

In my protocol there are several successive checks. It seems to me that earlier checks should stop the iteration, but VerifPal continues exploring it.

Could you please help me clarify this issue?

Best regards,

Maxime

NB: The trace of the error found by Verifpal (you can see that bp3, bp4 and bp8 are checks that shouldn’t pass):

Result • authentication? Alice -> Soc: newbatchrootproof — When:
            batchrootproof → SIGN(skman, HASH(HASH(uid0), HASH(uidn)))
            a_batchroot → HASH(HASH(uid0), HASH(uidn))
            bp1 → ASSERT(HASH(HASH(uid0), HASH(uidn)), HASH(HASH(uid0), HASH(uidn)))?
            bp2 → nil
            salt → nil ← mutated by Attacker (originally salt)
            newbatchroot → uid0 ← mutated by Attacker (originally HASH(HASH(uid0), HASH(salt)))
            newbatchrootproof → uid0 ← mutated by Attacker (originally SIGN(skalice, newbatchroot))
            bp3 → ASSERT(HASH(HASH(uid0), HASH(nil)), uid0)?

            nil is obtained:
            uid0 → nil ← mutated by Attacker (originally uid0)
            batchrootproof → SIGN(skman, HASH(HASH(uid0), HASH(uidn)))
            a_batchroot → HASH(HASH(uid0), HASH(uidn))
            bp1 → ASSERT(HASH(HASH(uid0), HASH(uidn)), HASH(HASH(uid0), HASH(uidn)))?
            bp2 → nil ← obtained by Attacker
            salt → nil ← mutated by Attacker (originally salt)
            newbatchroot → HASH(HASH(uid0), HASH(nil)) ← mutated by Attacker (originally HASH(HASH(uid0), HASH(salt)))
            newbatchrootproof → uid0 ← mutated by Attacker (originally SIGN(skalice, newbatchroot))
            bp3 → ASSERT(HASH(HASH(uid0), HASH(nil)), HASH(HASH(uid0), HASH(nil)))?
            bp4 → SIGNVERIF(G^skalice, HASH(HASH(uid0), HASH(nil)), uid0)?
            newownershipproof → SIGN(skman, uid0)
            bp5 → SIGNVERIF(G^skman, SIGN(skalice, HASH(HASH(uid0), HASH(salt))), SIGN(skman, uid0))?
            bp6 → ASSERT(HASH(HASH(uid0), HASH(nil)), HASH(HASH(uid0), HASH(nil)))?
            bp7 → nil ← obtained by Attacker
            bp8 → SIGNVERIF(G^skalice, HASH(HASH(uid0), HASH(nil)), uid0)?
            newbatchrootproof (uid0), sent by Attacker and not by Alice, is successfully used in SIGNVERIF(G^skman, uid0, SIGN(skman, uid0))? within Soc's state.

ST Restricted
<issue.vp>
_______________________________________________
Verifpal mailing list
Verifpal at lists.symbolic.software<mailto:Verifpal at lists.symbolic.software>
https://lists.symbolic.software/mailman/listinfo/verifpal

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20221014/930f10de/attachment-0001.htm>