{"id":4399,"date":"2014-09-09T06:00:20","date_gmt":"2014-09-09T04:00:20","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4399"},"modified":"2014-09-07T12:05:25","modified_gmt":"2014-09-07T10:05:25","slug":"resena-mechanized-network-origin-and-path-authenticity-proofs","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-mechanized-network-origin-and-path-authenticity-proofs\/","title":{"rendered":"Rese\u00f1a: Mechanized network origin and path authenticity proofs"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\">Coq<\/a> titulado <a href=\"http:\/\/www.netsec.ethz.ch\/research\/opt-verif.pdf\">Mechanized network origin and path authenticity proofs<\/a>.<\/p>\n<p>Sus autores son Fuyuan Zhang, <a href=\"http:\/\/www.andrew.cmu.edu\/user\/liminjia\">Limin Jia<\/a>, <a href=\"http:\/\/www.netsec.ethz.ch\/people\/basescuc\">Cristina Basescu<\/a>, <a href=\"http:\/\/users.ece.cmu.edu\/~hyunjin1\">Tiffany Hyun-Jin Kim<\/a>, <a href=\"http:\/\/users.crhc.illinois.edu\/yihchun\">Yih-Chun Hu<\/a> y <a href=\"http:\/\/www.netsec.ethz.ch\/people\/aperrig\">Adrian Perrig<\/a>.<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  <em>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 LS 2, 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.<\/em>\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 en el <a href=\"http:\/\/www.sigsac.org\/ccs\/CCS2014\/\">ACM CCS 2014<\/a> (<em>21st ACM Conference on Computer and Communications Security<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra <a href=\"http:\/\/www.ece.cmu.edu\/liminjia\/net-verif\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq titulado Mechanized network origin and path authenticity proofs. Sus autores son Fuyuan Zhang, Limin Jia, Cristina Basescu, Tiffany Hyun-Jin Kim, Yih-Chun Hu y Adrian Perrig. Su resumen es A secure routing infrastructure is vital for secure and reliable Internet services. Source authentication and path validation&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[45,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4399"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4399"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4399\/revisions"}],"predecessor-version":[{"id":4401,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4399\/revisions\/4401"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4399"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4399"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4399"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}