generate n values and randomly select one, how to model?

[mmhuang]

Hi all. 

    I  designed a protocol where one of the steps is to generate n values ​​according to a specified algorithm and randomly select one of them to use. How should this be modeled in tamarin?

   Could anyone can provide solution.

   Thanks. 

[Ralf Sasse]

Hi,

Very abstractly: is what comes out of this a random value? If so, just using a Tamarin fresh variable seems the most appropriate abstraction.

As you say this is generated by an algorithm, I wonder if all these values are deterministic? Then the above abstraction would be too strong. You could then create a Fact with all those computed values (however you model each computation, this may be difficult) and have them in there in a multiset, and in the next rule just pick one element from the multiset (which would actually check that the protocol is secure independent of which value was chosen)

So, one rule has

... -> ComputedValues(x1 + x2 + x3 + x4)

Next rule has

ComputedValues(Chosen+ Rest) --> .. use Chosen here...

Note that this may be more tricky to get right, and is not easy. Having an actual random value would be a lot simpler.

Cheers,
Ralf

--
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 on the web visit https://groups.google.com/d/msgid/tamarin-prover/2b657740-1343-4762-87a7-3930623c00c4n%40googlegroups.com.