Unexpected parsing error

[Alessandro Zanatta]

Dear all,

I'm Alessandro Zanatta, bachelor student in Computer Science at the University of Udine, Italy. I'm using Tamarin for my thesis and I was trying to model DH with possibly small/bad groups.

I'm having some errors I cannot understand. You can find a minimal example that reproduces the problem here:

theory non_working_DH

begin

builtins: diffie-hellman

functions:

  dhExp/3,

  WEAK_MODULO/0,

  STRONG_MODULO/0,

  BAD_ELEMENT/0,

  GOOD_ELEMENT/0

equations:

  dhExp(WEAK_MODULO,   g,           e) = BAD_ELEMENT,

  dhExp(STRONG_MODULO, BAD_ELEMENT, e) = BAD_ELEMENT,

  dhExp(STRONG_MODULO, g,           e) = g^e

end

Here is the error it gives (tamarin-prover non-working-DH.spthy):

maude tool: 'maude'
checking version: 3.0. OK.
checking installation: OK.

tamarin-prover: "non-working-DH.spthy" (line 16, column 43):
unexpected "^"
expecting ",", "heuristic", "builtins", "options", "functions", "equations", "restriction", "axiom", "lemma", "rule", letter, "!", "lookup", conditional process (with
equality), conditional process (with predicate), "new", "in", "out", "insert", "delete", "lock", "unlock", "event", "[", "0", identifier, "let", "(", predicates, "#ifd
ef", "#define" or "end"
CallStack (from HasCallStack):
 error, called at src/Theory/Text/Parser/Token.hs:148:21 in tamarin-prover-theory-1.6.0-4xY8tGI4gcd2kXzIGyjzDc:Theory.Text.Parser.Token

and here is the version of Tamarin I'm using (tamarin-prover -V):

tamarin-prover 1.6.0, (C) David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, Benedikt Schmidt, ETH Zurich 2010-2020
Git revision: a631d75fb82ed2d662c05981ce571d61aeb5ae09, branch: master
Compiled at: 2021-03-31 14:14:41.4334603 UTC

I've checked the manual, but it seems like I cannot add any equation which uses symbols from the builtin DH (it works just fine if I use 'g' instead of 'g^e', while using 'g*e' (just as a test) also gives a similar error), is that expected? If so, do you have any suggestion on how to proceed to model this?

Regards,
Alessandro

[Jannik Dreier]

Dear Allessandro,

The error message is not very clear, but essentially Tamarin does not
accept the usage of builtin symbols in user-defined equations (here: g^e
in your last equation) as this can potentially break soundness.

Best regards,
Jannik

On 28/06/2021 09:06, Alessandro Zanatta wrote:
>
> Dear all,
>
> I'm Alessandro Zanatta, bachelor student in Computer Science at the
> University of Udine, Italy. I'm using Tamarin for my thesis and I was
> trying to model DH with possibly small/bad groups.

> I've checked the manual, but it seems like I cannot add any equation
> which uses symbols from the builtin DH (it works just fine if I use 'g'
> instead of 'g^e', while using 'g*e' (just as a test) also gives a
> similar error), is that expected? If so, do you have any suggestion on
> how to proceed to model this?
>
> Regards,
> Alessandro
>

> --
> 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
> <mailto:tamarin-prove...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tamarin-prover/b5fae482-22cb-4c09-a218-5a9a980712a0n%40googlegroups.com
> <https://groups.google.com/d/msgid/tamarin-prover/b5fae482-22cb-4c09-a218-5a9a980712a0n%40googlegroups.com?utm_medium=email&utm_source=footer>.

--
Jannik Dreier
Maître de Conférences | Associate Professor
Université de Lorraine | TELECOM Nancy | LORIA
rese...@jannikdreier.net | +33 3 54 95 84 46

[Dennis Jackson]

Hi Alessandro,

Cas Cremers and I did some work on small subgroup attacks in Tamarin. As part of that work, I modified Tamarin's equational theory to add:

id/0

id^x = id

This should suffice for your model above. We also showed how, with some additional steps, we could derive much accurate models of small subgroups and elliptic curve points, which might be interesting in itself for you.

You can find our patched version of Tamarin and our case studies here:

https://github.com/galadran/advanced-tamarin-dh

The paper describing how our models work is here:

https://dennis-jackson.uk/assets/pdfs/subgroups.pdf

Please feel free to reach out if you have any questions,

Best,

Dennis

[Alessandro Zanatta]

Hi,

I've read (most of) the paper. I think this is exactly what I was looking for. Thank you! That problem's solved, seems.

I've got another question, but that's not really inherent to the topic of this conversation. I'll send it here anyway though, it probably is a rather easy fix - but I can't get my head around it.

I'm getting errors about pattern matching. I've created another basic example, here's the code:

theory patt_matching

begin

 

  builtins: asymmetric-encryption

  functions:

    higher_level_encrypt/2,

    higher_level_decrypt/2,

    lower_level_encrypt/2,

    lower_level_decrypt/2

  /*

   * I'd really like to keep on using my higher level functions as the lower level

   * one requires, in my case, deriving a session key and an IV (here I've skipped

   * the details about it and just used a placeholder).

   */

  equations:

    higher_level_encrypt(m, pubkey)  = lower_level_encrypt(m, pubkey),

    higher_level_decrypt(c, privkey) = lower_level_decrypt(c, privkey)

  rule RegisterPK:

      [ Fr(~sk) ]

    -->

      [ !PrivateKey($X, ~sk), !PublicKey($X, pk(~sk)), Out(pk(~sk))]

  rule C1:

      [

        !PublicKey($Server, pkey),

        Fr(~msg)

      ]

    -->

      [ Out(higher_level_encrypt(~msg, pkey)) ]

  rule S1:

      [

        !PrivateKey($Server, skey),

 // Using lower_level_encrypt instead of higher level solves the error (but not the main problem)

        In(higher_level_encrypt(msg, pk(skey)))

      ]

    -->

      [ Out(msg) ]

end

This gives the following error:

Multiplication restriction of rules:

 The following rule is not multiplication restricted:

   rule (modulo E) S1:

      [

      !PrivateKey( $Server, skey ),

      In( higher_level_encrypt(msg, pk(skey)) )

      ]

     -->

      [ Out( msg ) ]

  

 After replacing reducible function symbols in lhs with variables:

   rule (modulo E) S1:

      [ !PrivateKey( $Server, skey ), In( x.1 ) ]

     -->

      [ Out( msg ) ]

  

   Variables that occur only in rhs:  msg

CallStack (from HasCallStack):

 error, called at src/Theory/Tools/Wellformedness.hs:919:28 in tamarin-prover-theory-1.6.0-4xY8tGI4gcd2kXzIGyjzDc:Theory.Tools.Wellformedness

Why is the LHS rewritten that way? Is there a way to avoid having to actually use the lower_level_function? I've got a rather complex protocol to model, having higher level functions would prove very beneficial in terms of both readability and maintainability.

Thank you again for your kind help.

Regards, Alessandro Zanatta

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/MTR9U7y7eYo/unsubscribe.

To unsubscribe from this group and all its topics, send an email to tamarin-prove...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/c71edb0c-99c2-4112-b0bc-c757d829fdaen%40googlegroups.com.

[Cas Cremers]

Hi,

I think the problem is the `Out(msg)` in S2, which should be `Out(~msg)`. (`~msg` and `msg` are different variables; you typically want to use only one of them consistently in a rule)

Best,

Cas

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/91F61C72-13C2-4D16-AF17-B9FDEB0B6361%40getmailspring.com.