help with partial deconstructions caused by iterative rules and equations.

[Nikodem Witkiewicz]

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.

[hua hua]

for partial deconstructions, i remember you can just use the command  tamarin-prover interactive . --auto-sources 

[Nikodem Witkiewicz]

Dear hua,
Thank you very much for your answer.

Yes, there is such an option. However, I reached a dead end with modeling HIDE in this way, so I completely reconstructed it. Also, if i remember correctly, the autosources failed.
I should have mentioned it in this thread earlier. Sorry that I haven't. Once again, thank you for your time. 

Best,
Nikodem

--
You received this message because you are subscribed to a topic in the Google Groups "Tamarin-prover" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tamarin-prover/aMfyC-Zp-Fg/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tamarin-prove...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/f7381ba5-5df8-4887-98bf-fe36cc7e10e4n%40googlegroups.com.