{"id":141,"date":"2010-01-24T11:18:26","date_gmt":"2010-01-24T11:18:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=141"},"modified":"2013-03-08T05:53:47","modified_gmt":"2013-03-08T05:53:47","slug":"metodos-formales-y-seguridad-en-la-red","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/metodos-formales-y-seguridad-en-la-red\/","title":{"rendered":"M\u00e9todos formales y seguridad en la Red"},"content":{"rendered":"

Hoy publica “El Pa\u00eds” el art\u00edculo Espa\u00f1a, blanco de m\u00e1s de cuarenta ciberataques<\/a>. El art\u00edculo es un reportaje sobre “la guerra de los ciberesp\u00edas” a ra\u00edz del ataque a Google<\/a>. Adem\u00e1s cuenta las iniciativas espa\u00f1olas para aumentar la seguridad.<\/p>\n

Desde sus inicios los m\u00e9todos formales<\/a> se han aplicado a aumentar la seguridad de los sistemas cr\u00edticos<\/a> y, m\u00e1s generalmente, a la ingenier\u00eda de la seguridad<\/a>. Dado el uso de la Red, sus programas y servicios se est\u00e1n convirtiendo en sistemas cr\u00edticos y, por tanto, en campo de aplicaci\u00f3n de los m\u00e9todos formales. Muestra del inter\u00e9s de los sistemas de Red para los m\u00e9todos formales son la realizaci\u00f3n de tesis como las siguientes
\n<\/p>\n

    \n
  1. Axiomatic Semantics Verification of a Secure Web Server<\/a> (P.E. Black, 1998)\n
  2. The Analysis of Cryptographic APIs Using The Theorem Prover Otter<\/a> (P. Youn, 2004).\n
  3. Automated Analysis of Security APIs<\/a> (A.H. Lin, 2005).\n
  4. Using a PVS Embedding of CSP to Verify Authentication Protocols<\/a> (B. Dutertre y S. Schneider, 1997).\n
  5. Proving Properties of Security Protocols by Induction<\/a> (L.C. Paulson, 1997).\n
  6. AnZenMail: A secure and certified e-mail system<\/a> (E. Shibayama y als. 2002).\n
  7. Formalization and Verification of a Mail Server in Coq<\/a> (R. Affeldt y N. Kobayashi, 2003).\n
  8. Robbing the bank with a theorem prover<\/a> (C.P. Youn y als. 2005).\n
  9. A Tool for Managing Security Policies in Organisations<\/a> (A.V. \u00c1lvarez, R. Monroy, J. V\u00e1zquez, 2006).\n
  10. Defending the Bank with a Proof Assistant<\/a> (J. Courant y J.F. Monin, 2006).\n
  11. Modeling partial attacks with Alloy<\/a> (A. Lin, M. Bond y J. Clulow, 2007).\n
  12. Formal Analysis of PKCS# 11<\/a> (S. Delaune, S. Kremer y G. Steel, 2008).\n
  13. Formal Support to Security Protocol Development: A Survey<\/a> (J.C. L\u00f3pez Pimentel y R. Monroy, 2008).\n<\/ol>\n

    Adem\u00e1s, hay series de congresos espec\u00edficos como<\/p>\n

      \n
    1. ARSPA-WITS’10 (Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security)<\/a> que se celebrar\u00e1 en Paphos (Chipre) el 27 de Marzo.\n
    2. WWV2010 (6th International Workshop on Automated Specification and Verification of Web Systems)<\/a> que se celebrar\u00e1 en Viena el 30 de Julio y se pueden mandar art\u00edculos hasta el 12 de Abril.\n<\/ol>\n","protected":false},"excerpt":{"rendered":"

      Hoy publica “El Pa\u00eds” el art\u00edculo Espa\u00f1a, blanco de m\u00e1s de cuarenta ciberataques. El art\u00edculo es un reportaje sobre “la guerra de los ciberesp\u00edas” a ra\u00edz del ataque a Google. Adem\u00e1s cuenta las iniciativas espa\u00f1olas para aumentar la seguridad. Desde sus inicios los m\u00e9todos formales se han aplicado a aumentar la seguridad de los sistemas…<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"closed","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":[164],"tags":[20,42,34,35,37,36],"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\/141"}],"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=141"}],"version-history":[{"count":10,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/141\/revisions"}],"predecessor-version":[{"id":3080,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/141\/revisions\/3080"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=141"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=141"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=141"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}