Fine-grained oracle control over proof strategy

Skip to first unread message

Rob Lorch

Jan 12, 2023, 1:57:15 PMJan 12
to tamarin-prover

Oracles allow the user to rank proof goals. Sometimes proof goals have multiple possible cases for how they were generated-- is there any way for the user to specify the ordering of this case analysis? 

In other words-- In the following screenshot, the oracle orders the proof goals in the right pane. But, is there any way for the oracle to also order the case analysis in the left pane? Some cases for a proof goal may be more likely than others.

Screen Shot 2023-01-05 at 4.22.13 PM.png



Ralf Sasse

Jan 13, 2023, 4:45:38 AMJan 13
to, Rob Lorch

Hi Rob,

For a successful proof all cases in the left pane must be proven anyway, which is the historic reason why there is no option to reorder those cases.

Unfortunately, in a case like yours, where you want an instance for an exists-trace lemma (or equivalently when you expect an attack) this might be helpful, but sorry, it is not supported. It might be an interesting additional feature though.


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
To view this discussion on the web visit

Rob Lorch

Jan 13, 2023, 1:57:36 PMJan 13
to tamarin-prover
Hi Dr. Sasse,

This makes sense, thank you for your response.


Reply all
Reply to author
0 new messages