2
$\begingroup$

I am starting Tamarin prover, and it is hard to understand.

Here is a basic example of my issue:

First Code :

theory test 
begin

builtins : asymmetric-crypto, diffie-hellman

rule Register_pk:
    [Fr(~ltkA)]-->[!Ltk($A, ~ltkA), !Pk($A, pk(~ltkA)), Out(pk(~ltkA))]

rule C1:
    [Fr(~x)]
    -->[C1($C, ~x), Out(<$C, 'g'^~x)>]

rule S1:
    let pubkeyC = 'g'^x in
    [Fr(~y), In(<C, pubkeyC)>]
    --[ Secret($S, C, pubkeyC^~y)]->
    [S1($S, ~y, pubkeyC)]

lemma Secret_dh:
"
    All S C dh_secret #i. Secret(S, C, dh_secret)@#i ==> not( Ex #k. K(dh_secret)@#k)
"
end

after a : tamarin-prover --prove test.spthy the lemma is verified

Then I only change the lemma into :

Second Code :

lemma Secret_dh:
exists-trace
"
    All S C dh_secret #i. Secret(S, C, dh_secret)@#i ==> Ex #k. K(dh_secret)@#k
"

And after a : tamarin-prover --prove test.spthy the lemma is verified too.

I find this completely abnormal.

$\endgroup$
1
1
$\begingroup$

Did you try asking this on the Tamarin google group? I'm guessing that's the right place to ask such a question and get a good answer.

Though from a first glance, I would guess that the empty trace (or any trace in which no Secret fact occurs) satisfies your second lemma, and this is thus entirely expected behavior.

Intuitively, your second lemma states: there exists a trace, such that (if a Secret fact occurs in it, then the adversary knows the secret). This trivially holds for any trace without a Secret fact, and thus the lemma indeed holds.

Or, put differently, your second lemma is not the negation of the first lemma.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.