Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Verification, Model Checking, and Abstract Interpretation

VMCAI 2003: Verification, Model Checking, and Abstract Interpretation pp 116–131Cite as

A Logical Encoding of the π-Calculus: Model Checking Mobile Processes Using Tabled Resolution

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2575))

Abstract

We present MMC, a model checker for mobile systems speci fied in the style of the π-calculus. MMC’s development builds on our experience gained in developing XMC, a model checker for an extension of Milner’s value-passing calculus implemented using the XSB tabled logic-programming system. MMC, however, is not simply an extension of XMC; rather it is virtually a complete re-implementation that addresses the salient issues that arise in the π-calculus, including scope extrusion and intrusion, and dynamic generation of new names to avoid name capture. We show that tabled logic programming is especially suitable as an efficient implementation platform for model checking π-calculus specications, and can be used to obtain an exact encoding of the π-calculus’s transitional semantics. Moreover, MMC is easily extended to handle process expressions in the spi-calculus. Our experimental data shows that MMC outperforms other known tools for model checking the π-calculus.

This work was supported in part by NSF grants EIA-9705998, CCR-9876242, CCR-9988155, and CCR-0205376; ONR grant N000140110967; and ARO grants DAAD190110003, DAAD190110019.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Mobility model checker for the π-calculus. Dept. of Computer Science, SUNY at Stony Brook, 2002. Available from http://www.cs.sunysb.edu/~lmc/mmc.

  2. M. Abadi and B. Blanchet. Analyzing security protocols with secrecy types and logic programs. In Proceedings of POPL’02, pages 33–44, Jan. 2002.

    Google Scholar 

  3. M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spicalculus. In Fourth ACM Conference on CCS, pages 36–47. ACM Press, 1997.

    Google Scholar 

  4. B. Aziz and G.W. Hamilton. A privacy analysis for the pi-calculus: The denotational approach. In Proceedings of the 2nd Workshop on the Specification, Analysis and Validation for Emerging Technologies, Copenhagen, Denmark, July 2002.

    Google Scholar 

  5. S. Basu, M. Mukund, C. R. Ramakrishnan, I. V. Ramakrishnan, and R. M. Verma. Local and symbolic bisimulation using tabled constraint logic programming. In International Conference on Logic Programming, pages 166–180, 2001.

    Google Scholar 

  6. F. B. Beste. The model prover — a sequent-calculus based modal μ-calculus model checker tool for finite control π-calculus agents. Technical report, Swedish Institute of Computer Science, 1998.

    Google Scholar 

  7. B. Blanchet. From secrecy to authenticity in security protocols. In 9th International Static Analysis Symposium, pages 242–259, September 2002.

    Google Scholar 

  8. M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada. Maude: Specification and programming in rewriting logic. Theoretical Computer Science, 2001.

    Google Scholar 

  9. B. Cui and D. S. Warren. A system for tabled constraint logic programming. In First International Conference on Computational Logic, pages 478–492, 2000.

    Google Scholar 

  10. M. Dam. Proof systems for pi-calculus logics. Logic for Concurrency and Synchronisation, 2001.

    Google Scholar 

  11. G. Denker and J. Meseguer. Protocol specification and analysis in Maude. In Proc. of Workshop on Formal Methods and Security Protocols, June 1998.

    Google Scholar 

  12. Y. Dong and C.R. Ramakrishnan. An optimizing compiler for efficient model checking. In Proceedings of FORTE/PSTV’ 99, 1999.

    Google Scholar 

  13. F. Duran, S. Eker, P. Lincoln, and J. Meseguer. Principles of mobile maude. In Proc. ASA/MA, volume 1882, pages 73–85. Springer-Verlag, 2000.

    Google Scholar 

  14. T. Franzen. A theorem-proving approach to deciding properties of finite-control agents. Technical report, Swedish Institute of Computer Science, 1996.

    Google Scholar 

  15. A. Gordon and A.S.A. Jeffrey. Authenticity by typing for security protocols. In IEEE Computer Security Foundations Workshop, 2001.

    Google Scholar 

  16. H. Lin. Symbolic bisimulation and proof systems for the π-calculus. Technical report, School of Cognitive and Computer Science, U. of Sussex, UK, 1994.

    Google Scholar 

  17. G. Lowe. An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters, pages 131–133, 1995.

    Google Scholar 

  18. G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software Concepts and Tools, 17:93–102, 1996.

    Google Scholar 

  19. C. Meadows. The NRL protocol analyzer: an overview. Journal of Logic Programming, 26(2):113–131, 1996.

    Article  MATH  Google Scholar 

  20. R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.

    Google Scholar 

  21. R. Milner. The polyadic π-calculus: a tutorial. The Proceedings of the International Summer School on Logic and Algebra of Specification, 1991.

    Google Scholar 

  22. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Parts I and II. Information and Computation, 100(1):1–77, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  23. R. Milner, J. Parrow, and D. Walker. Modal logics for mobile processes. Theoretical Computer Science, pages 149–171, 1993.

    Google Scholar 

  24. F. Orava and J. Parrow. An algebraic verification of a mobile network. Formal Aspects of Computing, 4:497–543, 1992.

    Article  MATH  Google Scholar 

  25. J. Parrow. An introduction to the π-calculus. In Bergstra, Ponse, and Smolka, editors, Handbook of Process Algebra. Elsevier, 20

    Google Scholar 

  26. Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. W. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In Proceedings of CAV’ 97, Haifa, Israel, July 1997.

    Google Scholar 

  27. A. Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, I.V. Ramakrishnan, and S.A. Smolka. Verification of parameterized systems using logic-program transformations. In Proceedings of TACAS 2000, 2000.

    Google Scholar 

  28. C. Stirling and D. Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, pages 161–177, 1991.

    Google Scholar 

  29. P. Thati, K. Sen, and N. Marti-oliet. An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0. In Intl. Workshop on Rewriting Logic and its Applications, 2002.

    Google Scholar 

  30. B. Victor. The mobility workbench user’s guide. Technical report, Department of Computer Systems, Uppsala University, Sweden, 1995.

    Google Scholar 

  31. B. Victor and F. Moller. The mobility workbench-a tool for the π-calculus. In D. Dill, editor, Proceedings of CAV’94. Springer-Verlag, 1994.

    Google Scholar 

  32. XSB. The XSB logic programming system v2.4, 2001. Available from http://xsb.sourceforge.net.

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, State University of New York at Stony Brook, Stony Brook, NY, 11794-4400, USA

    Ping Yang, C.R. Ramakrishnan & Scott A. Smolka

Authors
  1. Ping Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. C.R. Ramakrishnan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Scott A. Smolka
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, New York University, 715 Broadway (7th floor), NY 10003, NewYork, USA

    Lenore D. Zuck

  2. College of Computer Science, Northeastern University, 360 Huntington Ave., 02115, Boston, MA, USA

    Paul C. Attie

  3. Computer Science Department, Venice University C’Foscari, Via Torino 155, 30170, Mestre-Venezia, Italy

    Agostino Cortesi

  4. Department of Computer Science and Electrical Engineering, West Virginia University, 26505, Morgantown, WV, USA

    Supratik Mukhopadhyay

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Yang, P., Ramakrishnan, C., Smolka, S.A. (2003). A Logical Encoding of the π-Calculus: Model Checking Mobile Processes Using Tabled Resolution. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2003. Lecture Notes in Computer Science, vol 2575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36384-X_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-36384-X_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00348-9

  • Online ISBN: 978-3-540-36384-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation