Skip to main content
SpringerLink
Log in

Symbolic Model Checking the Knowledge in Herbivore Protocol

  • Conference paper
Model Checking and Artificial Intelligence (MoChArt 2010)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6572))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Goel, S., Robson, M., Polte, M., Sirer, E.G.: Herbivore: A Scalable and Efficient Protocol for Anonymous Communication. Technical Report TR2003-1890, Cornell Univeristy Computing and Information Science (2003)

    Google Scholar 

  2. Halpern, J., Vardi, M.Y.: Model Checking vs. Theorem Proving: A Manifesto. Technical Report, IBM Almaden Research Center(1991); An extended version of a paper in Proc. 2nd Int. Conf. on Principles of Knowledge Representation and Reasoning (1991)

    Google Scholar 

  3. van der Meyden, R.: Common Knowledge and Update in Finite Environments. Information and Computation 140(2), 115–157 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  4. Gammie, P., van der Meyden, R.: MCK: Model Checking the Logic of Knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  5. Lomuscio, A., Raimondi, F.: MCMAS: a Model Checker for Multi-Agent Systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  6. Su, K.: Model Checking Temporal Logics of Knowledge in Distributed Systems. In: Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, pp. 98–103. AAAI Press / The MIT Press (2004)

    Google Scholar 

  7. Su, K., Sattar, A., Luo, X.: Model Checking Temporal Logics of Knowledge Via OBDDs. The Computer Journal 50(4), 403–420 (2007)

    Article  Google Scholar 

  8. Engelhardt, K., van der Meyden, R., Moses, Y.: Knowledge and the Logic of Local Propositions. In: TARK 1998: Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge, pp. 29–41. Morgan Kaufmann Publishers Inc., San Francisco (1998)

    Google Scholar 

  9. Luo, X.: Symbolic Model Checking Multi-Agent Systems. Phd Thesis, School of Information Science and Technology, Sun Yat-sen University (2006) (in Chinese)

    Google Scholar 

  10. Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  11. Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning about Knowledge. MIT Press, Cambridge (1995)

    MATH  Google Scholar 

  12. Bryant, R.E.: Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys 24(3), 293–318 (1992)

    Article  MathSciNet  Google Scholar 

  13. Holzmann, G.: The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)

    Article  Google Scholar 

  14. Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  15. Lichtenstein, O., Pnueli, A.: Checking That Finite State Concurrent Programs Satisfy Their Linear Specification. In: POPL 1985: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 97–107. ACM Press, New York (1985)

    Google Scholar 

  16. Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another Look at LTL Model Checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 415–427. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  17. Chaum, D.: The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability. Journal of Cryptology 1, 65–75 (1988)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. College of Computer Science & Technology, Huaqiao University, Xiamen, China

    Xiangyu Luo

  2. School of Software, Tsinghua University, Beijing, China

    Xiangyu Luo & Ming Gu

  3. College of Mathmatics Physics and Information Engineering, Zhejiang Normal University, Jinhua, China

    Kaile Su

  4. Institute for Integrated and Intelligent Systems, Griffith University, Brisbane, Australia

    Kaile Su

  5. School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu, China

    Lijun Wu

  6. School of Computer, South China Normal University, Guangzhou, China

    Jinji Yang

Authors
  1. Xiangyu Luo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kaile Su
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ming Gu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Lijun Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Jinji Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science and Engineering, University of New South Wales, 2052, Sydney, Australia

    Ron van der Meyden

  2. Institut für Informatik, Albert-Ludwigs-Universität Freiburg, 79110, Freiburg, Germany

    Jan-Georg Smaus

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Luo, X., Su, K., Gu, M., Wu, L., Yang, J. (2011). Symbolic Model Checking the Knowledge in Herbivore Protocol. In: van der Meyden, R., Smaus, JG. (eds) Model Checking and Artificial Intelligence. MoChArt 2010. Lecture Notes in Computer Science(), vol 6572. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20674-0_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-20674-0_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-20673-3

  • Online ISBN: 978-3-642-20674-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation