Skip to main content
SpringerLink
Log in
Book cover

International Conference on Research in Security Standardisation

SSR 2015: Security Standardisation Research pp 246–265Cite as

Formal Support for Standardizing Protocols with State

  • Conference paper
  • First Online:

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

Abstract

Many cryptographic protocols are designed to achieve their goals using only messages passed over an open network. Numerous tools, based on well-understood foundations, exist for the design and analysis of protocols that rely purely on message passing. However, these tools encounter difficulties when faced with protocols that rely on non-local, mutable state to coordinate several local sessions.

We adapt one of these tools, cpsa, to provide automated support for reasoning about state. We use Ryan’s Envelope Protocol as an example to demonstrate how the message-passing reasoning can be integrated with state reasoning to yield interesting and powerful results.

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 EPUB and 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

References

  1. Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. J. ACM 52(1), 102–146 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  2. Arapinis, M., Ritter, E., Ryan, M.D.: Statverif: verification of stateful processes. In: Computer Security Foundations Symposium (CSF), pp. 33–47. IEEE (2011)

    Google Scholar 

  3. Arapinis, M., Ryan, M., Ritter, E.: StatVerif: verification of stateful processes. In: IEEE Symposium on Computer Security Foundations. IEEE CS Press, June 2011

    Google Scholar 

  4. Blanchet, B.: An efficient protocol verifier based on Prolog rules. In: 14th Computer Security Foundations Workshop, pp. 82–96. IEEE CS Press, June 2001

    Google Scholar 

  5. Cortier, V., Keighren, G., Steel, G.: Automatic analysis of the security of XOR-based key management schemes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 538–552. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Cortier, V., Steel, G.: A generic security API for symmetric key management on cryptographic devices. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 605–620. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  7. Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. J. Comput. Secur. 13(3), 423–482 (2005)

    Article  Google Scholar 

  8. Datta, A., Franklin, J., Garg, D., Kaynar, D.: A logic of secure systems and its application to trusted computing. In: 2009 30th IEEE Symposium on Security and Privacy, pp. 221–236. IEEE (2009)

    Google Scholar 

  9. Delaune, S., Kremer, S., Ryan, M.D.: Composition of password-based protocols. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF’08), pp. 239–251. IEEE Computer Society Press, June 2008

    Google Scholar 

  10. Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: A formal analysis of authentication in the TPM. In: Degano, P., Etalle, S., Guttman, J. (eds.) FAST 2010. LNCS, vol. 6561, pp. 111–125. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: Formal analysis of protocols based on TPM state registers. In: IEEE Symposium on Computer Security Foundations. IEEE CS Press, June 2011

    Google Scholar 

  12. Fröschle, S., Sommer, N.: Reasoning with past to prove PKCS#11 keys secure. In: Degano, P., Etalle, S., Guttman, J. (eds.) FAST 2010. LNCS, vol. 6561, pp. 96–110. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Gürgens, S., Rudolph, C., Scheuermann, D., Atts, M., Plaga, R.: Security evaluation of scenarios based on the TCG’s TPM specification. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 438–453. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Guttman, J.D.: Shapes: surveying crypto protocol runs. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols, Cryptology and Information Security Series. IOS Press (2011)

    Google Scholar 

  15. Guttman, J.D.: State and progress in strand spaces: proving fair exchange. J. Autom. reasoning 48(2), 159–195 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  16. Guttman, J.D.: Establishing and preserving protocol security goals. J. Comput. Secur. 22(2), 201–267 (2014)

    Article  Google Scholar 

  17. Guttman, J.D., Liskov, M.D., Ramsdell, J.D., Rowe, P.D.: Formal support for standardizing protocols with state (extended version). Arxiv, September 2015. http://arxiv.org/abs/1509.07552

  18. Herzog, J.: Applying protocol analysis to security device interfaces. IEEE Secur. Priv. 4(4), 84–87 (2006)

    Article  Google Scholar 

  19. Kremer, S., Künnemann, R.: Automated analysis of security protocols with global state. In: IEEE Symposium on Security and Privacy, pp. 163–178 (2014)

    Google Scholar 

  20. Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  21. Mödersheim, S.: Abstraction by set-membership: verifying security protocols and web services with databases. In: ACM Conference on Computer and Communications Security, pp. 351–360 (2010)

    Google Scholar 

  22. Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). http://pvs.csl.sri.com

    Google Scholar 

  23. Ramsdell, J.D., Dougherty, D.J., Guttman, J.D., Rowe, P.D.: A hybrid analysis for security protocols with state. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 272–287. Springer, Heidelberg (2014)

    Google Scholar 

  24. Ramsdell, J.D., Guttman, J.D.: CPSA: A cryptographic protocol shapes analyzer (2009). http://hackage.haskell.org/package/cpsa

  25. Ramsdell, J.D., Guttman, J.D., Millen, J.K., O’Hanlon, B.: An analysis of the CAVES attestation protocol using CPSA. MITRE Technical report MTR090213, The MITRE Corporation, December 2009. http://arxiv.org/abs/1207.0418

  26. Rowe, P.D., Guttman, J.D., Liskov, M.D.: Measuring protocol strength with security goals. Submitted to IJIS in the SSR 2014 special issue, April 2015. http://web.cs.wpi.edu/~guttman/pubs/ijis_measuring-security.pdf

  27. Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7(2/3), 191–230 (1999)

    Article  Google Scholar 

  28. Youn, P., Adida, B., Bond, M., Clulow, J., Herzog, J., Lin, A., Rivest, R., Anderson, R.: Robbing the bank with a theorem prover. In: Security Protocols Workshop (2007). http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-644.pdf

Download references

Author information

Authors and Affiliations

  1. The MITRE Corporation, Bedford, MA, USA

    Joshua D. Guttman, Moses D. Liskov, John D. Ramsdell & Paul D. Rowe

Authors
  1. Joshua D. Guttman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Moses D. Liskov
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. John D. Ramsdell
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Paul D. Rowe
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Moses D. Liskov .

Editor information

Editors and Affiliations

  1. Hewlett Packard Laboratories, Bristol, United Kingdom

    Liqun Chen

  2. NICT, Tokyo, Japan

    Shin'ichiro Matsuo

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Guttman, J.D., Liskov, M.D., Ramsdell, J.D., Rowe, P.D. (2015). Formal Support for Standardizing Protocols with State. In: Chen, L., Matsuo, S. (eds) Security Standardisation Research. SSR 2015. Lecture Notes in Computer Science(), vol 9497. Springer, Cham. https://doi.org/10.1007/978-3-319-27152-1_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-27152-1_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-27151-4

  • Online ISBN: 978-3-319-27152-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation