caa a22 4500 605516383 CHVBK 20210128100714.0 cr unu---uuuuu 210128e20150301xx s 000 0 eng 10.1007/s00165-014-0315-x doi (NATIONALLICENCE)springer-10.1007/s00165-014-0315-x Formalizing provable anonymity in Isabelle/HOL [Elektronische Daten] [Yongjian Li, Jun Pang] 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. British Computer Society, 2014 Anonymity nationallicence Security protocols nationallicence Theorem proving nationallicence Inductive methods nationallicence Li Yongjian State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, P.O. Box 8717, Beijing, China aut Pang Jun Computer Science and Communications, Faculty of Science, Technology and Communication, University of Luxembourg, Walferdange, Luxembourg aut Formal Aspects of Computing Springer London 27/2(2015-03-01), 255-282 0934-5043 27:2<255 2015 27 165 https://doi.org/10.1007/s00165-014-0315-x text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0315-x text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Li Yongjian State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, P.O. Box 8717, Beijing, China aut NATIONALLICENCE 700 1- Pang Jun Computer Science and Communications, Faculty of Science, Technology and Communication, University of Luxembourg, Walferdange, Luxembourg aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/2(2015-03-01), 255-282 0934-5043 27:2<255 2015 27 165