What is an "impossible chain"?

[Simon BOUGET]

Hi all,

I am trying to prove an "exists-trace" lemma, and by manual exploration, I found the trace that I expect from my protocol.

However, this trace is discarded by Tamarin, "by contradiction /* impossible chain */".

Which I don't understand, because when I click on the hyperlink on "contradiction", it does show me a picture of the chain, and it seems very possible to me, it's exactly the one I expect.

So what does it mean for this trace to be discarded because of an "impossible" chain?

(I can provide the picture in question if it's helpful, but I'm more interested in understanding the general meaning of this message, not why this specific one is rejected.)

Thanks,

Simon

[Cas Cremers]

Hi Simon,

"Impossible chains" are those that are detected by checking if it is possible to deduce the chain-end from the chain-start by extending the chain or replacing it with an edge. The underlying rationale is to discard some "future" contradictions early.

Best,

Cas

--
You received this message because you are subscribed to the Google Groups "tamarin-prover" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tamarin-prove...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/CABhg3H%3D8B1CdMmZnM%3DfZcC6QGs43tGBunyscXfXQ1WJ4ORQPjw%40mail.gmail.com.

[Simon BOUGET]

Hi Cas,

Thanks for the explanation. There was indeed a contradiction a few steps further, due to a typo in a variable name... Took me far too long to realize the issue, but thank you for helping me find it.

Best,

Simon

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/CABdrxL7ZJrVtCaupQ9gUswWp849N_gFdq%3Dj%3DTLrwgyhSXB7kQg%40mail.gmail.com.