{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,11]],"date-time":"2025-12-11T20:51:12Z","timestamp":1765486272736,"version":"3.41.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,1,22]],"date-time":"2019-01-22T00:00:00Z","timestamp":1548115200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Priv. Secur."],"published-print":{"date-parts":[[2019,2,28]]},"abstract":"<jats:p>The formal specification of privacy goals in symbolic protocol models has proved to be not quite trivial so far. 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. But then a subtle question emerges: How can we be sure that we have specified all pairs of worlds to properly reflect our intuitive privacy goal? To address this problem, we introduce in this article a novel and declarative way to specify privacy goals, called (\u03b1, \u03b2)-privacy. This new approach is based on specifying two formulae \u03b1 and \u03b2 in first-order logic with Herbrand universes, where \u03b1 reflects the intentionally released information and \u03b2 includes the actual cryptographic (\u201ctechnical\u201d) messages the intruder can see. Then (\u03b1, \u03b2)-privacy means that the intruder cannot derive any \u201cnontechnical\u201d statement from \u03b2 that he cannot derive from \u03b1 already. We describe by a variety of examples how this notion can be used in practice. Even though (\u03b1, \u03b2)-privacy does not directly contain a notion of distinguishing between worlds, there is a close relationship 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 obtain a decision procedure for a large fragment of (\u03b1, \u03b2)-privacy.<\/jats:p>","DOI":"10.1145\/3289255","type":"journal-article","created":{"date-parts":[[2019,1,23]],"date-time":"2019-01-23T13:02:14Z","timestamp":1548248534000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Alpha-Beta Privacy"],"prefix":"10.1145","volume":"22","author":[{"given":"Sebastian","family":"M\u00f6dersheim","sequence":"first","affiliation":[{"name":"DTU Compute, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9916-271X","authenticated-orcid":false,"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[{"name":"Department of Informatics, King's College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,1,22]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36467-6_3"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1841962.1841969"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2005.14"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.12.023"},{"volume-title":"Programming Languages with Applications to Biology and Security \u2014 Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday (LNCS 9465)","author":"Almousa Omar","key":"e_1_2_1_6_1","unstructured":"Omar Almousa , Sebastian M\u00f6dersheim , and Luca Vigan\u00f2 . 2015. Alice and Bob: Reconciling formal models and implementation . In Programming Languages with Applications to Biology and Security \u2014 Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday (LNCS 9465) . Springer , 66--85. Omar Almousa, Sebastian M\u00f6dersheim, and Luca Vigan\u00f2. 2015. Alice and Bob: Reconciling formal models and implementation. In Programming Languages with Applications to Biology and Security \u2014 Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday (LNCS 9465). Springer, 66--85."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45741-3_13"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2017.03.001"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.06.002"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271090"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.05.004"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.19"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2728816.2728823"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 22nd International Conference on Implementation and Application of Automata (CIAA\u201917)","author":"Cortier V\u00e9ronique","year":"2017","unstructured":"V\u00e9ronique Cortier . 2017 . Electronic voting: How logic can help . In Proceedings of the 22nd International Conference on Implementation and Application of Automata (CIAA\u201917) , Marne-la-Vall\u00e9e, France. Springer, xi--xii. V\u00e9ronique Cortier. 2017. Electronic voting: How logic can help. In Proceedings of the 22nd International Conference on Implementation and Application of Automata (CIAA\u201917), Marne-la-Vall\u00e9e, France. Springer, xi--xii."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.15"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133998"},{"key":"e_1_2_1_18_1","volume-title":"Relating two standard notions of secrecy. Logical Methods in Computer Science 3, 3","author":"Cortier V\u00e9ronique","year":"2007","unstructured":"V\u00e9ronique Cortier , Micha\u00ebl Rusinowitch , and Eugen Zalinescu . 2007. Relating two standard notions of secrecy. Logical Methods in Computer Science 3, 3 ( 2007 ). V\u00e9ronique Cortier, Micha\u00ebl Rusinowitch, and Eugen Zalinescu. 2007. Relating two standard notions of secrecy. Logical Methods in Computer Science 3, 3 (2007)."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-15777"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.10.005"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-09428-1_17"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1791834.1791836"},{"volume-title":"Mathematical Logic","author":"Ebbinghaus Heinz-Dieter","key":"e_1_2_1_23_1","unstructured":"Heinz-Dieter Ebbinghaus , J\u00f6rg Flum , and Wolfgang Thomas . 1994. Mathematical Logic . Springer . Heinz-Dieter Ebbinghaus, J\u00f6rg Flum, and Wolfgang Thomas. 1994. Mathematical Logic. Springer."},{"volume-title":"Proceedings of the IEEE Symposium on Security and Privacy","author":"Joseph","key":"e_1_2_1_24_1","unstructured":"Joseph A. Goguen and Jos\u00e9 Meseguer. 1982. Security policies and security models . In Proceedings of the IEEE Symposium on Security and Privacy , Oakland, CA. IEEE CS Pr., 11--20. Joseph A. Goguen and Jos\u00e9 Meseguer. 1982. Security policies and security models. In Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA. IEEE CS Pr., 11--20."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891832"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32275-7_24"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2007.367856"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1297689.1297693"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217299.1217302"},{"volume-title":"Encyclopedia of Cryptography and Security. 605--607.","author":"Mantel Heiko","key":"e_1_2_1_32_1","unstructured":"Heiko Mantel . 2011. Information flow and noninterference . In Encyclopedia of Cryptography and Security. 605--607. Heiko Mantel. 2011. Information flow and noninterference. In Encyclopedia of Cryptography and Security. 605--607."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.22"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_41"},{"volume-title":"Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW'99)","author":"Ryan Peter Y. A.","key":"e_1_2_1_35_1","unstructured":"Peter Y. A. Ryan and S. A. Schneider . 1999. Process algebra and non-interference . In Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW'99) , Mordano, Italy. IEEE CS Pr. Peter Y. A. Ryan and S. A. Schneider. 1999. Process algebra and non-interference. In Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW'99), Mordano, Italy. IEEE CS Pr."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.971193"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00245-2"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218488502001648"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753480"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC2759"}],"container-title":["ACM Transactions on Privacy and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3289255","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3289255","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:38Z","timestamp":1750207418000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3289255"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,22]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2,28]]}},"alternative-id":["10.1145\/3289255"],"URL":"https:\/\/doi.org\/10.1145\/3289255","relation":{},"ISSN":["2471-2566","2471-2574"],"issn-type":[{"type":"print","value":"2471-2566"},{"type":"electronic","value":"2471-2574"}],"subject":[],"published":{"date-parts":[[2019,1,22]]},"assertion":[{"value":"2017-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}