1: \begin{thebibliography}{}
2:
3: \bibitem[\protect\citeauthoryear{Abadi and Gordon}{Abadi and
4: Gordon}{1997}]{abadi97}
5: Abadi, M. and A.~D. Gordon (1997).
6: \newblock A calculus for cryptographic protocols: The spi calculus.
7: \newblock In {\em Fourth {ACM} Conference on Computer and Communications
8: Security}, pp.\ 36--47.
9:
10: \bibitem[\protect\citeauthoryear{Chaum}{Chaum}{1988}]{Chaum88}
11: Chaum, D. (1988).
12: \newblock The dining cryptographers problem: Unconditional sender and recipient
13: untraceability.
14: \newblock {\em Journal of Cryptology\/}~{\em 1\/}(1), 65--75.
15:
16: \bibitem[\protect\citeauthoryear{Danezis}{Danezis}{2003}]{danezis:pet2003}
17: Danezis, G. (2003).
18: \newblock Mix-networks with restricted routes.
19: \newblock In R.~Dingledine (Ed.), {\em Proc.~Privacy Enhancing Technologies
20: Workshop (PET 2003)}, Volume 2760 of {\em Lecture Notes in Computer Science},
21: Berlin/New York, pp.\ 54--68. Springer-Verlag.
22:
23: \bibitem[\protect\citeauthoryear{Diaz, Seys, Claessens, and Preneel}{Diaz
24: et~al.}{2002}]{Diaz02}
25: Diaz, C., S.~Seys, J.~Claessens, and B.~Preneel (2002).
26: \newblock Towards measuring anonymity.
27: \newblock In R.~Dingledine and P.~Syverson (Eds.), {\em Proc.~Privacy Enhancing
28: Technologies Workshop (PET 2002)}, Volume 2482 of {\em Lecture Notes in
29: Computer Science}, Berlin/New York, pp.\ 54--68. Springer-Verlag.
30:
31: \bibitem[\protect\citeauthoryear{Fagin, Halpern, and Megiddo}{Fagin
32: et~al.}{1990}]{FHM}
33: Fagin, R., J.~Y. Halpern, and N.~Megiddo (1990).
34: \newblock A logic for reasoning about probabilities.
35: \newblock {\em Information and Computation\/}~{\em 87\/}(1/2), 78--128.
36:
37: \bibitem[\protect\citeauthoryear{Fagin, Halpern, Moses, and Vardi}{Fagin
38: et~al.}{1995}]{FHMV}
39: Fagin, R., J.~Y. Halpern, Y.~Moses, and M.~Y. Vardi (1995).
40: \newblock {\em Reasoning about Knowledge}.
41: \newblock Cambridge, Mass.: MIT Press.
42:
43: \bibitem[\protect\citeauthoryear{Focardi and Gorrieri}{Focardi and
44: Gorrieri}{2001}]{focardi01}
45: Focardi, R. and R.~Gorrieri (2001).
46: \newblock Classification of security properties ({P}art {I}: {I}nformation
47: flow).
48: \newblock In {\em Foundations of Security Analysis and Design}, pp.\ 331--396.
49: Springer.
50:
51: \bibitem[\protect\citeauthoryear{Fournet and Abadi}{Fournet and
52: Abadi}{2003}]{fournet02}
53: Fournet, C. and M.~Abadi (2003).
54: \newblock Hiding names: Private authentication in the applied pi calculus.
55: \newblock In {\em Proc.~International Symposium on Software Security (ISSS
56: 2002)}, Volume 2609 of {\em Lecture Notes in Computer Science}, Berlin/New
57: York, pp.\ 317--338. Springer-Verlag.
58:
59: \bibitem[\protect\citeauthoryear{Glasgow, MacEwen, and Panangaden}{Glasgow
60: et~al.}{1992}]{GMP92}
61: Glasgow, J., G.~MacEwen, and P.~Panangaden (1992).
62: \newblock A logic for reasoning about security.
63: \newblock {\em ACM Transactions on Computer Systems\/}~{\em 10\/}(3), 226--264.
64:
65: \bibitem[\protect\citeauthoryear{Goel, Robson, Polte, and Sirer}{Goel
66: et~al.}{2002}]{goel02}
67: Goel, S., M.~Robson, M.~Polte, and E.~G. Sirer (2002).
68: \newblock Herbivore: A scalable and efficient protocol for anonymous
69: communication.
70: \newblock Unpublished manuscript.
71:
72: \bibitem[\protect\citeauthoryear{Gray and Syverson}{Gray and
73: Syverson}{1998}]{gray98}
74: Gray, J.~W. and P.~F. Syverson (1998).
75: \newblock A logical approach to multillevel security of probabilistic systems.
76: \newblock {\em Distributed Computing\/}~{\em 11\/}(2), 73--90.
77:
78: \bibitem[\protect\citeauthoryear{Halpern and O'Neill}{Halpern and
79: O'Neill}{2002}]{HalOn02}
80: Halpern, J.~Y. and K.~O'Neill (2002).
81: \newblock Secrecy in multiagent systems.
82: \newblock In {\em Proc.~15th IEEE Computer Security Foundations Workshop}, pp.\
83: 32--46.
84:
85: \bibitem[\protect\citeauthoryear{Halpern and O'Neill}{Halpern and
86: O'Neill}{2003}]{HalOn03}
87: Halpern, J.~Y. and K.~O'Neill (2003).
88: \newblock Anonymity and information hiding in multiagent systems.
89: \newblock In {\em Proc.~16th IEEE Computer Security Foundations Workshop}, pp.\
90: 75--88.
91:
92: \bibitem[\protect\citeauthoryear{Halpern and Pucella}{Halpern and
93: Pucella}{2001}]{HalPuc01}
94: Halpern, J.~Y. and R.~Pucella (2001).
95: \newblock On the relationship between strand spaces and multi-agent systems.
96: \newblock In {\em Proc.~Eighth ACM Conference on Computer and Communications
97: Security}, pp.\ 106--115.
98: \newblock To appear, {\em ACM Transactions on Information and System Security}.
99:
100: \bibitem[\protect\citeauthoryear{Halpern and Tuttle}{Halpern and
101: Tuttle}{1993}]{HT}
102: Halpern, J.~Y. and M.~R. Tuttle (1993).
103: \newblock Knowledge, probability, and adversaries.
104: \newblock {\em Journal of the ACM\/}~{\em 40\/}(4), 917--962.
105:
106: \bibitem[\protect\citeauthoryear{Hoare}{Hoare}{1985}]{hoare85}
107: Hoare, C. (1985).
108: \newblock {\em Communicating Sequential Processes}.
109: \newblock Prentice-Hall.
110:
111: \bibitem[\protect\citeauthoryear{Hughes and Shmatikov}{Hughes and
112: Shmatikov}{2004}]{hughes02}
113: Hughes, D. and V.~Shmatikov (2004).
114: \newblock Information hiding, anonymity and privacy: a modular approach.
115: \newblock {\em Journal of Computer Security\/}~{\em 12\/}(1), 3--36.
116:
117: \bibitem[\protect\citeauthoryear{Kwiatkowska, Norman, and Parker}{Kwiatkowska
118: et~al.}{2001}]{KNP01}
119: Kwiatkowska, M., G.~Norman, and D.~Parker (2001).
120: \newblock {PRISM}: Probabilistic symbolic model checker.
121: \newblock In P.~Kemper (Ed.), {\em Proc.~Tools Session of Aachen 2001
122: International Multiconference on Measurement, Modelling and Evaluation of
123: Computer-Communication Systems}, pp.\ 7--12.
124: \newblock Available as Technical Report 760/2001, University of Dortmund.
125:
126: \bibitem[\protect\citeauthoryear{Levine and Shields}{Levine and
127: Shields}{2002}]{levine02}
128: Levine, B. and C.~Shields (2002).
129: \newblock Hordes: A multicast based protocol for anonymity.
130: \newblock {\em Journal of Computer Security\/}~{\em 10\/}(3), 213--240.
131:
132: \bibitem[\protect\citeauthoryear{Milner}{Milner}{1980}]{Mil}
133: Milner, R. (1980).
134: \newblock {\em A Calculus of Communicating Systems}.
135: \newblock Lecture Notes in Computer Science, Vol. 92. Berlin/New York:
136: Springer-Verlag.
137:
138: \bibitem[\protect\citeauthoryear{Pfitzmann and K\"{o}hntopp}{Pfitzmann and
139: K\"{o}hntopp}{2001}]{terminology}
140: Pfitzmann, A. and M.~K\"{o}hntopp (2001).
141: \newblock Anonymity, unobservability, and pseudeonymity: a proposal for
142: terminology.
143: \newblock In {\em International Workshop on Designing Privacy Enhancing
144: Technologies}, New York, pp.\ 1--9. Springer-Verlag.
145:
146: \bibitem[\protect\citeauthoryear{Reiter and Rubin}{Reiter and
147: Rubin}{1998}]{reiter98}
148: Reiter, M. and A.~Rubin (1998).
149: \newblock Crowds: Anonymity for web transactions.
150: \newblock {\em ACM Transactions on Information and System Security\/}~{\em
151: 1\/}(1), 66--92.
152:
153: \bibitem[\protect\citeauthoryear{Schneider}{Schneider}{1996}]{schneider96b}
154: Schneider, S. (1996).
155: \newblock {Security Properties and {CSP}}.
156: \newblock In {\em Proc.~1996 {IEEE} Symposium on Security and Privacy}, pp.\
157: 174--187.
158:
159: \bibitem[\protect\citeauthoryear{Schneider and Sidiropoulos}{Schneider and
160: Sidiropoulos}{1996}]{schneider96}
161: Schneider, S. and A.~Sidiropoulos (1996).
162: \newblock {CSP} and anonymity.
163: \newblock In {\em European Symposium on Research in Computer Security}, pp.\
164: 198--218.
165:
166: \bibitem[\protect\citeauthoryear{Serjantov and Danezis}{Serjantov and
167: Danezis}{2002}]{Serj02}
168: Serjantov, A. and G.~Danezis (2002).
169: \newblock Towards an information theoretic metric for anonymity.
170: \newblock In R.~Dingledine and P.~Syverson (Eds.), {\em Proc.~Privacy Enhancing
171: Technologies Workshop (PET 2002)}, Volume 2482 of {\em Lecture Notes in
172: Computer Science}, Berlin/New York, pp.\ 41--53. Springer-Verlag.
173:
174: \bibitem[\protect\citeauthoryear{Sherwood, Bhattacharjee, and
175: Srinivasan}{Sherwood et~al.}{2002}]{sherwood02}
176: Sherwood, R., B.~Bhattacharjee, and A.~Srinivasan (2002).
177: \newblock P5: A protocol for scalable anonymous communication.
178: \newblock In {\em {IEEE} Symposium on Security and Privacy}, pp.\ 58--70.
179:
180: \bibitem[\protect\citeauthoryear{Shmatikov}{Shmatikov}{2002}]{shmat02}
181: Shmatikov, V. (2002).
182: \newblock Probabilistic analysis of anonymity.
183: \newblock In {\em Proc.~15th Computer Security Foundations Workshop}, pp.\
184: 119--128.
185:
186: \bibitem[\protect\citeauthoryear{Syverson, Goldschlag, and Reed}{Syverson
187: et~al.}{1997}]{syverson97}
188: Syverson, P.~F., D.~M. Goldschlag, and M.~G. Reed (1997).
189: \newblock Anonymous connections and onion routing.
190: \newblock In {\em {IEEE} Symposium on Security and Privacy}, pp.\ 44--54.
191:
192: \bibitem[\protect\citeauthoryear{Syverson and Stubblebine}{Syverson and
193: Stubblebine}{1999}]{syverson99}
194: Syverson, P.~F. and S.~G. Stubblebine (1999).
195: \newblock Group principals and the formalization of anonymity.
196: \newblock In {\em World Congress on Formal Methods}, pp.\ 814--833.
197:
198: \bibitem[\protect\citeauthoryear{Thayer, Herzog, and Guttman}{Thayer
199: et~al.}{1999}]{FHG99}
200: Thayer, F.~J., J.~C. Herzog, and J.~D. Guttman (1999).
201: \newblock Strand spaces: Proving security protocols correct.
202: \newblock {\em Journal of Computer Security\/}~{\em 7\/}(2/3), 191--230.
203:
204: \bibitem[\protect\citeauthoryear{van~der Meyden}{van~der
205: Meyden}{1998}]{vandermeyden98}
206: van~der Meyden, R. (1998).
207: \newblock Common knowledge and update in finite environments.
208: \newblock {\em Information and Computation\/}~{\em 140\/}(2), 115--157.
209:
210: \bibitem[\protect\citeauthoryear{van~der Meyden and Su}{van~der Meyden and
211: Su}{2004}]{vandermeyden02}
212: van~der Meyden, R. and K.~Su (2004).
213: \newblock Symbolic model checking the knowledge of the dining cryptographers.
214: \newblock In {\em Proc.~17th IEEE Computer Security Foundations Workshop}.
215: \newblock To appear.
216:
217: \bibitem[\protect\citeauthoryear{von Ahn, Bortz, and Hopper}{von Ahn
218: et~al.}{2003}]{hopper03}
219: von Ahn, L., A.~Bortz, and N.~J. Hopper (2003).
220: \newblock $k$-anonymous message transmission.
221: \newblock In {\em 10th {ACM} Conference on Computer and Communications
222: Security}, pp.\ 122--130.
223:
224: \bibitem[\protect\citeauthoryear{Zdancewic and Myers}{Zdancewic and
225: Myers}{2001}]{zdancewic01}
226: Zdancewic, S. and A.~C. Myers (2001).
227: \newblock Robust declassification.
228: \newblock In {\em Proc.~14th IEEE Computer Security Foundations Workshop}, pp.\
229: 15--23.
230:
231: \end{thebibliography}
232: