Applications of Formal Methods for
Security of Network Protocols and Distributed Systems
(CS 7670)

This site is maintained for public access, if you are enrolled in the class see the Canvas webpage for detailed information.

Class Information
Course Description

Network protocols and distributed systems are at the core of all computing systems we rely on today. Thus, it is important that we have assurance about their design and implementation, i.e. their designs and implementations are free of bugs and vulnerabilities. For secure protocols, their goals must also be achieved in the presence of adversaries that must be clearly specified. Formal methods can help disambiguate system specifications and can expose flaws in system requirements, often not captured through testing. In this class we will study how formal methods have been applied to gain assurance about network protocols and distributed systems design and implementation. We will focus both on the benefits and limitations of formal methods based approaches.

The objectives of the course are the following:

  • Provide an overview of the main methods of getting assurance about protocol implementations, including secure network protocols and showing how formal methods fit in this context.
  • Provide an overview of current state of the art formal methods capabilities when applied to network protocols and distributed systems. This will include an overview of existing available tools, highlighting their strengths and weaknesses.
  • Read recent, state-of-the-art research papers from both systems and security conferences focused on applications of formal methods to network protocols and distributed systems and discuss them in class. Students will actively participate in class discussions, and lead discussions on multiple papers during the semester.
  • Experiment with applying formal methods to network protocols and distributed systems through several programming exercises and a semester-long research project. Students can select the topic of the research project.


The grade will be based on paper review submission (PR), participation in paper discussions in class (PD), presentations of papers in class and discussion lead (PL), one programming assignment (PA) and research project (RP). Paper reviews are due by 9pm the day before the lecture when the paper is discussed.Submission is through Gradescope. Grade is computed as follows:

Grade = 15%*PR + 15%*PD + 10%*PL + 20%*PA + 40%*RP.
Academic Integrity

Academic Honesty and Ethical behavior are required in this course, as it is in all courses at Northeastern University. There is zero tolerance to cheating.

You are encouraged to talk with the professor about any questions you have about what is permitted on any particular assignment.




A tentative schedule is posted below for public access. Class platform is Canvas available through mynortheastern. All additional material for the class and all class communication will take place on Canvas. For the most updated information check Canvas.

Week Topics Projects
Week 1 Class overview.
Security for distributed systems and network protocols.
Week 2 Overview of formal methods for security
  • A Survey of Practical Formal Methods for Security. Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter Wurtz Vinther Tran-Jorgensen, Jim Woodcock. 2021 [PDF]
  • SoK: Computer-Aided Cryptography. Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno. IEEE S&P 2021. [PDF]
Template for reviews out.
Week 3 Distributed systems: Key-value store
  • Using Lightweight Modeling To Understand Chord. Pamela Zave. ACM SIGCOMM CCR 2012. [PDF]
  • Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3. James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, and Andrew Warfield. SOSP 2021 [PDF]
Programming assignment out.
Week 4 Distributed systems: Paxos and Raft
  • IronFleet: Proving Practical Distributed Systems Correct Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, Brian Zill. SOSP 2015. [PDF]
  • Verdi: a framework for implementing and formally verifying distributed systems. James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. PLDI 2015
    Additional papers: [PDF]
  • Formal Verification of Multi-Paxos for Distributed Consensus Saksham Chand, Yanhong A. Liu, Scott D. Stoller [PDF]
  • An Empirical Study on the Correctness of Formally Verified Distributed Systems Pedro Fonseca Kaiyuan Zhang Xi Wang Arvind Krishnamurthy. Eurosys 2017. [PDF]
Week 5 Distributed systems: Byzantine-resilience
  • A Formally Verified Protocol for Log Replication with Byzantine Fault Tolerance. Joel Wanner, Laurent Chuat, and Adrian Perrig. SRDS 2020. [PDF]
  • Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda. Harold Carr, Christopher Jenkins, Mark Moir, Victor Cacciari Miraldo, Lisandra Silva. 2022 [PDF]
  • Formal Model-Driven Analysis of Resilience of GossipSub to Attacks from Misbehaving Peers. Ankit Kumar, Max von Hippel, Pete Manolios, Cristina Nita-Rotaru. IEEE S&P 2024. [PDF]
    Additional papers:
  • Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. Vincent Rahli , Ivana Vukotic, Marcus Völp, Paulo Esteves-Verissimo. ESOP 2018. [PDF]
  • Prime: Byzantine Replication under Attack. Yair Amir, Brian Coan, Jonathan Kirsch, and John Lane. TDSC 2010. [PDF]
  • The Honey Badger of BFT Protocols. Authors: Andrew Miller, Yu Xia, Kyle Croman, Elaine Shi, and Dawn Song. ACM CCS 2016 [PDF]
Week 6 Distributed systems: Performance
  • Finding Latent Performance Bugs in Systems Implementations. Charles Killian, Karthik Nagaraj, Ryan Braud ,James W. Anderson, Salman Pervez, and Ranjit Jhala. FSE 2010. [PDF]
  • Performal: Formal Verification of Latency Properties for Distributed Systems. Tony Nuda Zhang, Upamanyu Sharma, and Manos Kapritsos. PLDI 2023 [PDF]
  • Formal Methods for Network Performance Analysis Mina Tahmasbi Arashloo, Ryan Beckett, Rachit Agarwal. NSDI 2023 [PDF]
Programming assignment due.
Week 7 Network protocols: TLS
  • Implementing TLS with Verified Cryptographic Security. Karthikeyan Bhargavan, Cedric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. IEEE S&P 2013. [PDF]
  • A Comprehensive Symbolic Analysis of TLS 1.3. Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, Thyla van der Merwe. ACM CCS 2017 [PDF]
  • Implementing and Proving the TLS 1.3 Record Layer. IEEE S&P 2017. Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Jean Karim Zinzindohoué [PDF]
Research project proposal due
Week 8
Network Protocols: QUIC
  • Formal specification and testing of QUIC Ken McMillan and Lenore Zuck. SIGCOMM 2019 [PDF]
  • A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. Antoine Delignat-Lavaud, Cedric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou. IEEE S&P 2021. [PDF]
    Additional papers:
  • How Secure and Quick is QUIC? Provable Security and Performance Analyses. R. Lychev, S. Jero, A. Boldyreva, and C. Nita-Rotaru. IEEE S&P 2015. [PDF]
Finalize research project proposals.
Week 10
Network protocols: Payment systems
  • The EMV Standard: Break, Fix, Verify David Basin, Ralf Sasse, Jorge Toro-Pozo. IEEE SP 2021 [PDF]
  • Card Brand Mixup Attack: Bypassing the PIN in non-Visa Cards by Using Them for Visa Transactions. David A. Basin, Ralf Sasse, and Jorge Toro-Pozo. 2021. USENIX Security 2021. [PDF]
Week 11 Network protocols: Signal, Multi-factor Authentication
  • Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet. IEEE EuroS&P 2017. [PDF]
  • A Formal Security Analysis of the Signal Messaging Protocol Extended Version, July 2019. Katriel Cohn-Gordon, Cas Cremers, Benjamin Dowling, Luke Garratt, Douglas Stebila. [PDF]
  • An Extensive Formal Analysis of Multi-factor Authentication Protocols. Charlie Jacomme, Steve Kremer. ACM TOPS 2021. [PDF]
Week 12 Network protocols: 5G and 802.11 WPA2.
  • A Formal Analysis of 5G Authentication. David Basin, Jannik Dreier, Lucca Hirschi, Sasa Radomirović, Ralf Sasse, Vincent Stettler. CCS 2018. [PDF]
  • A Formal Analysis of IEEE 802.11's WPA2. Cas Cremers, Benjamin Kiesl, Niklas Medinger. Usenix Security 2020. [PDF]
Week 13 Network protocols: TCP
  • Formal specification and verification of safety and performance of TCP selective acknowledgment. M.A. Smith and K.K. Ramakrishnan, IEEE/ACM TON 2012. [PDF]
  • Toward formally verifying congestion control behavior. Venkat Arun, Mina Tahmasbi Arashloo, Ahmed Saeed, Mohammad Alizadeh, Hari Balakrishnan. SIGCOM 2021. [PDF]
Week 14 Project presentations in class Project presentations due April 10
Week 15 Finalize research project report.
Code and report due April 19

Additional Reading List

Copyright© 2023 Cristina Nita-Rotaru. Send your comments and questions to Cristina Nita-Rotaru