2012 20th IEEE International Conference on Network Protocols (ICNP) (2012)
Austin, TX, USA USA
Oct. 30, 2012 to Nov. 2, 2012
Chen Chen , University of Pennsylvania, Philadelphia, 19104, USA
Limin Jia , Carnegie Mellon University, Pittsburgh, PA 15213, USA
Boon Thau Loo , University of Pennsylvania, Philadelphia, 19104, USA
Wenchao Zhou , Georgetown University, Washington, DC 20057, USA
In recent years, there have been strong interests in the networking community in designing new Internet architectures that provide strong security guarantees. However, none of these proposals back their security claims by formal analysis. In this paper, we use a reduction-based approach to prove the route authenticity property in secure routing protocols. These properties require routes announced by honest nodes in the network not to be tampered with by the adversary. We focus on protocols that rely on layered signatures to provide security: each route announcement is associated with a list of signatures attesting the authenticity of its subpaths. Our approach combines manual proofs with automated analysis. We define several reduction steps to reduce proving route authenticity properties to simple conditions that can be automatically checked by the Proverif tool. We show that our analysis is correct with respect to the trace semantics of the routing protocols.
Routing protocols, Security, Routing, Topology, Internet, Semantics
C. Chen, L. Jia, B. T. Loo and W. Zhou, "Reduction-based security analysis of Internet routing protocols," 2012 20th IEEE International Conference on Network Protocols (ICNP 2012)(ICNP), Austin, TX, 2012, pp. 1-6.