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 language | English (US) |
|---|---|
| Title of host publication | Proceedings of the ACM Conference on Computer and Communications Security |
| Publisher | Association for Computing Machinery |
| Pages | 346-357 |
| Number of pages | 12 |
| ISBN (Electronic) | 9781450329576, 9781450329576, 9781450331470, 9781450331500, 9781450331517, 9781450331524, 9781450331531, 9781450331548, 9781450331555, 9781450332392 |
| DOIs | |
| State | Published - Nov 3 2014 |
| Event | 21st ACM Conference on Computer and Communications Security, CCS 2014 - Scottsdale, United States Duration: Nov 3 2014 → Nov 7 2014 |
Publication series
| Name | Proceedings of the ACM Conference on Computer and Communications Security |
|---|---|
| ISSN (Print) | 1543-7221 |
Other
| Other | 21st ACM Conference on Computer and Communications Security, CCS 2014 |
|---|---|
| Country | United States |
| City | Scottsdale |
| Period | 11/3/14 → 11/7/14 |
Fingerprint
Keywords
- Formal methods
- Mechanized proofs
- Origin authenticity
- Path authenticity
- Secrecy
ASJC Scopus subject areas
- Software
- Computer Networks and Communications
Cite this
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 proceeding › Conference contribution
}
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 -