Dear Petar,
I tried what you described, and the equational theory with enc+dec canceling in either order is fine in theory. However then you cannot use either enc or dec on a LHS anymore due to the *-restrictedness you mention. With this snippet:
functions: enc/2, dec/2
equations: enc(dec(x,y),y)=x,
dec(enc(x,y),y)=x
rule test: [ In(enc(z,k)) ] --[]-> [ State(z) ]
I get the warning that it's not *-restricted, and it replaces the
LHS with a variable z.1, which leads to the RHS having an unbound
variable, and a non-executable rule. The tool does not abort
(maybe it should) but the warning tells you not to use it:
WARNING: ignoring the following wellformedness errors
Multiplication restriction of rules:
The following rule is not multiplication restricted:
rule (modulo E) test:
[ In( enc(z, k) ) ] --> [ State( z ) ]
After replacing reducible function symbols in lhs with
variables:
rule (modulo E) test:
[ In( x.1 ) ] --> [ State( z ) ]
Variables that occur only in rhs: z
So, Tamarin doing this replacement of 'enc(..)' by a different
variable is expected, and you should not try to use pattern
matching on the enc and dec in this scenario as the result may not
be what you expect.
Best regards,
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/82ad9c9a-8d9c-4a6c-a786-dfeab2d29a8fn%40googlegroups.com.
Hi Petar,
As enc is reducible in your model, both variants are possible and required. What you need to do (and check if it is appropriate for what you are trying to model!) is ensure that you can differentiate between successful and unsuccessful decryption. dec(x,~k) can indeed be anything. However, if success can be checked, you could format the messages x as pairs <'1',y> with the constant '1' as first argument of a pair, and then check that after decryption the result is a pair, with '1' as first argument. Again, as a warning, this means you assume that decryption success is visible, and it also means that the decrypted term cannot be another enc or dec term, as it's a pair. If all that would be fine you can change your rule to:
rule test:
[ In(x), PrevState(~k) ]
--[ Eq(fst(dec(x,~k)),'1') ]->
[ State(dec(x,~k)) ]
restriction equals: "All x y #i. Eq(x,y)@i ==> x=y"
and add the standard equality restriction from the manual (as
above). This checks that after decrypting, the first element of a
pair is the constant '1'. This should work, and due to the use of
the pair operator should not (but I did not try it) have nay
interference with the dec operator.
Best regards,
Ralf
To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/38a2c808-c6eb-43af-9d90-4625612afc86n%40googlegroups.com.