{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T11:04:51Z","timestamp":1777806291302,"version":"3.51.4"},"reference-count":61,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2025,12,11]],"date-time":"2025-12-11T00:00:00Z","timestamp":1765411200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"},{"start":{"date-parts":[[2025,12,11]],"date-time":"2025-12-11T00:00:00Z","timestamp":1765411200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Security"],"published-print":{"date-parts":[[2026,1]]},"abstract":"<jats:p>\n                    We present a decision procedure for verifying whether a protocol respects privacy goals, given a bound on the number of transitions. We consider\n                    <jats:italic toggle=\"yes\">multi message-analysis problems<\/jats:italic>\n                    , where the intruder does not know exactly the structure of the messages but rather knows several possible structures and that the real execution corresponds to\n                    <jats:italic toggle=\"yes\">one<\/jats:italic>\n                    of them. This allows for modeling a large class of security protocols, with standard cryptographic operators, non-determinism, branching and statefulness. Our first contribution is the definition of a decision procedure for a fragment of alpha-beta privacy. Moreover, we have implemented a prototype tool as a proof-of-concept and a first step towards automation. Our second contribution is to show that, for a class of protocols satisfying certain syntactic conditions, it is sound to restrict the intruder model to a typed model, where the intruder only sends well-typed messages. Our typing result holds for an unbounded number of transitions.\n                  <\/jats:p>","DOI":"10.1177\/0926227x251378716","type":"journal-article","created":{"date-parts":[[2025,12,11]],"date-time":"2025-12-11T10:11:34Z","timestamp":1765447894000},"page":"46-81","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":0,"title":["A decision procedure and typing result for alpha-beta privacy"],"prefix":"10.1177","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9028-1480","authenticated-orcid":false,"given":"Laouen","family":"Fernet","sequence":"first","affiliation":[{"name":"DIKU, University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6901-8319","authenticated-orcid":false,"given":"Sebastian","family":"M\u00f6dersheim","sequence":"additional","affiliation":[{"name":"DTU Compute, Technical University of Denmark, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9916-271X","authenticated-orcid":false,"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[{"name":"Department of Informatics, King\u2019s College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2025,12,11]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"crossref","unstructured":"Gondron S M\u00f6dersheim S Vigan\u00f2 L. Privacy as reachability. In: CSF 2022 2022 pp.130\u2013146. IEEE.","DOI":"10.1109\/CSF54842.2022.9919668"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3289255"},{"key":"e_1_3_3_4_2","doi-asserted-by":"crossref","unstructured":"Fernet L M\u00f6dersheim S. Deciding a fragment of (alpha beta)-privacy. In: STM\u00a02021 LNCS Vol. 13075 2021 pp.122\u2013142. Springer.","DOI":"10.1007\/978-3-030-91859-0_7"},{"key":"e_1_3_3_5_2","doi-asserted-by":"crossref","unstructured":"Aparicio-S\u00e1nchez D Escobar S Guti\u00e9rrez R et al. An optimizing protocol transformation for constructor finite variant theories in Maude-NPA. In: ESORICS 2020 LNCS Vol. 12309 2020 pp.230\u2013250. Springer.","DOI":"10.1007\/978-3-030-59013-0_12"},{"key":"e_1_3_3_6_2","doi-asserted-by":"crossref","unstructured":"Blanchet B. An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW 2001 2001 pp.82\u201396. IEEE.","DOI":"10.1109\/CSFW.2001.930138"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.06.002"},{"key":"e_1_3_3_8_2","doi-asserted-by":"crossref","unstructured":"Cheval V Kremer S Rakotonirina I. DEEPSEC: deciding equivalence properties in security protocols theory and practice. In: SP 2018 2018 pp.529\u2013546. IEEE.","DOI":"10.1109\/SP.2018.00033"},{"key":"e_1_3_3_9_2","doi-asserted-by":"crossref","unstructured":"Cheval V Kremer S Rakotonirina I. The Hitchhiker\u2019s guide to decidability and complexity of equivalence properties in security protocols. In: Logic Language and Security LNCS Vol. 12300 2020 pp.127\u2013145. Springer.","DOI":"10.1007\/978-3-030-62077-6_10"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00490-5"},{"key":"e_1_3_3_11_2","doi-asserted-by":"crossref","unstructured":"Cheval V. APTE: an algorithm for proving trace equivalence. In: TACAS 2014 LNCS Vol. 8413 2014 pp.587\u2013592. Springer.","DOI":"10.1007\/978-3-642-54862-8_50"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2926715"},{"key":"e_1_3_3_13_2","doi-asserted-by":"crossref","unstructured":"Tiu A Dawson J. Automating open bisimulation checking for the spi calculus. In: CSF 2010 2010 pp.307\u2013321. IEEE.","DOI":"10.1109\/CSF.2010.28"},{"key":"e_1_3_3_14_2","doi-asserted-by":"crossref","unstructured":"Tiu A Nguyen N Horne R. SPEC: an equivalence checker for security protocols. In: APLAS 2016 LNCS Vol. 10017 2016 pp.87\u201395. Springer.","DOI":"10.1007\/978-3-319-47958-3_5"},{"key":"e_1_3_3_15_2","doi-asserted-by":"crossref","unstructured":"Barbosa H Barrett CW Brain M et\u00a0al. cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022 LNCS Vol. 13243 2022 pp.415\u2013442. Springer.","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_3_16_2","doi-asserted-by":"crossref","unstructured":"Meier S Schmidt B Cremers C et\u00a0al. The TAMARIN prover for the symbolic analysis of security protocols. In: CAV 2013 LNCS Vol. 8044 2013 pp.696\u2013701. Springer.","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.10.005"},{"key":"e_1_3_3_18_2","doi-asserted-by":"crossref","unstructured":"Cheval V Rakotonirina I. Indistinguishability beyond diff-equivalence in ProVerif. In: CSF 2023 2023 pp.184\u2013199. IEEE.","DOI":"10.1109\/CSF57540.2023.00036"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.481513"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2003-11204"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.018"},{"key":"e_1_3_3_22_2","doi-asserted-by":"crossref","unstructured":"Almousa O M\u00f6dersheim S Modesti P et\u00a0al. Typing and compositionality for security protocols: a generalization to the geometric fragment. In: ESORICS 2015 LNCS Vol. 9327 2015 pp.209\u2013229. Springer.","DOI":"10.1007\/978-3-319-24177-7_11"},{"key":"e_1_3_3_23_2","doi-asserted-by":"crossref","unstructured":"Arapinis M Duflot M. Bounding messages for free in security protocols. In: FSTTCS 2007 LNCS Vol. 4855 2007 pp.376\u2013387. Springer.","DOI":"10.1007\/978-3-540-77050-3_31"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.09.003"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0059-4"},{"key":"e_1_3_3_26_2","doi-asserted-by":"crossref","unstructured":"Hess A M\u00f6dersheim S. Formalizing and proving a typing result for security protocols in Isabelle\/HOL. In: CSF 2017 2017 pp.451\u2013463. IEEE.","DOI":"10.1109\/CSF.2017.27"},{"key":"e_1_3_3_27_2","doi-asserted-by":"crossref","unstructured":"Hess A M\u00f6dersheim S. A typing result for stateful protocols. In: CSF 2018 2018 pp.374\u2013388. IEEE.","DOI":"10.1109\/CSF.2018.00034"},{"key":"e_1_3_3_28_2","doi-asserted-by":"crossref","unstructured":"Fernet L M\u00f6dersheim S Vigan\u00f2 L. A decision procedure for alpha-beta privacy for a bounded number of transitions. In: CSF 2024 2024 pp.159\u2013174. IEEE.","DOI":"10.1109\/CSF61375.2024.00011"},{"key":"e_1_3_3_29_2","unstructured":"Hinrichs T Genesereth M. Herbrand logic. Technical Report LG-2006-02 Stanford University USA. 2006. https:\/\/ginapp.stanford.edu\/reports\/LG-2006-02.pdf."},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0055-7"},{"key":"e_1_3_3_31_2","doi-asserted-by":"crossref","unstructured":"Millen J Shmatikov V. Constraint solving for bounded-process cryptographic protocol analysis. In: CCS\u00a02001 2001 pp.166\u2013175. ACM.","DOI":"10.1145\/501983.502007"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.05.004"},{"key":"e_1_3_3_33_2","doi-asserted-by":"crossref","unstructured":"Brus\u00f3 M Chatzikokolakis K den Hartog J. Formal verification of privacy for RFID systems. In: CSF 2010 2010 pp.75\u201388. IEEE.","DOI":"10.1109\/CSF.2010.13"},{"key":"e_1_3_3_34_2","unstructured":"Fernet L M\u00f6dersheim S. noname: formal verification of (alpha beta)-privacy in security protocols 2024. DOI: 10.5281\/zenodo.14198336."},{"key":"e_1_3_3_35_2","doi-asserted-by":"crossref","unstructured":"Weis SA Sarma SE Rivest RL et al. Security and privacy aspects of low-cost radio frequency identification systems. In: Security in Pervasive Computing LNCS Vol. 2802 2004 pp.201\u2013212. Springer.","DOI":"10.1007\/978-3-540-39881-3_18"},{"key":"e_1_3_3_36_2","unstructured":"Ohkubo M Suzuki K Kinoshita S. Cryptographic approach to \u201cprivacy-friendly\u201d tags. In: RFID Privacy Workshop 2003 2003."},{"key":"e_1_3_3_37_2","unstructured":"ICAO. Machine readable travel documents. Doc Series Doc 9303. \u00a0https:\/\/www.icao.int\/publications\/doc-series\/doc-9303."},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.12.023"},{"key":"e_1_3_3_39_2","unstructured":"Fernet L M\u00f6dersheim S. Private authentication with alpha-beta-privacy. In: OID 2023 2023 LNI. GI."},{"key":"e_1_3_3_40_2","doi-asserted-by":"crossref","unstructured":"Baelde D Delaune S Moreau S. A method for proving unlinkability of stateful protocols. In: CSF 2020 2020 pp.169\u2013183. IEEE.","DOI":"10.1109\/CSF49147.2020.00020"},{"key":"e_1_3_3_41_2","doi-asserted-by":"crossref","unstructured":"Arapinis M Chothia T Ritter E et\u00a0al. Analysing unlinkability and anonymity using the applied pi calculus. In: CSF 2010 2010 pp.107\u2013121. IEEE.","DOI":"10.1109\/CSF.2010.15"},{"key":"e_1_3_3_42_2","doi-asserted-by":"crossref","unstructured":"Chothia T Smirnov V. A traceability attack against e-passports. In: FC 2010 LNCS Vol. 6052 2010 pp.20\u201334. Springer.","DOI":"10.1007\/978-3-642-14577-3_5"},{"key":"e_1_3_3_43_2","doi-asserted-by":"crossref","unstructured":"Filimonov I Horne R Mauw S et\u00a0al. Breaking unlinkability of the ICAO 9303 standard for e-passports using bisimilarity. In: ESORICS 2019 LNCS Vol. 11735 2019 pp.577\u2013594. Springer.","DOI":"10.1007\/978-3-030-29959-0_28"},{"key":"e_1_3_3_44_2","doi-asserted-by":"crossref","unstructured":"Cheval V Kremer S Rakotonirina I. Exploiting symmetries when proving equivalence properties for security protocols. In: CCS 2019 2019 pp.905\u2013922. ACM.","DOI":"10.1145\/3319535.3354260"},{"key":"e_1_3_3_45_2","doi-asserted-by":"crossref","unstructured":"Baudet M. Deciding security of protocols against off-line guessing attacks. In: CCS 2005 2005 pp.16\u201325. ACM.","DOI":"10.1145\/1102120.1102125"},{"key":"e_1_3_3_46_2","doi-asserted-by":"crossref","unstructured":"Rajaona F Boureanu I Ramanujam R et\u00a0al. Epistemic model checking for privacy. In: CSF 2024 2024 pp.1\u201316. IEEE.","DOI":"10.1109\/CSF61375.2024.00020"},{"key":"e_1_3_3_47_2","doi-asserted-by":"crossref","unstructured":"Rajaona F Boureanu I Ramanujam R et\u00a0al. Phoebe: epistemic model checker for privacy properties in security protocols. 2024. https:\/\/github.com\/UoS-SCCS\/phoebe\/.","DOI":"10.1109\/CSF61375.2024.00020"},{"key":"e_1_3_3_48_2","doi-asserted-by":"crossref","unstructured":"Cortier V Grimm N Lallemand J et\u00a0al. A type system for privacy properties. In: CCS 2017 2017 pp.409\u2013423. ACM.","DOI":"10.1145\/3133956.3133998"},{"key":"e_1_3_3_49_2","doi-asserted-by":"crossref","unstructured":"Cortier V Grimm N Lallemand J et\u00a0al. Equivalence properties by typing in cryptographic branching protocols. In: POST 2018 LNCS Vol. 10804 2018 pp.160\u2013187. Springer.","DOI":"10.1007\/978-3-319-89722-6_7"},{"key":"e_1_3_3_50_2","doi-asserted-by":"crossref","unstructured":"Armando A Carbone R Compagna L. SATMC: a sat-based model checker for security-critical systems. In: TACAS 2014 LNCS Vol. 8413 2014 pp.31\u201345. Springer.","DOI":"10.1007\/978-3-642-54862-8_3"},{"key":"e_1_3_3_51_2","doi-asserted-by":"crossref","unstructured":"Armando A Basin D Boichut Y et\u00a0al. The AVISPA tool for the automated validation of internet security protocols and applications. In: CAV 2005 LNCS Vol. 3576 2005 pp.281\u2013285. Springer.","DOI":"10.1007\/11513988_27"},{"key":"e_1_3_3_52_2","unstructured":"Armando A Arsac W Avanesov T et\u00a0al. The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: TACAS 2012 LNCS Vol. 7214 2012 pp.267\u2013282. Springer."},{"key":"e_1_3_3_53_2","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim S Vigan\u00f2 L. The open-source fixed-point model checker for symbolic analysis of security protocols. In: FOSAD 2007\/2008\/2009 Tutorial Lectures LNCS Vol. 5705 2009 pp.166\u2013194. Springer.","DOI":"10.1007\/978-3-642-03829-7_6"},{"key":"e_1_3_3_54_2","doi-asserted-by":"crossref","unstructured":"Turuani M. The CL-Atse protocol analyser. In: RTA 2006 LNCS Vol. 4098 2006 pp.277\u2013286. Springer.","DOI":"10.1007\/11805618_21"},{"key":"e_1_3_3_55_2","doi-asserted-by":"crossref","unstructured":"Hess A M\u00f6dersheim S Brucker A et\u00a0al. Performing security proofs of stateful protocols. In: CSF 2021 2021 pp.1\u201316. IEEE.","DOI":"10.1109\/CSF51468.2021.00006"},{"key":"e_1_3_3_56_2","doi-asserted-by":"crossref","unstructured":"Chr\u00e9tien R Cortier V Delaune S. Typing messages for free in security protocols: the case of equivalence properties. In: CONCUR 2014 Vol. 8704 2014 pp.372\u2013386. Springer.","DOI":"10.1007\/978-3-662-44584-6_26"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3343507"},{"key":"e_1_3_3_58_2","doi-asserted-by":"crossref","unstructured":"Chretien R Cortier V Delaune S. Decidability of trace equivalence for protocols with nonces. In: CSF 2015 2015 pp.170\u2013184. IEEE.","DOI":"10.1109\/CSF.2015.19"},{"key":"e_1_3_3_59_2","doi-asserted-by":"crossref","unstructured":"Cortier V Dallon A Delaune S. SAT-Equiv: an efficient tool for equivalence properties. In: CSF 2017 2017 pp.481\u2013494. IEEE.","DOI":"10.1109\/CSF.2017.15"},{"key":"e_1_3_3_60_2","doi-asserted-by":"crossref","unstructured":"Cortier V Dallon A Delaune S. Efficiently deciding equivalence for standard primitives and phases. In: ESORICS 2018 LNCS Vol. 11098 2018 pp.491\u2013511. Springer.","DOI":"10.1007\/978-3-319-99073-6_24"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09582-9"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/3577020"}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0926227X251378716","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.1177\/0926227X251378716","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0926227X251378716","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:45:56Z","timestamp":1777495556000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.1177\/0926227X251378716"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12,11]]},"references-count":61,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,1]]}},"alternative-id":["10.1177\/0926227X251378716"],"URL":"https:\/\/doi.org\/10.1177\/0926227x251378716","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,12,11]]}}}