Signature verification using pattern matching (without public key)

[Daniel Andrade]

Hello.

In the following minimal working example we (i) generate a nonce and (ii) sign it with `~ltk` in the first rule; and then (iii) verify the nonce in the second rule using pattern matching.

I expected the exist-trace lemma to succeed when the public key is available in rule Receive and to fail when the public key input is commented (as is the case in the code below). Yet the proof still succeeds in the second case. I thought we needed the public key because of sign(~nonce, ~ltk) in rule Received.

1. Shouldn't lemma functional fail to find a trace since the public key is not available in rule Received?
2. In the first figure below, which is of a trace where the public key is available in rule Received, we have two rules Register_pk. In this case should we assume the ~ltk in the first Register_pk equals ~ltk.1 in the second Register_pk?
   

(I was trying to verify the signature using pattern matching instead of using Eq(true, verify(sign(~nonce, ~ltk), ~nonce, pub)).)

theory SignatureVerification

begin

builtins: signing

rule Register_pk:
    [ Fr(~ltk) ] --> [ !Ltk($id, ~ltk), !Pk($id, pk(~ltk)) ]

rule Send:
    let
        signature = <~nonce, sign(~nonce, ~ltk)>
    in
    [ !Ltk($A, ~ltk), Fr(~nonce) ]
    --[ Sent(~nonce) ]->
    [ Out(signature) ]

rule Receive:
    let
        signature = <~nonce, sign(~nonce, ~ltk)>
    in
    [ In(signature)
    // , !Pk($A, pub)  // comment this: Receive will not have the public key
    ]
    --[ Received(~nonce) ]->
    []

lemma functional: exists-trace
    "Ex nonce #i #j. Sent(nonce) @ i & Received(nonce) @ j"

end

With public key:

Without public key:

[Ralf Sasse]

Dear Daniel

Your rule does not do what you want it to do: the public key that you list is just an unrelated one.

rule Receive:
    let
        signature = <~nonce, sign(~nonce, ~ltk)>
    in
    [ In(signature)
    // , !Pk($A, pub)  // comment this: Receive will not have the public key
    ]
    --[ Received(~nonce) ]->
    []

the "pub" in the !Pk fact is just unrelated. It has to be "pk(~ltk)" to actually model a signature check. So you would rewrite your rule as such:

rule Receive:
    let
        signature = <~nonce, sign(~nonce, ~ltk)>
    in
    [ In(signature)

     , !Pk($A, pk(~ltk))  // comment this: Receive will not have the public key
    ]
    --[ Received(~nonce) ]->
    []

for the version that checks the signature.

In the other version, with that !Pk commented out, you want to model that the signature verification key is not available from what you write, however what you have modeled is that simply any input is accepted and no check whatsoever is done, so this will always succeed.There is no easy way to model this idea of the key not being there without going much deeper into 'restrictions' that disallow this.

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/d28b7f30-2186-4efa-b56f-664ab2a0f3d8n%40googlegroups.com.

[Daniel Andrade]

Thank you for the explanation, Ralf.

I was confused regarding the behavior of pattern matching when the public key is not present. I thought the rule would simply fail but it seems that any input is accepted in such cases as you explained.

In a model I'm working on I forgot to add the public key in a rule, but Tamarin was still executing the proof without failing, hence the question.

For the version that checks the signature I actually fixed it correctly on the model I'm working on, but botched the minimal example for the forums. (The figure wasn't looked okay to me, that's why I asked.)

Kind regards,

Daniel