8 partial deconstructions when I try to implement a timeout rule.

[A. Y.]

Hi, I'm working on a challenge-response protocol that can detect prover response losses. The idea was for the prover itself to be the observer of the detection, receiving a challenge where the verifier's state doesn't match the prover's updated state.
However, to implement response loss detection, I need to include a challenge timeout rule. This prevents deadlocks due to the fact that the verifier is stateful and, once it sends a challenge, would remain in the verify state forever if we don't implement the timeout.
However, as soon as I insert the timeout rule, the GUI displays eight partial constructions, causing almost all my lemmas to fail.

rule Register:

    [ ... ]

  --[ ... ]-->

    [ ...

      St_V_Challenge(~idV, %1, 'null'),

      ... ]

rule V_challenge:

    [ ...

      St_V_Challenge(~idV, %prev_cP, prev_nP),

      Fr(~ch),

      ... ]

  --[ ... ]-->

    [ ...

      St_V_Verify(~idV, %prev_cP, prev_nP, ~ch),

      ... ]

rule V_timeout:

    [ ...

      St_V_Verify(~idV, %prev_cP, prev_nP, ~ch),

      ... ]

  --[ ... ]-->

    [ ...

      St_V_Challenge(~idV, %prev_cP, prev_nP),

      ... ]

[Nikodem Witkiewicz]

Hi,
There are a few options for solving partial deconstructions.
You may:

• use the --auto-sources flag;
• resolve them yourself by writing source lemmas;
• use some modelling tricks (check out the manual).

I highly recommend reading Tamarin book and the manual. 

Cheers,

Nikodem

--
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 visit https://groups.google.com/d/msgid/tamarin-prover/7163b2e9-0c94-4414-af06-685ec4616257n%40googlegroups.com.