Symbolic Model Checking the Knowledge in Herbivore Protocol

There are no files associated with this record.

Title Symbolic Model Checking the Knowledge in Herbivore Protocol
Author Luo, Xiangyu; Su, Kaile; Gu, Ming; Wu, Lijun; Yang, Jinji
Publication Title Model Checking and Artificial Intelligence - 6th International Workshop, MoChArt 2010
Editor R. van der Meyden and J.-G. Smaus
Year Published 2011
Place of publication Berlin, Germany
Publisher Springer-Verlag
Abstract The importance of anonymity has increased over the past few years in many applications. Herbivore is a distributed anonymous communication system, providing private file sharing and messaging over the Internet. In this paper, we utilize MCTK to model the round protocol of the Herbivore system and verify the anonymity and other knowledge properties that the protocol should provide, where MCTK is an OBDD-based symbolic model checker for temporal logic of knowledge developed by us, under the semantics of interpreted systems with local propositions. We model the round protocol of the Herbivore system in MCTK under the assumption that all agents have perfect recall of all observations. We implement the round protocol of the Herbivore system in MCTK and another epistemic model checker MCK. The encouraging experimental results show the validity of our MCTK.
Peer Reviewed Yes
Published Yes
Alternative URI http://dx.doi.org/10.1007/978-3-642-20674-0_8
ISBN 9783642206735
Conference name MoChArt 2010
Location Atlanta, United States
Date From 2010-07-11
Date To 2010-07-11
URI http://hdl.handle.net/10072/40030
Date Accessioned 2011-06-13
Date Available 2011-08-15T06:39:43Z
Language en_AU
Faculty Faculty of Science, Environment, Engineering and Technology
Subject Computational Logic and Formal Languages
Publication Type Conference Publications (Full Written Paper - Refereed)
Publication Type Code e1

Show simple item record

Griffith University copyright notice