I'm working on a paper about model checking on cryptographic protocols and many of the papers I have read, base their approaches in the Needham-Schroeder protocol. I undestand this was one of the earliest security protocols for authentication and that Lowe's findings makes it an interesting protocol to talk about, I get that it is also one of the easiest protocols to explain and that's why it is used on textbooks, I have also read about how it led to the creation of some modern protocols like SSL. However it felts somewhat strange for me that even modern research keeps on using it for their work instead of the fixed version or some other similar protocols.
Does this protocol has a set of features that makes it kinda "perfect" for research about verification or something like that, what am I missing?