{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,26]],"date-time":"2023-05-26T19:29:48Z","timestamp":1685129388474},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2015,3,1]],"date-time":"2015-03-01T00:00:00Z","timestamp":1425168000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2015,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We formalize in a theorem prover the notion of provable anonymity. Our formalization relies on inductive definitions of message distinguishing ability and observational equivalence on traces observed by the intruder. Our theory differs from its original proposal and essentially boils down to the inductive definition of distinguishing messages with respect to a knowledge set for the intruder. We build our theory in Isabelle\/HOL to achieve a mechanical framework for the analysis of anonymity protocols. Its feasibility is illustrated through two case studies of the Crowds and Onion Routing protocols.<\/jats:p>","DOI":"10.1007\/s00165-014-0315-x","type":"journal-article","created":{"date-parts":[[2014,9,24]],"date-time":"2014-09-24T00:00:38Z","timestamp":1411516838000},"page":"255-282","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Formalizing provable anonymity in Isabelle\/HOL"],"prefix":"10.1145","volume":"27","author":[{"given":"Yongjian","family":"Li","sequence":"first","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, P.O. Box 8717, Beijing, China"},{"name":"College of Information Engineering, Capital Normal University, Beijing, China"}]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[{"name":"Computer Science and Communications, Faculty of Science, Technology and Communication, University of Luxembourg, Walferdange, Luxembourg"},{"name":"Interdisciplinary Centre for Security, Reliability and Trust, University of Luxembourg, Walferdange, Luxembourg"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.032"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/2794418.2794756"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.06.002"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Baudet M (2005) Deciding security of protocols against off-line guessing attacks. In: Proceedings of 12th ACM conference on computer and communications security. ACM Press New York pp 16\u201325","DOI":"10.1145\/1102120.1102125"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Blanchet B (2001) An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of 14th IEEE computer security foundations workshop. IEEE Press New York pp 82\u201396","DOI":"10.1109\/CSFW.2001.930138"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bhargava M Palamidessi C (2005) Probabilistic anonymity. In: Proceedings of 16th conference on concurrency theory. Volume 3653 of LNCS. Springer Berlin pp 171\u2013185","DOI":"10.1007\/11539452_16"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Cheval V Blanchet B (2013) Proving more observational equivalences with ProVerif. In: Proceedings 2nd POST. Volume 7796 of LNCS. Springer Berlin pp 226\u2013246","DOI":"10.1007\/978-3-642-36830-1_12"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Cheval V Comon-Lundh H Delaune S (2011) Trace equivalence decision: negative tests and non-determinism. In: Proceedings of 18th ACM conference on computer and communications security. ACM Press New York pp 321\u2013330","DOI":"10.1145\/2046707.2046744"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Cheval V Cortier V Plet A (2013) Lengths may break privacy\u2014or how to check for equivalences with length. In: Proceedings of 25th conference on computer aided verification. Springer Berlin (to appear)","DOI":"10.1007\/978-3-642-39799-8_50"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/358549.358563"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Chothia T (2006) Analysing the mute anonymous file-sharing system using the pi-calculus. In: Proceedings of 26th conference on formal methods for networked and distributed systems. Volume 4229 of LNCS. Springer Berlin pp 115\u2013130","DOI":"10.1007\/11888116_9"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Chothia T Orzan SM Pang J Torabi Dashti M (2007) A framework for automatically checking anonymity with\u00a0 \u03bc CRL. In: Proceedings of 2nd symposium on trustworthy global computing. Volume 4661 of LNCS. Springer Berlin pp 301\u2013318","DOI":"10.1007\/978-3-540-75336-0_19"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Dong N Jonker HL Pang J (2012) Formal analysis of privacy in an eHealth protocol. In: Proceedings of 17th European symposium on research in computer security. Volume 7459 of LNCS. Springer Berlin pp 325\u2013342","DOI":"10.1007\/978-3-642-33167-1_19"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Dong N Jonker HL Pang J (2013) Enforcing privacy in the presence of others: notions formalisations and relations. In: Proceedings of 18th European symposium on research in computer security. Volume 8134 of LNCS. Springer Berlin pp 499\u2013516","DOI":"10.1007\/978-3-642-40203-6_28"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/1576303.1576305"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Dingledine R Mathewson N Syverson PF (2004) Tor: the second-generation onion router. In: Proceedings of 13th USENIX security symposium pp 303\u2013320","DOI":"10.21236\/ADA465464"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Deng Y Palamidessi C Pang J (2007) Weak probabilistic anonymity. In: Proceedings of 3rd workshop on security issues in concurrency. Volume 180 of ENTCS pp 55\u201376","DOI":"10.1016\/j.entcs.2005.05.047"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Fokkink WJ Pang J (2003) Cones and foci for protocol verification revisited. In: Proceedings of 6th conference on foundations of software science and computation structures. Volume 2620 of LNCS. Springer Berlin pp 267\u2013281","DOI":"10.1007\/3-540-36576-1_17"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0004-3"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Garcia FD Hasuo I Pieters W van Rossum P (2005) Provable anonymity. In: Proceedings of 3rd workshop on formal methods in security engineering. ACM Press New York pp 63\u201372","DOI":"10.1145\/1103576.1103585"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Goldschlag DM Reed MG Syverson PF (1996) Hiding routing information. In: Proceedings of 1st workshop on information hiding. LNCS 1174. Springer Berlin pp 137\u2013150","DOI":"10.1007\/3-540-61996-8_37"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.5555\/1145948.1145953"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/1297689.1297694"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jalgor.2009.02.007"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2006.06.016"},{"key":"e_1_2_1_2_27_2","unstructured":"Kong W Ogata K Cheng J Futatsugi K (2008) Trace anonymity in the OTS\/CafeOBJ method. In: Proceedings of 8th IEEE international conference on computer and information technology. IEEE Press New York pp 754\u2013759"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Kremer S Ryan M (2005) Analysis of an electronic voting protocol in the applied pi-calculus. In: Proceedings of 14th European symposium on programming. Volume 3444 of LNCS. Springer Berlin pp 186\u2013200","DOI":"10.1007\/978-3-540-31987-0_14"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Luo L Cai X Pang J Deng Y (2007) Analyzing an electronic cash protocol using applied pi-calculus. In: Proceedings of 5th conference on applied cryptography and network security. Volume 4521 of LNCS. Springer Berlin pp 87\u2013103","DOI":"10.1007\/978-3-540-72738-5_6"},{"key":"e_1_2_1_2_30_2","unstructured":"Li Y Formalization of provable anonymity in Isabelle. http:\/\/lcs.ios.ac.cn\/~lyj238\/anonymity.html"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Li Y Pang J (2011) An inductive approach to provable anonymity. In: Proceedings of 6th conference on availability reliability and security. IEEE Press New York pp 454\u2013459","DOI":"10.1109\/ARES.2011.70"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-011-0187-2"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Nipkow T Paulson LC Wenzel M (2002) Isabelle\/HOL: a proof assistant for higher-order logic. LNCS 2283. Springer Berlin","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Pang J (2002) Analysis of a security protocol in \u03bc CRL. In: Proceedings of 4th conference on formal engineering methods. Volume 2495 of LNCS. Springer Berlin pp 396\u2013400","DOI":"10.1007\/3-540-36103-0_40"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/353677.353681"},{"key":"e_1_2_1_2_36_2","unstructured":"Pfitzmann A Hansen M (2010) A terminology for talking about privacy by data minimization: anonymity unlinkability undetectability unobservability pseudonymity and identity management"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Pang J Zhang C (2009) How to work with honest but curious judges? (preliminary report). In: Proceedings of 7th workshop on security issues in concurrency. Volume 7 of EPTCS pp 31\u201345","DOI":"10.4204\/EPTCS.7.3"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/290163.290168"},{"key":"e_1_2_1_2_39_2","unstructured":"Syverson PF Goldschlag DM Reed MG (1997) Anonymous connections and onion routing. In: Proceedings of 18th IEEE symposium on security and privacy. IEEE Press New York pp 44\u201354"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.5555\/1297352.1297359"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Schneider S Sidiropoulos A (1996) CSP and anonymity. In: Proceedings of 4th European symposium on research in computer security. Volume 1146 of LNCS. Springer Berlin pp 198\u2013218","DOI":"10.1007\/3-540-61770-1_38"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Wenzel M (1999) Isar: a generic interpretative approach to readable formal proof documents. In: Proceedings of 12th conference on theorem proving in higher order logics. Volume 1690 of LNCS. Springer Berlin pp 167\u2013184","DOI":"10.1007\/3-540-48256-3_12"},{"key":"e_1_2_1_2_43_2","unstructured":"Yan L Sere K Zhou X Pang J (2004) Towards an integrated architecture for peer-to-peer and ad hoc overlay network applications. In: Proceedings of 10th workshop on future trends in distributed computing systems. IEEE Press New York pp 312\u2013318"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-014-0315-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-014-0315-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-014-0315-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:06:49Z","timestamp":1641485209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-014-0315-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["10.1007\/s00165-014-0315-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-014-0315-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3]]}}}