{"id":4064,"date":"2014-01-28T05:35:49","date_gmt":"2014-01-28T04:35:49","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4064"},"modified":"2014-01-27T06:36:52","modified_gmt":"2014-01-27T05:36:52","slug":"verifying-document-confidentiality-of-a-conference-management-system","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/verifying-document-confidentiality-of-a-conference-management-system\/","title":{"rendered":"Verifying document confidentiality of a conference management system"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de verificaci\u00f3n formal con <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/\">Isabelle\/HOL<\/a>  titulado <a href=\"http:\/\/www21.in.tum.de\/~popescua\/pdf\/confsys.pdf\">Verifying document confidentiality of a conference management system<\/a>.<\/p>\n<p>Sus autores son Sudeep Kanav, <a href=\"http:\/\/www21.in.tum.de\/~lammich\">Peter Lammich<\/a> y <a href=\"http:\/\/www21.in.tum.de\/~popescua\">Andrei Popescu<\/a> (de la Universidad T\u00e9cnica de Munich).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nWe present a case study in verified security for realistic systems: the implementation of a conference management system, whose functional kernel is faithfully represented in the Isabelle theorem prover, where we specify and verify confidentiality properties. The various theoretical and practical challenges posed by this development led to some novel security model and verification method that we hope is reusable for other multi-user document management systems.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de verificaci\u00f3n formal con Isabelle\/HOL titulado Verifying document confidentiality of a conference management system. Sus autores son Sudeep Kanav, Peter Lammich y Andrei Popescu (de la Universidad T\u00e9cnica de Munich). Su resumen es We present a case study in verified security for realistic systems: the implementation of a conference management&#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":[100],"tags":[144,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\/4064"}],"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=4064"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4064\/revisions"}],"predecessor-version":[{"id":4065,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4064\/revisions\/4065"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4064"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4064"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4064"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}