Home // INTERNET 2012, The Fourth International Conference on Evolving Internet // View article

Formalizing and Verifying Anonymity of Crowds-based Communication Protocols with IOA

Authors:
Yoshinobu Kawabe

Keywords: anonymity; formal verification; Crowds; theorem-proving

Abstract:
Crowds is a communication protocol that guarantees sender's anonymity. As a case study, this paper provides a computer-assisted anonymity proof for Crowds. To prove anonymity, we first describe a simple specification of Crowds with an I/O-automaton-based formal specification language. Then, the specification is translated into first-order logic formulae with a formal verification tool. Finally, by showing the existence of an anonymous simulation, the anonymity of Crowds is proved. In this proof, a theorem proving tool is employed. Also, in this study, we formalize an extension of Crowds that guarantees the anonymity with regard to a recipient.

Pages: 108 to 113

Copyright: Copyright (c) IARIA, 2012

Publication date: June 24, 2012

Published in: conference

ISSN: 2308-443X

ISBN: 978-1-61208-204-2

Location: Venice, Italy

Dates: from June 24, 2012 to June 29, 2012