[Verifpal] Counter-example problem

[Maxime MERE]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20220915/57770696/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: issue.vp
Type: application/octet-stream
Size: 2892 bytes
Desc: issue.vp
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20220915/57770696/attachment-0001.obj>