Formal Support for Standardizing Protocols with State

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9497)


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.


Protocol analysis tools Stateful protocols TPM  PKCS #11 


  1. 1.
    Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. J. ACM 52(1), 102–146 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 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. 3.
    Arapinis, M., Ryan, M., Ritter, E.: StatVerif: verification of stateful processes. In: IEEE Symposium on Computer Security Foundations. IEEE CS Press, June 2011Google Scholar
  4. 4.
    Blanchet, B.: An efficient protocol verifier based on Prolog rules. In: 14th Computer Security Foundations Workshop, pp. 82–96. IEEE CS Press, June 2001Google Scholar
  5. 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) CrossRefGoogle Scholar
  6. 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) CrossRefGoogle Scholar
  7. 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)CrossRefGoogle Scholar
  8. 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. 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 2008Google Scholar
  10. 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) CrossRefGoogle Scholar
  11. 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 2011Google Scholar
  12. 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) CrossRefGoogle Scholar
  13. 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) CrossRefGoogle Scholar
  14. 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. 15.
    Guttman, J.D.: State and progress in strand spaces: proving fair exchange. J. Autom. reasoning 48(2), 159–195 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Guttman, J.D.: Establishing and preserving protocol security goals. J. Comput. Secur. 22(2), 201–267 (2014)CrossRefGoogle Scholar
  17. 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.
  18. 18.
    Herzog, J.: Applying protocol analysis to security device interfaces. IEEE Secur. Priv. 4(4), 84–87 (2006)CrossRefGoogle Scholar
  19. 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. 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) CrossRefGoogle Scholar
  21. 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. 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). Google Scholar
  23. 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. 24.
    Ramsdell, J.D., Guttman, J.D.: CPSA: A cryptographic protocol shapes analyzer (2009).
  25. 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.
  26. 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.
  27. 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)CrossRefGoogle Scholar
  28. 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).

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.The MITRE CorporationBedfordUSA

Personalised recommendations