Academic
Publications
Symbolic Model Checking the Knowledge in Herbivore Protocol

Symbolic Model Checking the Knowledge in Herbivore Protocol,10.1007/978-3-642-20674-0_8,Xiangyu Luo,Kaile Su,Ming Gu,Lijun Wu,Jinji Yang

Symbolic Model Checking the Knowledge in Herbivore Protocol   (Citations: 2)
BibTex | RIS | RefWorks Download
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.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: