Mechanized network origin and path authenticity proofs

Fuyuan Zhang, Limin Jia, Cristina Basescu, Tiffany Hyun Jin Kim, Yih Chun Hu, Adrian Perrig

Research output: Chapter in Book/Report/Conference proceedingConference contribution


A secure routing infrastructure is vital for secure and reliable Internet services. Source authentication and path validation are two fundamental primitives for building a more secure and reliable Internet. Although several protocols have been proposed to implement these primitives, they have not been formally analyzed for their security guarantees. In this paper, we apply proof techniques for verifying cryptographic protocols (e.g., key exchange protocols) to analyzing network protocols. We encode LS2, a program logic for reasoning about programs that execute in an adversarial environment, in Coq. We also encode protocol-specific data structures, predicates, and axioms. To analyze a source-routing protocol that uses chained MACs to provide origin and path validation, we construct Coq proofs to show that the protocol satisfies its desired properties. To the best of our knowledge, we are the first to formalize origin and path authenticity properties, and mechanize proofs that chained MACs can provide the desired authenticity properties.

Original languageEnglish (US)
Title of host publicationProceedings of the ACM Conference on Computer and Communications Security
PublisherAssociation for Computing Machinery
Number of pages12
ISBN (Electronic)9781450329576, 9781450329576, 9781450331470, 9781450331500, 9781450331517, 9781450331524, 9781450331531, 9781450331548, 9781450331555, 9781450332392
StatePublished - Nov 3 2014
Event21st ACM Conference on Computer and Communications Security, CCS 2014 - Scottsdale, United States
Duration: Nov 3 2014Nov 7 2014

Publication series

NameProceedings of the ACM Conference on Computer and Communications Security
ISSN (Print)1543-7221


Other21st ACM Conference on Computer and Communications Security, CCS 2014
CountryUnited States


  • Formal methods
  • Mechanized proofs
  • Origin authenticity
  • Path authenticity
  • Secrecy

ASJC Scopus subject areas

  • Software
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'Mechanized network origin and path authenticity proofs'. Together they form a unique fingerprint.

Cite this