Consider the Promela spec of the buggy version of the Needham-Schroeder protocol seen as exercise. 

Adapt the Promela spec to represent the fixed version of the protocol and verify it with Spin. 

Document your fix with well identifiable comments written in the Promela spec, and send it to giovanni.denaro@unimib.it.