help with partial deconstructions caused by iterative rules and equations.

20 views

Skip to first unread message

Nikodem Witkiewicz

unread,

Jul 21, 2025, 9:36:39 AMJul 21

to Tamarin-prover

Dear All,

I'm working on my master's thesis, where I focus on cryptography using bilinear pairings. I'm trying to model the basic HIDE scheme described here: HIDE-scheme. Since using the built-in bilinear pairing features caused non-termination, I have written my own equations instead.

My implementation is not complete yet (there will be additional mechanisms to ensure that the parent's key is not revealed during the decryption process), but I'm currently struggling with a problem I can't solve on my own. Namely, I am unable to prove message secrecy due to partial deconstructions.

I have not yet included the rule that reveals the key. Therefore, secrecy should hold — but I am not able to formally prove it. I’ve read about partial deconstructions in the book and the manual, but I still can't resolve the issue.

I'm attaching my model. Note there are some lemmas leading to proper decryption existance. I also acknowledge the warnings. As far as i understand them, they result form a possible counter reduction to -1, which Tamarin's natural-numbers built-in does not support. The model does not consider such a situation, so you may skip it.

I would appreciate any advice on solving the problem, and also on the model. itself.