Reducible function symbols in a rule premises

[parad...@gmail.com]

Dear all,

I hope you are doing well.

I have a question regarding the usage of reducible function symbols (like
sdec) in a rule premise. As I understood, *-restricted protocols disallow
usage of reducible function symbols on the lhs in order to prevent pattern
matching on them. But suppose that I have the following two equations:

dec(enc(x,y),y) = x
enc(dec(x,y),y) = x

Now, both of the function symbols enc and dec are reducible. Does this mean
that I can not use In(enc(x,y)) or In(dec(x, y)) in a protocol rule? As I have
seen, Tamarin doesn't complain in this case and uses some preprocessing in
which In(enc(x,y)) replaces with In(z) for some variable z. Is this expected
behaviour?

Wish you all the best.

Regards,
Petar

[Ralf Sasse]

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.

[parad...@gmail.com]

Hi Ralf,

Thanks for the explanation, I didn't get any warning because I had an empty
conclusion. So, with both of the equations in place, if I'm expecting to get
"enc(z,k)" from the environment and extract "z", I should write something like

rule test:
   [ In(x), PrevState(~k) ]
   --[]->
   [ State(dec(x,~k)) ]

Now, I have two cases (variants) of the rule:
1) rule test:
       [ In(x), PrevState(~k) ]
       --[]->
       [ State(dec(x,~k)) ]

2) rule test:
       [ In(enc(z,~k)), PrevState(~k) ]
       --[]->
       [ State(z) ]

But the variant 1) is basically an oracle -- I can get anything from the
environment. Is there any way to enforce only variant 2)?

Regards,
Petar

[Ralf Sasse]

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.

[parad...@gmail.com]

Thank you for the explanation.

Regards,
Petar