Programming Cryptographic Protocols

  • Joshua D. Guttman
  • Jonathan C. Herzog
  • John D. Ramsdell
  • Brian T. Sniffen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3705)


Cryptographic protocols are useful for trust engineering in distributed transactions. Transactions require specific degrees of confidentiality and agreement between the principals engaging in it. Moreover, trust management assertions may be attached to protocol actions, constraining the behavior of a principal to be compatible with its own trust policy. We embody these ideas in a cryptographic protocol programming language cppl at the Dolev-Yao level of abstraction. A strand space semantics for cppl shaped our compiler development, and allows a protocol designer to prove that a protocol is sound.


Security Protocol Trust Management Cryptographic Protocol Runtime Environment Incoming Message 
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.


  1. 1.
    Abadi, M., Blanchet, B., Fournet, C.: Just Fast Keying in the pi calculus. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 340–354. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  2. 2.
    Abadi, M., Burrows, M., Lampson, B., Plotkin, G.D.: A calculus for access control in distributed systems. ACM Transactions on Programming Languages and Systems 15(4), 706–734 (1993)CrossRefGoogle Scholar
  3. 3.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th ACM Symposium on Principles of Programming Languages (POPL 2001), January 2001, pp. 104–115 (2001)Google Scholar
  4. 4.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148(1), 1–70 (1999)CrossRefzbMATHMathSciNetGoogle Scholar
  5. 5.
    Appel, A.W., Felten, E.W.: Proof-carrying authentication. In: 6th ACM Conference on Computer and Communications Security (November 1999)Google Scholar
  6. 6.
    Blanchet, B., Podelski, A.: Verification of cryptographic protocols: Tagging enforces termination. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 136–152. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Blaze, M., Feigenbaum, J., Lacy, J.: Distributed trust management. In: Proceedings, 1996 IEEE Symposium on Security and Privacy, May 1997, pp. 164–173 (1997)Google Scholar
  8. 8.
    Boreale, M.: Symbolic trace analysis of cryptographic protocols. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, p. 667. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  9. 9.
    Broadfoot, P., Lowe, G.: On distributed security transactions that use secure transport protocols. In: Proceedings, 16th Computer Security Foundations Workshop, pp. 63–73. IEEE Computer Society Press, Los Alamitos (2003)Google Scholar
  10. 10.
    Ceri, S., Gottlob, G., Tanca, L.: What you always wanted to know about datalog (and never dared to ask). IEEE Transactions of Knowledge and Data Engineering 1(1) (1989)Google Scholar
  11. 11.
    Chen, W., Swift, T., Warren, D.S.: Efficient top-down computation of queries under the well-founded semantics. J. Logic Prog. 24(3), 161–199 (1995)CrossRefzbMATHMathSciNetGoogle Scholar
  12. 12.
    Chen, W., Warren, D.S.: Tabled evaluation with delaying for general logic programs. J. ACM 43(1), 20–74 (1996)CrossRefzbMATHMathSciNetGoogle Scholar
  13. 13.
    Crazzolara, F., Milicia, G.: Developing security protocols in χ-spaces. In: Proceedings, 7th Nordic Workshop on Secure IT Systems, Karlstad, Sweden (November 2002)Google Scholar
  14. 14.
    Crazzolara, F., Winskel, G.: Composing strand spaces. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 97–108. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  15. 15.
    Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Transactions on Information Theory 29, 198–208 (1983)CrossRefzbMATHMathSciNetGoogle Scholar
  16. 16.
    Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security 12(2), 247–311 (2004); Initial version appeared in Workshop on Formal Methods and Security Protocols (1999)Google Scholar
  17. 17.
    Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 141–156. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  18. 18.
    Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. In: Proceedings, 15th Computer Security Foundations Workshop, June 2002. IEEE Computer Society Press, Los Alamitos (2002)Google Scholar
  19. 19.
    Guttman, J.D.: Key compromise and the authentication tests. In: Mislove, M. (ed.) Electronic Notes in Theoretical Computer Science, vol. 47, p. 21 (2001),
  20. 20.
    Guttman, J.D., Thayer, F.J.: Protocol independence through disjoint encryption. In: Proceedings, 13th Computer Security Foundations Workshop, July 2000. IEEE Computer Society Press, Los Alamitos (2000)Google Scholar
  21. 21.
    Guttman, J.D., Thayer, F.J.: Authentication tests and the structure of bundles. Theoretical Computer Science 283, 333–380 (2002)CrossRefzbMATHMathSciNetGoogle Scholar
  22. 22.
    Guttman, J.D., Thayer, F.J.: The sizes of skeletons: Decidable cryptographic protocol authentication and secrecy goals. MTR 05B09 Revision 1, The MITRE Corporation (March 2005)Google Scholar
  23. 23.
    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)CrossRefGoogle Scholar
  24. 24.
    Kaufman, C., (ed.): Internet key exchange (IKEv2) protocol. Internet Draft (September 2004), Available at
  25. 25.
    Lampson, B., Abadi, M., Burrows, M., Wobber, E.: Authentication in distributed systems: Theory and practice. ACM Transactions on Computer Systems 10(4), 265–310 (1992)CrossRefGoogle Scholar
  26. 26.
    Leroy, X.: Cryptokit. Sofwtare available via Version 1.3 (April 2005),
  27. 27.
    Leroy, X., Doligez, D., Garrigue, J., Rémy, D., Vouillon, J.: The Objective Caml System. INRIA Version 3.00 (2000),
  28. 28.
    Li, N., Mitchell, J.C., Winsborough, W.H.: Design of a role-based trust management framework. In: Proceedings, 2002 IEEE Symposium on Security and Privacy, pp. 114–130. IEEE Computer Society Press, Los Alamitos (2002)Google Scholar
  29. 29.
    Lowe, G.: An attack on the Needham-Schroeder public key authentication protocol. Information Processing Letters 56(3), 131–136 (1995)CrossRefzbMATHGoogle Scholar
  30. 30.
    Lowe, G.: A hierarchy of authentication specifications. In: 10th Computer Security Foundations Workshop Proceedings, pp. 31–43. IEEE Computer Society Press, Los Alamitos (1997)CrossRefGoogle Scholar
  31. 31.
    Millen, J., Muller, F.: Cryptographic protocol generation from CAPSL. Technical Report SRI-CSL-01-07, SRI International (December 2001)Google Scholar
  32. 32.
    Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12) (December 1978)Google Scholar
  33. 33.
    Perrig, A., Song, D.X.: A first step toward the automatic generation of security protocols. In: Network and Distributed System Security Symposium, February 2000. Internet Society (2000)Google Scholar
  34. 34.
    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
  35. 35.
    Trusted Computing Group TCG Specification Architecture Overview, revision 1.2 edition (April 2004),
  36. 36.
    Trusted Computing Group TPM Main: Part I Design Principles, specification version 1.2, revision 85 edn. (February 2005),
  37. 37.
    Woo, T.Y.C., Lam, S.S.: Authentication for distributed systems. Computer 25(1), 39–52 (1992)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Joshua D. Guttman
    • 1
  • Jonathan C. Herzog
    • 1
  • John D. Ramsdell
    • 1
  • Brian T. Sniffen
    • 1
  1. 1.The MITRE CorporationUSA

Personalised recommendations