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

Abstract

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
Pages346-357
Number of pages12
ISBN (Electronic)9781450329576, 9781450329576, 9781450331470, 9781450331500, 9781450331517, 9781450331524, 9781450331531, 9781450331548, 9781450331555, 9781450332392
DOIs
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

Other

Other21st ACM Conference on Computer and Communications Security, CCS 2014
CountryUnited States
CityScottsdale
Period11/3/1411/7/14

Fingerprint

Network protocols
Internet
Routing protocols
Authentication
Data structures

Keywords

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

ASJC Scopus subject areas

  • Software
  • Computer Networks and Communications

Cite this

Zhang, F., Jia, L., Basescu, C., Kim, T. H. J., Hu, Y-C., & Perrig, A. (2014). Mechanized network origin and path authenticity proofs. In Proceedings of the ACM Conference on Computer and Communications Security (pp. 346-357). (Proceedings of the ACM Conference on Computer and Communications Security). Association for Computing Machinery. https://doi.org/10.1145/2660267.2660349

Mechanized network origin and path authenticity proofs. / Zhang, Fuyuan; Jia, Limin; Basescu, Cristina; Kim, Tiffany Hyun Jin; Hu, Yih-Chun; Perrig, Adrian.

Proceedings of the ACM Conference on Computer and Communications Security. Association for Computing Machinery, 2014. p. 346-357 (Proceedings of the ACM Conference on Computer and Communications Security).

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

Zhang, F, Jia, L, Basescu, C, Kim, THJ, Hu, Y-C & Perrig, A 2014, Mechanized network origin and path authenticity proofs. in Proceedings of the ACM Conference on Computer and Communications Security. Proceedings of the ACM Conference on Computer and Communications Security, Association for Computing Machinery, pp. 346-357, 21st ACM Conference on Computer and Communications Security, CCS 2014, Scottsdale, United States, 11/3/14. https://doi.org/10.1145/2660267.2660349
Zhang F, Jia L, Basescu C, Kim THJ, Hu Y-C, Perrig A. Mechanized network origin and path authenticity proofs. In Proceedings of the ACM Conference on Computer and Communications Security. Association for Computing Machinery. 2014. p. 346-357. (Proceedings of the ACM Conference on Computer and Communications Security). https://doi.org/10.1145/2660267.2660349
Zhang, Fuyuan ; Jia, Limin ; Basescu, Cristina ; Kim, Tiffany Hyun Jin ; Hu, Yih-Chun ; Perrig, Adrian. / Mechanized network origin and path authenticity proofs. Proceedings of the ACM Conference on Computer and Communications Security. Association for Computing Machinery, 2014. pp. 346-357 (Proceedings of the ACM Conference on Computer and Communications Security).
@inproceedings{1d7a7c15bda4482a8059cac4bb5e2917,
title = "Mechanized network origin and path authenticity proofs",
abstract = "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.",
keywords = "Formal methods, Mechanized proofs, Origin authenticity, Path authenticity, Secrecy",
author = "Fuyuan Zhang and Limin Jia and Cristina Basescu and Kim, {Tiffany Hyun Jin} and Yih-Chun Hu and Adrian Perrig",
year = "2014",
month = "11",
day = "3",
doi = "10.1145/2660267.2660349",
language = "English (US)",
series = "Proceedings of the ACM Conference on Computer and Communications Security",
publisher = "Association for Computing Machinery",
pages = "346--357",
booktitle = "Proceedings of the ACM Conference on Computer and Communications Security",

}

TY - GEN

T1 - Mechanized network origin and path authenticity proofs

AU - Zhang, Fuyuan

AU - Jia, Limin

AU - Basescu, Cristina

AU - Kim, Tiffany Hyun Jin

AU - Hu, Yih-Chun

AU - Perrig, Adrian

PY - 2014/11/3

Y1 - 2014/11/3

N2 - 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.

AB - 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.

KW - Formal methods

KW - Mechanized proofs

KW - Origin authenticity

KW - Path authenticity

KW - Secrecy

UR - http://www.scopus.com/inward/record.url?scp=84910684556&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84910684556&partnerID=8YFLogxK

U2 - 10.1145/2660267.2660349

DO - 10.1145/2660267.2660349

M3 - Conference contribution

AN - SCOPUS:84910684556

T3 - Proceedings of the ACM Conference on Computer and Communications Security

SP - 346

EP - 357

BT - Proceedings of the ACM Conference on Computer and Communications Security

PB - Association for Computing Machinery

ER -