55AA Security Lab

55AA-016

Network Protocol Analysis and Verification

Level
Graduate
Status
Under development

Note: this course is still being designed and calibrated; the page content is for reference and does not represent the final teaching version.

Syllabus

Course Overview

Network Protocol Analysis and Verification combines protocol engineering, formal modeling, and security analysis. Topics include state machines, protocol reverse engineering, fuzzing, model checking, symbolic protocol analysis, and implementation conformance testing.

This is a graduate topic course after networking, applied cryptography, and program analysis.

Prerequisites

  • Computer networking and applied-cryptography fundamentals.
  • Understanding of state machines, logic, and basic program analysis.
  • Ability to write test harnesses or protocol scripts.

Learning Outcomes

  • Extract protocol state machines from specifications and traces.
  • Write protocol parsing, fuzzing, and conformance tools.
  • Verify key properties with model checking or symbolic tools.
  • Identify authentication, replay, downgrade, and state-confusion issues.
  • Translate verification results into engineering fixes.

Course Format

  • Two meetings per week: one for core concepts and one for labs, paper discussion, or project review.
  • The course proceeds over 16 weeks, each with a checkable assignment, lab, or project milestone.
  • Reproducibility is required: code, configuration, data, lab logs, and reports must be reviewable by staff or peers.

Weekly Plan

Week 1
Week 2

Protocol specs, state machines, and threat models: lab and review

Draw a state machine and security goals for a protocol. Complete the paired lab, record issues, and explain design tradeoffs in class review.

Session 3Protocol specs, state machines, and threat models: lab and review: Concepts, Cases, and Method90 minSession 4Protocol specs, state machines, and threat models: lab and review: Lab, Review, and Transfer90 min
Week 3
Week 4

Tracing, parsing, and protocol reverse engineering: lab and review

Implement a parser and annotate field semantics. Complete the paired lab, record issues, and explain design tradeoffs in class review.

Session 7Tracing, parsing, and protocol reverse engineering: lab and review: Concepts, Cases, and Method90 minSession 8Tracing, parsing, and protocol reverse engineering: lab and review: Lab, Review, and Transfer90 min
Week 5
Week 6

Protocol fuzzing: lab and review

Build a stateful fuzzing harness. Complete the paired lab, record issues, and explain design tradeoffs in class review.

Session 11Protocol fuzzing: lab and review: Concepts, Cases, and Method90 minSession 12Protocol fuzzing: lab and review: Lab, Review, and Transfer90 min
Week 7
Week 8

Model-checking fundamentals: lab and review

Model a handshake or retransmission behavior. Complete the paired lab, record issues, and explain design tradeoffs in class review.

Session 15Model-checking fundamentals: lab and review: Concepts, Cases, and Method90 minSession 16Model-checking fundamentals: lab and review: Lab, Review, and Transfer90 min
Week 9
Week 10

Authentication protocols and symbolic analysis: lab and review

Verify authentication, secrecy, or freshness properties. Complete the paired lab, record issues, and explain design tradeoffs in class review.

Session 19Authentication protocols and symbolic analysis: lab and review: Concepts, Cases, and Method90 minSession 20Authentication protocols and symbolic analysis: lab and review: Lab, Review, and Transfer90 min
Week 11
Week 12

Conformance and differential testing: lab and review

Compare boundary behavior of two implementations. Complete the paired lab, record issues, and explain design tradeoffs in class review.

Session 23Conformance and differential testing: lab and review: Concepts, Cases, and Method90 minSession 24Conformance and differential testing: lab and review: Lab, Review, and Transfer90 min
Week 13
Week 14

Downgrade, replay, and state confusion: lab and review

Reproduce or design a protocol-state flaw. Complete the paired lab, record issues, and explain design tradeoffs in class review.

Session 27Downgrade, replay, and state confusion: lab and review: Concepts, Cases, and Method90 minSession 28Downgrade, replay, and state confusion: lab and review: Lab, Review, and Transfer90 min
Week 15
Week 16

Protocol verification report: lab and review

Submit models, testing tools, and fix recommendations. Complete the paired lab, record issues, and explain design tradeoffs in class review.

Session 31Protocol verification report: lab and review: Concepts, Cases, and Method90 minSession 32Protocol verification report: lab and review: Lab, Review, and Transfer90 min

Assessment

Individual assignments

Concept questions, reading responses, design tasks, and small programming or lab exercises.

25%
Labs and project

Protocol models, testing tools, verification results, and fix recommendations.

40%
Participation and review

Participation in discussions, demos, code or paper reviews, and peer feedback.

10%
Final report and defense

Submit reproducible artifacts, a technical report, and a demo explaining methods, results, limitations, and future work.

25%

Course Project

Projects choose a real or teaching protocol and complete state-machine modeling, testing tools, property verification, and security evaluation.

Policies

  • AI tools are allowed, but generated code, lab notes, and design suggestions must be reviewed by the student and disclosed in the report.
  • Students may not submit code, proofs, configuration, or experimental results they cannot explain; each member must defend their own design, tests, and tradeoffs.
  • Late work affects iteration grades, but the course values reproducible, auditable, and maintainable results over last-minute accumulation.

Reference Courses

International

China 985 Universities