A Hybrid Analysis for Security Protocols with State

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


Cryptographic protocols rely on message-passing to coordinate activity among principals. Many richly developed tools, based on well-understood foundations, are available for the design and analysis of pure message-passing protocols. However, in many protocols, a principal uses non-local, mutable state to coordinate its local sessions. Crosssession state poses difficulties for protocol analysis tools.

We provide a framework for modeling stateful protocols, and a hybrid analysis method. We leverage theorem-proving—specifically, PVS—for reasoning about computations over state. An “enrich-by-need” approach—embodied by CPSA—focuses on the message-passing part. The Envelope Protocol, due to Mark Ryan furnishes a case study.


Transition Relation Security Protocol Horn Clause Trusted Platform Module Security Goal 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. Journal of the ACM 52(1), 102–146 (2005)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Ables, K., Ryan, M.D.: Escrowed data and the digital envelope. In: Acquisti, A., Smith, S.W., Sadeghi, A.-R. (eds.) TRUST 2010. LNCS, vol. 6101, pp. 246–256. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  3. 3.
    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
  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 2001)Google 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.
    Cremers, C., Mauw, S.: Operational semantics and verification of security protocols. Springer (2012)Google Scholar
  8. 8.
    Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. Journal of Computer Security 13(3), 423–482 (2005)Google Scholar
  9. 9.
    Datta, A., Franklin, J., Garg, D., Kaynar, D.: A logic of secure systems and its application to trusted computing. In: 30th IEEE Symposium on Security and Privacy, pp. 221–236. IEEE (2009)Google 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 2011)Google 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.: State and progress in strand spaces: Proving fair exchange. Journal of Automated Reasoning 48(2), 159–195 (2012)CrossRefzbMATHMathSciNetGoogle Scholar
  15. 15.
    Guttman, J.D.: Establishing and preserving protocol security goals. Journal of Computer Security (2014)Google Scholar
  16. 16.
    Herzog, J.: Applying protocol analysis to security device interfaces. IEEE Security & Privacy 4(4), 84–87 (2006)CrossRefGoogle Scholar
  17. 17.
    Jacobs, B., Hasuo, I.: Semantics and logic for security protocols. Journal of Computer Security 17(6), 909–944 (2009)Google Scholar
  18. 18.
    Liskov, M.D., Rowe, P.D., Thayer, F.J.: Completeness of CPSA. Technical Report MTR110479, The MITRE Corporation (March 2011),
  19. 19.
    Meier, S., Cremers, C., Basin, D.: Efficient construction of machine-checked symbolic protocol security proofs. Journal of Computer Security 21(1), 41–87 (2013)Google Scholar
  20. 20.
    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
  21. 21.
    Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE). In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992), Google Scholar
  22. 22.
    Ramsdell, J.D.: Deducing security goals from shape analysis sentences. The MITRE Corporation (April 2012),
  23. 23.
    Ramsdell, J.D.: Proving security goals with shape analysis sentences. Technical Report MTR130488, The MITRE Corporation (September 2013),
  24. 24.
    Ramsdell, J.D., Guttman, J.D.: CPSA: A cryptographic protocol shapes analyzer (2009),
  25. 25.
    Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7(2/3), 191–230 (1999)Google Scholar
  26. 26.
    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 2014

Authors and Affiliations

  1. 1.The MITRE Corporation and Worcester Polytechnic InstituteWorcesterUSA

Personalised recommendations