[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Prototyping Formal Methods Tools: A Protocol Analysis Case Study

  • Chapter
  • First Online:
Protocols, Strands, and Logic

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 13066))

Abstract

Modern-day formal methods tools are more than just a core solver: they also need convenient languages, useful editors, usable visualizations, and often also scriptability. These are required to attract a community of users, to put ideas to work in practice, and to conduct evaluations of the formalisms and core technical ideas. Off-the-shelf solvers address one of these issues but not the others. How can full prototype environments be obtained quickly?

We have built Forge, a system for prototyping such environments. In this paper, we present a case-study to assess the utility of Forge. Concretely, we use Forge to build a basic protocol analyzer, inspired by the Cryptographic Protocol Shape Analyzer (cpsa). We show that we can obtain editing, basic visualization, and scriptability at no extra cost beyond embedding in Forge, and a modern, domain-specific visualization for relatively little extra effort.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 51.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 64.99
Price includes VAT (United Kingdom)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    Available at: www.forge-fm.org.

References

  1. Abbassi, A., Day, N.A., Rayside, D.: Astra version 1.0: evaluating translations from Alloy to SMT-LIB. CoRR abs/1906.05881 (2019). http://arxiv.org/abs/1906.05881

  2. Ball, T., Bounimova, E., Levin, V., Kumar, R., Lichtenberg, J.: The static driver verifier research platform. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 119–122. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_11

    Chapter  Google Scholar 

  3. Barwise, K.J., Allwein, G. (eds.): Logical Reasoning with Diagrams. Oxford University Press (1996)

    Google Scholar 

  4. Blanchet, B.: Modeling and verifying security protocols with the applied Pi calculus and ProVerif. Found. Trends Priv. Secur. 1(1–2), 1–135 (2016)

    Google Scholar 

  5. Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_11

    Chapter  Google Scholar 

  6. Bornholt, J., Torlak, E.: Synthesizing memory models from framework sketches and litmus tests. In: Programming Language Design and Implementation (PLDI) (2017)

    Google Scholar 

  7. Chudnov, A., et al.: Continuous formal verification of Amazon s2n. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 430–446. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_26

    Chapter  Google Scholar 

  8. Cook, B., Khazem, K., Kroening, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Model checking boot code from AWS data centers. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 467–486. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_28

    Chapter  Google Scholar 

  9. Cook, B., Podelski, A., Rybalchenko, A.: Terminator: beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_37

    Chapter  Google Scholar 

  10. Cunha, A., Macedo, N., Guimarães, T.: Target oriented relational model finding. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 17–31. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54804-8_2

    Chapter  Google Scholar 

  11. Danas, N., Nelson, T., Harrison, L., Krishnamurthi, S., Dougherty, D.J.: User studies of principled model finder output. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 168–184. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66197-1_11

    Chapter  Google Scholar 

  12. Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for shapes in cryptographic protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523–537. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_41

    Chapter  MATH  Google Scholar 

  13. Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theor. 29(2), 198–207 (1983). https://doi.org/10.1109/TIT.1983.1056650

    Article  MathSciNet  MATH  Google Scholar 

  14. Dougherty, D.J., Guttman, J.D., Ramsdell, J.D.: Security protocol analysis in context: computing minimal executions using SMT and CPSA. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 130–150. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98938-9_8

    Chapter  Google Scholar 

  15. Dyer, T., Baugh, J.: Sterling: a web-based visualizer for relational modeling languages. In: Raschke, A., Méry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 99–104. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-77543-8_7

    Chapter  Google Scholar 

  16. Felleisen, M., et al.: A programmable programming language. In: Communications of the ACM (2018)

    Google Scholar 

  17. Findler, R.B., et al.: DrScheme: a programming environment for Scheme. J. Funct. Program. 12(2), 159–182 (2002)

    Article  MathSciNet  Google Scholar 

  18. Fogel, A., et al.: A general approach to network configuration analysis. In: Networked Systems Design and Implementation, pp. 469–483 (2015). https://doi.org/10.5555/2789770.2789803

  19. Ghazi, A.A.E., Taghdiri, M.: Analyzing Alloy formulas using an SMT solver: a case study. CoRR abs/1505.00672 (2015). http://arxiv.org/abs/1505.00672

  20. Guttman, J.D.: Fair exchange in strand spaces. In: International Workshop on Security Issues in Concurrency, EPTCS, vol. 7, pp. 46–60 (2009). https://doi.org/10.4204/EPTCS.7.4

  21. Guttman, J.D., Ramsdell, J.D., Wand, M.: VLISP: a verified implementation of Scheme. LISP Symb. Comput. 8(1–2), 5–32 (1995)

    MATH  Google Scholar 

  22. Guttman, J.D., Thayer, F.J., Carlson, J.A., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Trust management in strand spaces: a rely-guarantee method. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 325–339. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24725-8_23

    Chapter  Google Scholar 

  23. Jackson, D.: Software Abstractions: Logic, Language, and Analysis, 2nd edn. MIT Press (2012). https://doi.org/10.5555/2141100

  24. Kobeissi, N., Nicolas, G., Tiwari, M.: Verifpal: cryptographic protocol analysis for the real world. In: Bhargavan, K., Oswald, E., Prabhakaran, M. (eds.) INDOCRYPT 2020. LNCS, vol. 12578, pp. 151–202. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-65277-7_8

    Chapter  Google Scholar 

  25. Liskov, M.D., Ramsdell, J.D., Guttman, J.D., Rowe, P.D.: The cryptographic protocol shapes analyzer: a manual. https://github.com/mitre/cpsa/blob/master/doc/cpsamanual.pdf. Accessed 6 Jun 2021

  26. Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Inf. Process. Lett. 56(3), 131–133 (1995). https://doi.org/10.1016/0020-0190(95)00144-2

    Article  MATH  Google Scholar 

  27. Macedo, N., Cunha, A., Guimarães, T.: Exploring scenario exploration. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 301–315. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46675-9_20

    Chapter  Google Scholar 

  28. Macedo, N., Guimarães, T., Cunha, A.: Model repair and transformation with Echo. In: Automated Software Engineering (2013). https://doi.org/10.1109/ASE.2013.6693135

  29. Marinov, D., Khurshid, S.: TestEra: a novel framework for automated testing of Java programs. In: Automated Software Engineering (2001). https://doi.org/10.1109/ASE.2001.989787

  30. McCormick, K.D., Cinelli, F.C.: Translating Alloy to SMT-LIB. Major qualifying project (b.s. thesis), Worcester Polytechnic Institute (2018)

    Google Scholar 

  31. Meng, B., Reynolds, A., Tinelli, C., Barrett, C.: Relational constraint solving in SMT. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 148–165. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_10

    Chapter  Google Scholar 

  32. Milicevic, A., Misailovic, S., Marinov, D., Khurshid, S.: Korat: a tool for generating structurally complex test inputs. In: International Conference on Software Engineering (2007)

    Google Scholar 

  33. Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: International Conference on Software Engineering (2015)

    Google Scholar 

  34. Montaghami, V., Rayside, D.: Bordeaux: a tool for thinking outside the box. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 22–39. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54494-5_2

    Chapter  Google Scholar 

  35. Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978). https://doi.org/10.1145/359657.359659

    Article  MATH  Google Scholar 

  36. Nelson, T., Ferguson, A.D., Scheer, M.J.G., Krishnamurthi, S.: Tierless programming and reasoning for software-defined networks. In: Networked Systems Design and Implementation (2014)

    Google Scholar 

  37. Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: International Conference on Software Engineering (2013)

    Google Scholar 

  38. Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: USENIX Large Installation System Administration Conference (2010)

    Google Scholar 

  39. Nelson, T., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Toward a more complete Alloy. In: Derrick, J., et al. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 136–149. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30885-7_10

    Chapter  Google Scholar 

  40. Neumerkel, U., Kral, S.: Declarative program development in prolog with GUPU. In: International Workshop on Logic Programming Environments, pp. 77–86 (2002)

    Google Scholar 

  41. Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How AWS uses formal methods. Commun. ACM 58(4), 66–73 (2015). https://doi.org/10.1145/2699417

    Article  Google Scholar 

  42. Porncharoenwase, S., Nelson, T., Krishnamurthi, S.: CompoSAT: specification-guided coverage for model finding. In: International Symposium on Formal Methods (FM) (2018)

    Google Scholar 

  43. Ptolemaeus, C. (ed.): System design, modeling, and simulation using Ptolemy II. Ptolemy.org (2014). http://ptolemy.org/books/Systems

  44. Rupakheti, C.R., Hou, D.: An abstraction-oriented, path-based approach for analyzing object equality in Java. In: Working Conference on Reverse Engineering (2010). https://doi.org/10.1109/WCRE.2010.30

  45. Saghafi, S., Danas, N., Dougherty, D.J.: Exploring theories with a model-finding assistant. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 434–449. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_30

    Chapter  Google Scholar 

  46. Sergey Bronnikov: Practical FM. https://github.com/ligurio/practical-fm. Accessed 23 Jan 2021

  47. Shimojima, A.: On the Efficacy of Representation. Ph.D. thesis. The Department of Philosophy, Indiana University (1996)

    Google Scholar 

  48. Sullivan, A., Wang, K., Zaeem, R.N., Khurshid, S.: Automated test generation and mutation testing for Alloy. In: Software Testing, Verification and Validation (ICST) (2017). https://doi.org/10.1109/ICST.2017.31

  49. Sullivan, A., Zaeem, R.N., Khurshid, S., Marinov, D.: Towards a test automation framework for Alloy. In: Symposium on Model Checking of Software (SPIN). pp. 113–116 (2014). https://doi.org/10.1145/2632362.2632369

  50. Tariq, Khadija: Linking Alloy with SMT-based Finite Model Finding. Master’s thesis, University of Waterloo (2021). http://hdl.handle.net/10012/16756

  51. Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. J. Comput. Secur. 7(1), 191–230 (1999)

    Article  Google Scholar 

  52. Torlak, E., Bodik, R.: Growing solver-aided languages with Rosette. In: Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software. SPLASH Onward! (2013)

    Google Scholar 

  53. Torlak, E., Bodik, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: Programming Language Design and Implementation (PLDI) (2014)

    Google Scholar 

  54. Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_49

    Chapter  Google Scholar 

Download references

Acknowledgments

We are grateful to Joshua Guttman for many enjoyable and productive conversations. We thank the creators of cpsa for their vision, the anonymous reviewers for their feedback, and the editors for putting together this much-deserved Festschrift. This work was partly supported by the US National Science Foundation. This research was also developed with funding from the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL). The views, opinions and/or findings expressed are those of the author and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.

Author information

Authors and Affiliations

  1. Computer Science Department, Brown University, Providence, RI, USA

    Abigail Siegel, Mia Santomauro, Tristan Dyer, Tim Nelson & Shriram Krishnamurthi

Authors
  1. Abigail Siegel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mia Santomauro
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tristan Dyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Tim Nelson
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Shriram Krishnamurthi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tim Nelson .

Editor information

Editors and Affiliations

  1. Department of Computer Science, Worcester Polytechnic Institute, Worcester, MA, USA

    Daniel Dougherty

  2. Th.M. Siebel Center for Computer Science, University of Illinois Urbana-Champaign, Urbana, IL, USA

    José Meseguer

  3. Institute of Mathematics and Computer Science, Technical University of Denmark, Kongens Lyngby, Denmark

    Sebastian Alexander Mödersheim

  4. J83K, The MITRE Corporation, Bedford, MA, USA

    Paul Rowe

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Siegel, A., Santomauro, M., Dyer, T., Nelson, T., Krishnamurthi, S. (2021). Prototyping Formal Methods Tools: A Protocol Analysis Case Study. In: Dougherty, D., Meseguer, J., Mödersheim, S.A., Rowe, P. (eds) Protocols, Strands, and Logic. Lecture Notes in Computer Science(), vol 13066. Springer, Cham. https://doi.org/10.1007/978-3-030-91631-2_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-91631-2_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-91630-5

  • Online ISBN: 978-3-030-91631-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation