Reloading a modified theory - how to do it quickly?

[rsasse]

During development of a theory it is often necessary to make small changes and reload the theory. The workflow for this is not very nice or efficient. Currently, I do the following:

• modify input spthy file
• alt-tab to command-line (where the tamarin executable is running)
• control-c (kill running tamarin)
• up-arrow, enter (to restart tamarin)
• alt-tab to browser
• click "Tamarin" button between "Running" and version number (top left)
• click the theory name I want to reload

I know that an alternative workflow could use the "Choose File" and "Load theory" buttons on the GUI main page, but that changes key presses for mouse movement, and is not any faster.

Is there any way we can envision making this faster? Possibly a button in the theory main page (where we list keyboard shortcuts and give a quick intro) to reload this theory? This would require storing which file the theory came from, but otherwise could be very nice.

Comments welcome, and if anyone wants to try their hand at this it would be a very nice quality-of-life improvement.

[mimoo]

If you could "watch" for file changes in the directory, and load new files automatically.

My current problem is that the file I'm working on takes ~30min to load, so every little change forces me to wait 30-min more in order to play again with the file. During development, and when things are not working correctly, it is quite annoying.

BTW, could that be because I'm having all these things in let...in? https://gist.github.com/mimoo/c08a128f2df2831c58a74ab83ac0b51c

[mpdehnel]

David: wow! What’s causing your file to take 30mins to load? Is it in the Maude stage, or in source pre-computation? (Is the terminal static or busy...?)

Martin

On 1 Feb 2019, at 23:20, David Wong notifications@github.com wrote:

If you could "watch" for file changes in the directory, and load new files automatically.

My current problem is that the file I'm working on takes ~30min to load, so every little change forces me to wait 30-min more in order to play again with the file. During development, and when things are not working correctly, it is quite annoying.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[mimoo]

I want to say source pre-computation, but what is Maude stage?

[rsasse]

So, even if Tamarin would "watch" for changes, the runtime would not improve actually. From what you say, the parse time (until you get the "server ready") seems to be fine, but what takes long is once you click on the file name in the GUI. At that point, pre-computation starts to compute all the variants, and this involves using Maude as the backend. I assume you are using latest version 1.4.1 (or some dev 1.5.1)? Your Maude version should be 2.7.1 also, but the newest Tamarin requires that anyway.

The let in bindings do not by themselves cause any slowdown, but your rules are quite large, which can lead to issues.

[galadran]

BTW, could that be because I'm having all these things in let...in? https://gist.github.com/mimoo/c08a128f2df2831c58a74ab83ac0b51c

Hi @mimoo,

I took a quick look at your theory. The long precomputation time is coming from an interaction between the Diffie Hellman equations and the XOR equations. In particular: rule Responder_ReadMsg1_WriteMsg2 generates 1200 variants, i.e. when you look at this rule under the equational theory, it is really 1200 different rules and Tamarin has to consider them all separately.

The term encrypted_rs is responsible, you can see by adding encrypted_rs = one to the start of the rule's let..in section and you will see Tamarin loads the file in about ~45 seconds or so. Still not wonderfully fast, but enough to show it is this one term which is the problem.

I'll have a think about whether there's an alternative way to fix this in your protocol, the idea would be to bind the encrypted_rs term so Tamarin knows "at compile time" that many of the 1200 variants are not possible.

Best, Dennis

[galadran]

A small improvement:

<       rs = sponge(input4) ⊕ encrypted_rs
---
>       rs = 'g'^unknownstatic
>       encrypted_rs = sponge(input4) ⊕ rs 

I think that this change is equivalent to your original specification, but it gives nearly a 3x speed up (~46 min to ~18min) for me. Essentially it says that the responder must unwrap a group element when it XORs the encrypted term with the keystream.

18 minutes is still far from ideal of course!

[kmilner]

Thanks @galadran for helping @mimoo out. For the issue itself, I agree we can definitely improve the workflow for reloading theories (one could imagine even allocating a particular number of cores to be used for precomputation in the background). I'll look into how doable that is to implement on Monday.

In terms of the long precomputation time @mimoo has, I think this points to a deficiency in the manual. Many of us know tricks for improving precomputation time because we have dug into the internal implementation, but I don't think that's adequately explained in the manual. I think it would be useful to have a section with a clear explanation of what is going on when you load a theory, why certain constructions are much slower than others, and what to look for and improve if it's causing issues.

[mimoo]

Thanks a lot for the help! Indeed, I was using senc/denc earlier instead of XOR to encrypt, and things were much faster. But I feel like that would be a bit of a cheat since I do use XOR to encrypt in the protocol (and then separately compute an authentication tag).

As for using the rs=g^unknown_static trick, that's great I will use that thanks :)

As for using a watch feature, it was more to avoid the "quit tamarin -> re-launch tamarin" workflow.

[mohitWrangler]

Here is a temporary hack that I use with Sublime Text Build

For each build execution, I launch the terminal with a specific window title ("tamarin-prover-interactive-sublime") and Tamarin prover command.

The shell_cmd variable in Sublime Text Build is as follows: -- "shell_cmd": "wmctrl -c \"tamarin-prover-interactive-sublime:Tilix: Default\" ; sleep 2 && tilix --maximize --title=\"tamarin-prover-interactive-sublime\" --command=\"bash -c \\\"PATH=$PATH:/home/linuxbrew/.linuxbrew/bin/ && $HOME/.local/bin/tamarin-prover interactive \\\\\"$file_name\\\\\" --prove ; while :; do read var; done\\\"\" & (sleep 3 && google-chrome \"http://127.0.0.1:3001\")"

The above command executes the following steps in order --

1. Close an existing terminal with the specific window tile which I specified when running the build each time. This closes the existing Tamarin Interactive session.
2. Launch the terminal again with Tamarin prover command and specific window title
3. Launch Google chrome with Tamarin session URL

Other Notes:

1. I use sleep command in between to ensure enough transition time.
2. The while loop after the command allows me to close the terminal manually if needed
3. You don't need to necessarily use the Tilix terminal.