{"ID":2846438,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2511.01124","arxiv_id":"2511.01124","title":"Verification and Attack Synthesis for Network Protocols","abstract":"Network protocols are programs with inputs and outputs that follow predefined communication patterns to synchronize and exchange information. There are many protocols and each serves a different purpose, e.g., routing, transport, secure communication, etc. The functional and performance requirements for a protocol can be expressed using a formal specification, such as, a set of logical predicates over its traces. A protocol could be prevented from achieving its requirements due to a bug in its design or implementation, a component failure (e.g., a crash), or an attack. This dissertation shows that formal methods can feasibly characterize the functionality and performance of network protocols under normal conditions as well as when subjected to attacks.","short_abstract":"Network protocols are programs with inputs and outputs that follow predefined communication patterns to synchronize and exchange information. There are many protocols and each serves a different purpose, e.g., routing, transport, secure communication, etc. The functional and performance requirements for a protocol can...","url_abs":"https://arxiv.org/abs/2511.01124","url_pdf":"https://arxiv.org/pdf/2511.01124v1","authors":"[\"Max von Hippel\"]","published":"2025-11-03T00:26:12Z","proceeding":"cs.CR","tasks":"[\"cs.CR\",\"cs.FL\"]","methods":"[]","has_code":false}