Specifying Systems: The TLA+ Language and Tools for Hardware ...
Leslie Lamport
Science of Concurrent Programs
Password Authentication with Insecure Communication