Formal Verification of Concurrent & Security Protocols

COSC437 (Security Protocols) work using model checkers to prove, or disprove, properties of protocols. In TLA+ and PlusCal I modelled Peterson's algorithm and Taubenfeld's Black-White Bakery mutual-exclusion algorithm for three concurrent processes, verifying mutual exclusion and liveness with the TLC model checker. A companion fault-injection model simulates a process crashing partway through the algorithm, and shows TLC detecting the resulting deadlock and liveness violations even while mutual exclusion still holds. It's a concrete demonstration of the difference between safety and liveness under failure. In ProVerif I modelled a symmetric-key mutual authentication protocol between two parties and a trusted server, under a Dolev-Yao attacker. All three properties failed, namely secrecy of the session key and agreement in each direction. Because the responder can't tell a nonce from a key, an attacker can reflect part of its own request back as the key ticket and get it to accept a session key the attacker knows. I then designed a modified protocol with tagged messages and a key confirmation step to close the attacks.