{"id":936,"date":"2026-07-14T15:56:10","date_gmt":"2026-07-14T14:56:10","guid":{"rendered":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/?page_id=936"},"modified":"2026-07-14T15:56:10","modified_gmt":"2026-07-14T14:56:10","slug":"alpha-beta-privacy-a-novel-and-declarative-way-to-reason-about-privacy","status":"publish","type":"page","link":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/alpha-beta-privacy-a-novel-and-declarative-way-to-reason-about-privacy\/","title":{"rendered":"Alpha-Beta Privacy (a novel and declarative way to reason about privacy)"},"content":{"rendered":"\n<div class=\"wp-block-group is-nowrap is-layout-flex wp-container-core-group-is-layout-8f761849 wp-block-group-is-layout-flex\">\n<figure class=\"wp-block-image\"><img decoding=\"async\" src=\"https:\/\/stadium.open.ac.uk\/stadia\/stadia\/speakerimages\/3593.jpg\" alt=\"Prof. Luca Vigano\"\/><\/figure>\n\n\n\n<p class=\"wp-block-paragraph\">Prof. Luca Vigano<br><small>This event took place on Friday 15 June 2018 at 11:30<\/small><\/p>\n<\/div>\n\n\n\n<p class=\"wp-block-paragraph\"><br>Formally specifying privacy goals is not trivial. The most widely used approach in formal methods is based on the static equivalence of frames in the applied pi-calculus, basically asking whether or not the intruder is able to distinguish two given worlds. A subtle question is how we can be sure that we have specified all pairs&nbsp;of worlds to properly reflect our intuitive privacy goal. To address this problem, we introduce a novel and declarative way to specify privacy goals, called &#8220;alpha-beta&nbsp;privacy&#8221;, and relate it to static equivalence. This new approach is based on specifying two formulae alpha and beta in first-order logic with Herbrand universes, where&nbsp;alpha reflects the intentionally released information and beta includes the actual cryptographic (&#8220;technical&#8221;) messages the intruder can see. Then alpha-beta privacy&nbsp;means that the intruder cannot derive any &#8220;non-technical&#8221; statement from beta that he cannot derive from alpha already. We describe by a variety of examples how&nbsp;this notion can be used in practice. Even though alpha-beta privacy does not directly contain a notion of distinguishing between worlds, there is a close relationship&nbsp;to static equivalence of frames that we investigate formally. This allows us to justify (and criticize) the specifications that are currently used in verification tools, and&nbsp;obtain partial tool support for alpha-beta privacy.&nbsp;<br>Joint work with Sebastian Moedersheim and Thomas Gross.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><a href=\"http:\/\/stadium.open.ac.uk\/stadia\/preview.php?s=29&amp;whichevent=3098\">Watch the webcast replay &gt;&gt;<\/a><\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><a href=\"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/past-seminars\/\">View all past events<\/a><\/p>\n\n\n\n<div class=\"wp-block-group is-nowrap is-layout-flex wp-container-core-group-is-layout-8f761849 wp-block-group-is-layout-flex\">\n<figure class=\"wp-block-image size-full has-custom-css wp-custom-css-ac9b5317\"><img loading=\"lazy\" decoding=\"async\" width=\"213\" height=\"246\" src=\"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-content\/uploads\/sites\/8\/2026\/07\/image-2.png\" alt=\"Maven of the Month\" class=\"wp-image-537\"\/><\/figure>\n\n\n\n<div class=\"wp-block-group is-vertical is-layout-flex wp-container-core-group-is-layout-4fc3f8e1 wp-block-group-is-layout-flex\">\n<h3 class=\"wp-block-heading\"><a href=\"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/maven-of-the-month\/\">Maven of the Month<\/a><\/h3>\n\n\n\n<p class=\"wp-block-paragraph\">We are also inviting top experts in AI and Knowledge Technologies to discuss major socio-technological topics with an audience that comprises both members of the Knowledge Media Institute, as well as the wider staff at The Open University. Differently from our seminar series, these events follow a Q&amp;A format.<\/p>\n<\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Prof. Luca ViganoThis event took place on Friday 15 June 2018 at 11:30 Formally specifying privacy goals is not trivial. The most widely used approach in formal methods is based on the static equivalence of frames in the applied pi-calculus, basically asking whether or not the intruder is able to distinguish two given worlds. A [&hellip;]<\/p>\n","protected":false},"author":13,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"unity_related_person":[],"unity_sdg":[],"unity_research_theme":[],"unity_strategic_priority":[],"unity_enabler":[],"unity_general_category":[],"unity_stem_unit":[],"unity_related_project":[],"unity_related_archived_project":[],"unity_related_event":[],"class_list":["post-936","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/pages\/936","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/users\/13"}],"replies":[{"embeddable":true,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/comments?post=936"}],"version-history":[{"count":1,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/pages\/936\/revisions"}],"predecessor-version":[{"id":937,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/pages\/936\/revisions\/937"}],"wp:attachment":[{"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/media?parent=936"}],"wp:term":[{"taxonomy":"unity_related_person","embeddable":true,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/unity_related_person?post=936"},{"taxonomy":"unity_sdg","embeddable":true,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/unity_sdg?post=936"},{"taxonomy":"unity_research_theme","embeddable":true,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/unity_research_theme?post=936"},{"taxonomy":"unity_strategic_priority","embeddable":true,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/unity_strategic_priority?post=936"},{"taxonomy":"unity_enabler","embeddable":true,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/unity_enabler?post=936"},{"taxonomy":"unity_general_category","embeddable":true,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/unity_general_category?post=936"},{"taxonomy":"unity_stem_unit","embeddable":true,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/unity_stem_unit?post=936"},{"taxonomy":"unity_related_project","embeddable":true,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/unity_related_project?post=936"},{"taxonomy":"unity_related_archived_project","embeddable":true,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/unity_related_archived_project?post=936"},{"taxonomy":"unity_related_event","embeddable":true,"href":"https:\/\/schools.stem.open.ac.uk\/knowledge-media-institute\/wp-json\/wp\/v2\/unity_related_event?post=936"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}