Specifying an equational theory

[Daniel S]

Dear All,

I'm quite early in my Tamarin journey, so apologies if this is a rookie question. I'm trying to understand equational theories in the following example. Suppose I want to model a community where each user has a pre-shared list of keys for each of given list of contacts and that contact pairs have matching keys. I choose to model key lookup with a function keypool(user,contact,index) where the first two arguments commute. Thus a simple protocol using this might be

theory keypool

begin

functions: keypool/3 [private]

equations: keypool(a,b,c) = keypool(b,a,c)

rule SelectIndex:

    [ Fr(~index) 

    ]

  --[ InitKey($Init,$Resp,keypool($Init,$Resp,~index))

    ]->

    [ Out(<$Init,$Resp,~index>)

    ]

rule RecoverKey:

    [ In(<$Init,$Resp,index>)

    ]

  --[ RespKey($Resp,$Init,keypool($Resp,$Init,index))

    ]->

    [ Done()

    ]

lemma KeySetup:

    exists-trace

    "Ex I R k #i #j.

        InitKey(I,R,k) @ i

     &  RespKey(R,I,k) @ j

    "

lemma Secrecy:

    "not (

         Ex I R k #i #j.

            InitKey(I,R,k) @i

         & K(k) @j     

     )

     "

end

Unfortunately, this seems to cause non-termination of the tamarin-prover (it hangs after reporting the installation check). I see that the manual does warn that there are challenges to theories that are not subterm convergent (as is the case here). On the other hand, this does seem to be a simple example of commutativity which is handled in XOR, multiset, and diffie-hellman. Indeed, rewriting things to use multisets does pass smoothly through:

theory keypool

begin

builtins: multiset

functions: keypool/2 [private]

rule SelectIndex:

    [ Fr(~index) 

    ]

  --[ InitKey($Init,$Resp,keypool($Init + $Resp,~index))

    ]->

    [ Out(<$Init,$Resp,~index>)

    ]

rule RecoverKey:

    [ In(<$Init,$Resp,index>)

    ]

  --[ RespKey($Resp,$Init,keypool($Resp + $Init,index))

    ]->

    [ Done()

    ]

lemma KeySetup:

    exists-trace

    "Ex I R k #i #j.

        InitKey(I,R,k) @ i

     &  RespKey(R,I,k) @ j

    "

lemma Secrecy:

    "not (

         Ex I R k #i #j.

            InitKey(I,R,k) @i

         & K(k) @j     

     )

     "

   

end

However, I'd like to use the original formulation for greater transparency to the proof consumer. What am I missing?

With thanks in advance,

Daniel

[Ralf Sasse]

Dear Daniel,

There is a difference between built-in theories (like XOR, DH, BP, multiset) and user-definable theories. User-definable theories must have the Finite Variant Property (FVP), which the user has to ensure, otherwise non-termination results most likely. This is not easy to check, so Tamarin does not even attempt to do so. The case of subterm-convergent equational theories is extra nice, as these theories are guaranteed to have FVP.

To explain a bit of background here, equational theories actually have two parts (and this nomenclature comes from term-rewriting, specifically Maude notions): the "actual equations" which must be terminating [thus no commutativity for example], and a set of "axioms" modulo which the equations are interpreted, where the axioms can include associativity, commutativity, etc.

There is no way for you as a Tamarin user to specify your user-defined equational theory modulo these, as the likelihood of mistakes and resulting false results from Tamarin is too high. You can fork Tamarin and go into the source code to implement your equational theory similar to the multiset one, but soundness would not be guaranteed by us, but need your own proof.

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/86ed4b5d-9d30-40be-8f7f-ead798fee365n%40googlegroups.com.