3 citations · 4 across the 9 of their papers we have counts for
10 papers
RFCLLM: Evaluating LLMs' Reasoning Ability of Network Protocol State Machines
Anqi Chen, Dan Goldwasser, Cristina Nita-Rotaru
Mapping textual specifications into formal representations is essential for ensuring the correctness of protocol designs and implementations. LLM-generated mappings, used for netwo…
Quantum-Resistant Networks: A Review of Primitives, Protocols and Best Practices
Elisa Bertino, Ramana Kompella, Ashish Kundu +3
Large-scale quantum computers threaten the public-key cryptographic foundations underpinning today's network security infrastructures. While significant progress has been made in s…
Automated Channel Fault Analysis with Tofu
Jacob Ginesin, Max von Hippel, Cristina Nita-Rotaru
Distributed protocols are the linchpin of the modern internet, underpinning every internet service. This has in turn motivated a massive body of research ensuring the security, rel…
Cross-Service Token: Finding Attacks in 5G Core Networks
Anqi Chen, Riccardo Preatoni, Alessandro Brighente +2
5G marks a major departure from previous cellular architectures, by transitioning from a monolithic design of the core network to a Service-Based Architecture (SBA) where services…
The Matrix Reloaded: A Mechanized Formal Analysis of the Matrix Cryptographic Suite
Jacob Ginesin, Cristina Nita-Rotaru
Secure instant group messaging applications such as WhatsApp, Facebook Messenger, Matrix, and the Signal Application have become ubiquitous in today's internet, cumulatively servin…
Payout Races and Congested Channels: A Formal Analysis of Security in the Lightning Network
Ben Weintraub, Satwik Prabhu Kumble, Cristina Nita-Rotaru +1
The Lightning Network, a payment channel network with a market cap of over 192M USD, is designed to resolve Bitcoin's scalability issues through fast off-chain transactions. There…
Rolling in the Shadows: Analyzing the Extraction of MEV Across Layer-2 Rollups
Christof Ferreira Torres, Albin Mamuti, Ben Weintraub +2
The emergence of decentralized finance has transformed asset trading on the blockchain, making traditional financial instruments more accessible while also introducing a series of…
A Formal Analysis of SCTP: Attack Synthesis and Patch Verification
Jacob Ginesin, Max von Hippel, Evan Defloor +2
SCTP is a transport protocol offering features such as multi-homing, multi-streaming, and message-oriented delivery. Its two main implementations were subjected to conformance test…
Verification of GossipSub in ACL2s
Ankit Kumar, Max von Hippel, Panagiotis Manolios +1
GossipSub is a popular new peer-to-peer network protocol designed to disseminate messages quickly and efficiently by allowing peers to forward the full content of messages only to…
A Case Study in Analytic Protocol Analysis in ACL2
Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan +2
When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of math…