Tamarin-prover issue on a basic Diffie-Hellman Exchange I am starting Tamarin-Prover and I have a little issue of understanding.
Here is a basic exemple of my issue :
First Code :
theory test 
begin

builtins : asymmetric-crypto, diffie-hellman

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

rule C1:
    [Fr(~x)]
    --&gt;[C1($C, ~x), Out(&lt;$C, 'g'^~x)&gt;]

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

lemma Secret_dh:
&quot;
    All S C dh_secret #i. Secret(S, C, dh_secret)@#i ==&gt; not( Ex #k. K(dh_secret)@#k)
&quot;
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
&quot;
    All S C dh_secret #i. Secret(S, C, dh_secret)@#i ==&gt; Ex #k. K(dh_secret)@#k
&quot;

And after a : tamarin-prover --prove test.spthy the lemma is verified too. And I find this completly abnormal ..
Thanks for your help .. And have a good day.
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.