Needham-Schroeder Public-Key Protocol - Non-Termination

[Stefano Berlato]

Dear all,

I am Stefano Berlato, PhD student in Computer Science Security at the University of Genoa, Italy. I would like to use Tamarin in my current research; I read the Tamarin manual and tried to learn how to specify simple protocols in Tamarin. 

As an exercise, I tried to specify the (flawed) Needham-Schroeder Public-Key Protocol. Unfortunately, while the sanity check I wrote works, I am not able to find the MitM attack, the reason being (I assume) the non-termination of the proof due to some errors in my specification.

In detail, I uploaded the theory in Tamarin (interactive mode) and tried to autoprove (option "a") the lemma. While the sanity check solves almost immediately, after several hours of computation (on a fairly powerful computer), the other lemma was still unsolved.

I attach to this message the theory. Whenever you will be available, could you please check it and give me some feedback on the specification?

Waiting for a kind reply at your earliest convenience, I thank you for your attention and wish you a pleasant day!

Regards,

Stefano

[Ralf Sasse]

Dear Stefano,

Compare your own code to the one in the Tamarin repository which models Needham-Schroeder:

https://github.com/tamarin-prover/tamarin-prover/blob/develop/examples/classic/NSPK3.spthy

The version with Lowe's fix is also available:

https://github.com/tamarin-prover/tamarin-prover/blob/develop/examples/classic/NSLPK3.spthy

Particularly, note the use of a 'sources' lemma that is necessary to solve partial deconstructions (in both NS, and NSL). I guess your model has a similar issue and has "partial deconstructions" left:

https://tamarin-prover.github.io/manual/book/008_precomputation.html#sec:openchains

and in general this section of the manual could help you:

https://tamarin-prover.github.io/manual/book/008_precomputation.html

Best regards,
Ralf

--

Le informazioni contenute nella presente comunicazione sono di natura privata e come tali sono da considerarsi riservate ed indirizzate esclusivamente ai destinatari indicati e per le finalità strettamente legate al relativo contenuto. Se avete ricevuto questo messaggio per errore, vi preghiamo di eliminarlo e di inviare una comunicazione all’indirizzo e-mail del mittente.

--

The information transmitted is intended only for the person or entity to which it is addressed and may contain confidential and/or privileged material. If you received this in error, please contact the sender and delete the material.

--
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/b51dbd6a-0b5c-4189-9b51-32f90238291bn%40googlegroups.com.

[Cas Cremers]

p.s. you might also want to have a look at this work, that can auto-generate such lemmas in many cases:

https://hal.archives-ouvertes.fr/hal-02991286

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/fbf4b0b6-4f25-f44c-a225-9a158053c512%40inf.ethz.ch.

[Stefano Berlato]

Dear Ralf,
thank you for your kind answer and the link to your Needham-Schroeder model. 

However, my model does not have any ""partial deconstructions" left. Are there any
other reasons for non-termination?

Regards,
Stefano

[Ralf Sasse]

Dear Stefano,

Non-termination is always a possibility due to the undecidability. It can hinge on small modeling choices even, thus sometimes manual checking of the proof attempt can help you understand where it goes wrong. The auto-prover uses a heuristic, and it may find a loop by accident that it keeps repeating. There are ways around that using so-called oracles, see the manual.

I then also spent some time looking at your theory to give you more concrete feedback. Find attached a zip file with 3 spthy files, one marked .._orig which is your original file with inline comments where you made a mistake in the last rule, which leads to some of the issues. This is changed in the theory file named as you sent it. Using that file, I was able to manually find the standard Lowe attack, see the _stored_attack file. The auto-prover did not immediately find the attack though either! Keep in mind that the underlying problem is undecidable, so non-termination is not unexpected for different modeling choices.

The way you write the rules is interesting, however you may want to look at the way Tamarin understands them, which may or may not be what you intended. For this, you can click on "Multiset Rewriting Rules" in the left pane of the GUI tab. The listed rules do include some adversary rules you can safely ignore, but show the rest of the rules as Tamarin understood what you wrote. This is particularly visible for the last rule, in the version you sent vs the one I modified.

Also, you are making a (fairly strong) modeling assumption that the recipient of a value can detect whether it's fresh or not. That is, you match against aenc(<~nonceA,$A>)pk(~privkeyB) which implies that B can check that the value from A really is a nonce. You may want to not do that, and then the proof would become a bit harder again.

Best regards,
Ralf

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/f94dc2f7-c6ea-48ce-9775-b7e0bbcd88b7n%40googlegroups.com.

[Stefano Berlato]

Dear all,

I fixed the model, now it works fine. Thank you again for your time and courtesy!

I saw that there is a translator from A&B notation to Tamarin (https://infsec.ethz.ch/research/software/anb.html), is it still supported/maintained?

Best regards,

Stefano

[Ralf Sasse]

Dear Stefano,

Happy to hear that you managed to improve the model and got it running! Happy Proving! :-)

That A&B translator probably still works, but there is no one actively maintaining it. Also, it really only works for limited protocols (2 party) and primitives (some built-ins). However, for that subset, it should work fine.

Best regards,
Ralf

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/395c5893-6096-48d7-9479-9ede389ab162n%40googlegroups.com.

[Marco Calipari]

Hello everyone,

I was trying to reproduce the NSPK in Tamarn, and somehow I cannot write correctly the "executable" lemma.
I have two versions, one of them is my own, and the other one a copycat of Stefano's.

In both cases the lemma is not prooved, and I cannot wrap my head arround with this problem.

I am gonna put both codes in this post, if anyone could tell me what is wrong it would be awesome.
Thanks in advance for your time and patience, best.

[Ralf Sasse]

Dear Marco,

Please take a look at the NSPK version provided by the Tamarin distribution.

https://github.com/tamarin-prover/tamarin-prover/tree/develop/examples/classic

You can find both the broken NSPK3 and fixed NSLPK3 there.

For your particular files:

- the copycat version cannot work, because it uses a state fact on the left of a rule that does not ever get created:

1. in rule "Step_1_A_Sends_To_B": factName `A_State_1'

- for the other file, at least the rule "Step4_B_receives_last_msg_and_checks" is wrong because of the let binding you give: it  forces the received "message_2_A_recv" to be an encryption of a pair, while the second line of the let binding applies fst to it twice, which would really need a triple to make sense.

Thus, I am not surprised that neither of the examples will work.

Best regards,
Ralf

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/14819d05-7fe6-4fb2-b292-75be38c006dan%40googlegroups.com.

[Marco Calipari]

Hello ralf, thanks  alot for your answer.

I have checked the file in the repo, but still I cannot understand what might be wrong.
I made the modification you suggested, thanks a lot. but somehow it still does not work. I believe I followed all the necessary steps to generate a correct result. 
Maybe it's something small that I am not able to see and that do not allow the lemma to be proven.

Any other suggestion would be incredibly helpful.

I changed according to the hint, and also some namings to make more sense for the message sequence. 
The main difference that now tamarin says that it's plain wrong, without specifying what he used for generating the counterexample

Best regards, Marco

[felipecboeira]

Hi Marco,

as Ralf mentioned, you have a premise that is not ever created: A_State(..., 'INIT'). Therefore, the rule cannot be instantiated.

So even the following will not solve:

lemma exec2:
exists-trace
"Ex msg #i. A_Sends_To_B(msg)@i"

Regards,

Felipe

Em ter., 1 de ago. de 2023 às 15:42, Marco Calipari <marco.ca...@gmail.com> escreveu:

Hello group.

An update: I was able to recreate Stefano's code. 
However I am not sure about one thing: 

At the and of the day, without considering smaller distraction mistakes,  my problem was that  I was not recording the state of the system with 4 different facts, but I was trying to use the rewriting rules to keep track of the system.

Meaning that in Stefano's code we'll have the following facts:  Facts{ ... , Step1(...) , Step2(...) , Step3(...) , Step4(...), ...}
What I was trying to to was to have two different facts that will keep track of the parties states: State_A(...) and State_B(...). Given the fact that tamarin is based of a multiset of rewriting rules, my idea was to update state-by-state those two facts accordingly to what is the acquired knowledge of the parties.
You can find my file attached to this email, so that you can have a better understanding of what is going on.

Although in my head sounds right, Tamarin would not validate the "executibality" lemma. 


If you know where I am wrong it would be awesome to hear some hints. As a non CS guy I find myself probably stuck in trivial things that looks tremendous without former knowledge.

Thanks a lot for your time and help.

Cheers,

Marco

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/65d9cb50-9414-4de7-b0ae-089edade6499n%40googlegroups.com.

[Marco Calipari]

Hi, thanks for your answer.
However what do you mean that my premise is not created?

"  premise that is not ever created: A_State(..., 'INIT')  "

If I place it on the left of the rule should't be that ok? how could I fix that? with a rule?

thanks

[felipecboeira]

Hello,

the left side of the rule contains the premises required to instantiate that rule, so 'A_State' must first be created (i.e. be on the right side of a rule). Section 5 of the manual includes more details about this with a nice example: https://tamarin-prover.github.io/manual/master/book/005_protocol-specification-rules.html

Regards,

Felipe

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/0e6d974a-2f22-4201-ab1e-5f44eda77a96n%40googlegroups.com.

[Marco Calipari]

Hello,

I did that change, but I still It does not work.
I used the persistent facts to initiate the values and the pub/priv key associations.
So that in that way I created the fact before. But still I get the same error:

At this point I am completely lost

[Marco Calipari]

Errata corige, in the file the first istantiations are badly named.
But even with correction, still the lemma is not validating

[Marco Calipari]

Hello group,

I was able to let this code run, my mistake was that in "rule step_2_B_recv_from_A_and_sends_to_A:" I was not copying the original B_State but already writing an update. So yeah I was able to let the lemma verify.
Thanks for you support,

Cheers

[Marco Calipari]

Hello Again Group.

I was going through again this protocol and trying to write an Authentication lemma.
I thought that, since my version of the protocol is very similar to Stefano's, his authentication lemma should fail also in my code. However this is not the case, and I was wondering if any of you could help me to understand why.

Specifically there is also something else that does not make quite sense:
When i use the auto source option I obtain that the Authentication lemma can find a solution, otherwise it would time out and shut the server down. If you could give me any insights it would be awesome.

Thanks a lot for your time and patience:


Here you'll find the tamarin code:

/*

 *  Author: Marco Calipari

 *  Model Name: NSPK.spthy

 *  Status:

 *

 *  

 */

 theory Needam_Shroeder_public_key

 begin

 

 builtins: asymmetric-encryption

 

 /**

     We initialize rules that will be used to lookup where the private and

     public key are gonna be taken from

     When we istanciate that rule we will come here tp create it

 */

 

 rule Identity_Key_Registration:

     [

         Fr(~private_Key)

      ]

     -->

     [

         !Private_Key_Association($ID , ~private_Key),

         !Public_Key_Association($ID , pk(~private_Key))

         

     ]

 

 /** We need this rule to make sure that our protocol is secure. */

 

 

rule Reveal_Private_Key:

     [

         !Private_Key_Association($ID , private_Key)

      ]

     --[ Reveal($ID) ]->

     [

         Out(private_Key)

     ]

rule init:

    [

        !Public_Key_Association($A , publicKeyA),

        !Public_Key_Association($B , publicKeyB),

        !Private_Key_Association($A , ~privateKeyA),

        !Private_Key_Association($B , ~privateKeyB)

     

     ]

    --[ Init() ]->

    [ A_State($A , $B , 'NonceA' , <~privateKeyA , publicKeyB> , 'INIT')

    , B_State($A , $B , 'NonceA' ,'NonceB', <~privateKeyB , publicKeyA> , 'INIT')]

 /** A -> B {Na , A}_KpubB */

rule Step_1_A_Sends_To_B:

     let

 

         message_one = aenc{<'1', ~NonceA , $A> }publicKeyB

 

     in

 

     [

         

         

         Fr(~NonceA),

         /** We record the knowledge of the system with the states.

            In this way we keep track of the different changes

            We can do this on a general knowledge level or record the different parties.

            In this case we record the knowledge of the different parties */

         A_State($A, $B, 'NonceA', <~privateKeyA, publicKeyB> , 'INIT')

       

      ]

     --[

         

         A_Sends_To_B(message_one)

         ]-> //Should I consider the action of sending the full message encrypted ecc?

       

     [

        A_State($A, $B, ~NonceA, <~privateKeyA, publicKeyB> , 'NONCE_SENT') , // Should I add the identity of B?

        Out(message_one)]

 

 

rule step_2_B_recv_from_A_and_sends_to_A:

 let

        // I have to place 2 in here because in geenral is the 2nd message sent in the protocl

        message_one = aenc{<'1', NonceA, $A> }pk(~privateKeyB)

        received_nonce = fst(snd(adec{message_one}~privateKeyB))

        received_entity = snd(snd(adec{message_one}~privateKeyB))

        message_two = aenc{< '2',received_nonce  ,~NonceB > }publicKeyA

 in

 [   Fr(~NonceB),

     In(message_one),

     B_State($A, received_entity, 'NonceA', 'NonceB', <~privateKeyB, publicKeyA> , 'INIT')

 ]

 --[

     B_recv_from_A(message_one , received_nonce),

     B_sends(message_two)

     

 ]->

 [

    B_State($A, received_entity, NonceA, ~NonceB, <~privateKeyB, publicKeyA> , 'NONCE_SENT'),

     Out(message_two)

 ]

 

 rule step_3_A_recv_from_B_and_sends_to_B:

 let

     message_two = aenc{< '2', ~NonceA , NonceB> }pk(~privateKeyA)

     received_nonce_A = fst(snd(adec{message_two}~privateKeyA))

     received_nonce_B = snd(snd(adec{message_two}~privateKeyA))

     message_three = aenc{<'3', received_nonce_B>}publicKeyB

 in

 [

     A_State($A, $B, ~NonceA, <~privateKeyA, publicKeyB> , 'NONCE_SENT'),

     In(message_two)

 ]

 --[

     A_Receives_B(message_two),

     A_completed_protocol($A , $B , received_nonce_A , received_nonce_B)

 ]->

 [

     A_State($A, $B, ~NonceA, <~privateKeyA, publicKeyB> , 'DONE'),

     Out(message_three)

 ]

 

rule Step4_B_receives_last_msg_and_checks:

     let

         message_three_recv = aenc{<'3', ~NonceB >}pk(~privateKeyB)

         received_nonce_B_4 = snd(adec{message_three_recv}~privateKeyB)

     in

     [

        B_State($A, $B, NonceA, ~NonceB,< ~privateKeyB, publicKeyA> , 'NONCE_SENT'),

         In(message_three_recv)

      ]

     --[ B_completed_the_protocol($A , $B , NonceA , received_nonce_B_4)

        ]->

     [

        B_State($A, $B, NonceA, received_nonce_B_4,< ~privateKeyB, publicKeyA>, 'DONE')

      ]

 

 lemma executibality:

 exists-trace

 

 // there exist four variables (nonceA, nonceB, A, B)

 // at a given moment (#i) so that (.)

 " Ex nonceA nonceB A B #i.

 

     // there is in the trace a "BHasCompletedProtocol"

     // fact at moment "i" with the four variables

     B_completed_the_protocol(A, B, nonceA, nonceB) @ i

 

     // and there is in the trace a "AHasCompletedProtocol"

     // fact at moment "j" with the four variables and j<l

     & (Ex #j. A_completed_protocol(A, B, nonceA, nonceB) @ j & j<i)

 

     // and there does NOT exist a moment "r" so that the

     // fact "PrivateKeyWasRevealed" was added in the trace

     // at moment "r" with variable A

     & not(Ex #r. Reveal(A) @ r)

 

     // and there does NOT exist a moment "r" so that the

     // fact "PrivateKeyWasRevealed" was added in the trace

     // at moment "r" with variable B.

     & not(Ex #r. Reveal(B) @ r)

 "

 

 lemma Authentication:

" All nonceA nonceB A B #i.

    B_completed_the_protocol(A, B, nonceA, nonceB) @ i

    & not(Ex #r. Reveal(A) @ r)

    & not(Ex #r. Reveal(B) @ r)  

    ==>

    (Ex #j. A_completed_protocol(A, B, nonceA, nonceB) @ j & j<i)

"

end