loop breaker for executable lemma because of equality restriction

[zidni hakam]

Hello all,

I didn't get a solved trace in my protocol model and got a loop breaker because of equality restriction I used. If I don't use the equality restriction they got solved in the executable lemma but got the red colored line in other lemma.

I assume that is because the equality restriction that I use can't be fulfilled by the tamarin-prover. I use equality restriction for the protocol bilinear pairing authentication.

Is it okay if i just ignore the executable lemma that didn't give me solved trace? Does the other verification is valid or not if I ignore that condition?

Best Regard,
Zidni

[Ralf Sasse]

If you do not get a 'proper' execution using an executability lemma, as you describe, there is a high chance that your protocol model contains an error, and is not actually executable. The problem with this is that the "empty" protocol (that cannot do anything) trivially fulfills all secrecy lemmas, so there is a high chance that your "verification" result cannot be trusted.

Cheers,
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/238af9db-3d04-42ec-93d9-ce6bc0d71a0bn%40googlegroups.com.

[zidni hakam]

Dear Ralf,

According to the trace that tamarin gives, the protocol model that use matching restriction is the one with the right trace than the one that didn't use it. That is why until now I still try to figure out why the tamarin didn't give the green line and word "solved", my assumption according to some try I already do is because the tamarin doesn't get the equal value of the message so it cause a looping. Here is the screenshot, trace and some code that show my modeling problem. 

left side is the modeling that use restriction and the right side is didn't use it.

Trace from protocol model that didn't use restriction.

Trace from protocol model that use restriction.

This is the some code that need equality restriction in my modeling protocol.

rule A_Init:

let

PA = pmult(~rA,'g')

IdA = Identity($A)

T1 = ~Timestamp

RA = H(IdA, PbA, PA, T1)

SA = sign(RA, PrA)

term = em('g', SA)

in

[ Fr(~rA), Fr(~Timestamp), !Pr($A, PrA), !Pb($A, PbA) ]

--[ Running($A,$B,term), Create($A, IdA) ]->

[ !State($A, IdA, PA, ~rA, T1), Out(<$A, $B, <IdA, PbA, PA, SA, T1>>) ]



rule B_Recv:

let

IdB = Identity($B)

m = H1(PbA, IdA)

RA = H(IdA,PbA,PA,T1)

temp1 = padd(PbJ, pmult(m, PbA))

term = em('g', SA)

leftside = em(temp1, RA)

PB = pmult(~rB,'g')

SKBA = h(pmult(~rB,em(RA, PA)))

SB = sign(PA, PrB)

hb = h(IdB, PbB, PB, SKBA, T1, SB)

in

[ Fr(~rB), !PbNet($NM, PbJ), !Pb($B, PbB), !Pr($B, PrB), In(<$A, $B, <IdA, PbA, PA, SA, T1>>) ]

--[ Eq(leftside, term), !SharedKey($B, $A, SKBA), Honest($B), Honest($A), /*Secret(SKBA),*/ Commit($A,$B,term), Running($A,$B,hb), Create($B,IdB)/*, Finish()*/ ]-> [ !Point($B, IdB, PB, ~rB), Out(<$B, $A, <IdB, PbB, PB, hb>>) ]

Best Regard,
Zidni

[Ralf Sasse]

Dear Zidni,

In your try, it seems Tamarin has exhausted the whole possible search space and is convinced that there is no execution on the left, so it is not an infinite loop or non-determination, but the restriction you use limits the protocol so that it cannot be executed anymore, meaning something is wrong.

Unfortunately, I don't have the time to debug a partial model of a protocol that I don't know. Good luck!

Cheers,
Ralf

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/f1ffa17b-d687-465f-9f54-35adcdd9f520n%40googlegroups.com.

[zidni hakam]

Dear Ralf,

Another question, what about the red line on lemma that didn't show any counter example or possible attack in the trace given when the executable lemma is solved? Is that also something wrong in my modeling protocol?

Best regards,

Zidni