'''(70 points)''' Complete [http://www.cse.chalmers.se/edu/course/TDA294/Lab1.html Part 2] of Lab 1 from the [http://www.cse.chalmers.se/edu/course/TDA294/ Sofware Engineering Formal Methods Course] at Chalmers University of Technology. 

[http://www.cse.chalmers.se/edu/course/TDA294/Lab1.html Part 2] is to model [https://en.wikipedia.org/wiki/Needham%E2%80%93Schroeder_protocol Needham-Schroeder protocol], and then augment that model with an attacker, patch the protocol, and verify the patched protocol correct.