[Verifpal] Counter-example problem

[Nadim Kobeissi]

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> 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 <https://lists.symbolic.software/mailman/listinfo/verifpal>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20221011/1023a331/attachment.htm>