Advertisement

Security-Typed Languages for Implementation of Cryptographic Protocols: A Case Study

  • Aslan Askarov
  • Andrei Sabelfeld
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3679)

Abstract

Security protocols are critical for protecting modern communication infrastructures and are therefore subject to thorough analysis. However practical implementations of these protocols lack the same level of attention and thus may be more exposed to attacks. This paper discusses security assurance provided by security-typed languages when implementing cryptographic protocols. Our results are based on a case study using Jif, a Java-based security-typed language, for implementing a non-trivial cryptographic protocol that allows playing online poker without a trusted third party. The case study deploys the largest program written in a security-typed language to date and identifies insights ranging from security guarantees to useful patterns of secure programming.

Keywords

Security Level Trusted Third Party Cryptographic Protocol Homomorphic Encryption Covert Channel 
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.

References

  1. 1.
    CERT® advisory CA-2003-26: Multiple vulnerabilities in SSL/TLS implementations (October 2003), http://www.cert.org/advisories/CA-2003-26.html
  2. 2.
    Jif source code for the mental poker protocol (March 2005), http://www.cs.chalmers.se/~aaskarov/jifpoker
  3. 3.
    Agat, J.: Transforming out timing leaks. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 40–53 (January 2000)Google Scholar
  4. 4.
    Anderson, R.: Why cryptosystems fail. In: ACM Conference on Computer and Communications Security, pp. 215–227 (November 1993)Google Scholar
  5. 5.
    Banerjee, A., Naumann, D.A.: Secure information flow and pointer confinement in a Java-like language. In: Proc. IEEE Computer Security Foundations Workshop, pp. 253–267 (June 2002)Google Scholar
  6. 6.
    Barnett, A., Smart, N.P.: Mental poker revisited. In: Paterson, K.G. (ed.) Cryptography and Coding 2003. LNCS, vol. 2898, pp. 370–383. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Bauer, L., Ligatti, J., Walker, D.: Composing security policies with Polymer. In: Proc. ACM Conf. on Programming Language Design and Implementation (June 2005) (to appear)Google Scholar
  8. 8.
    Castellà-Roca, J., Domingo-Ferrer, J., Riera, A., Borrell, J.: Practical mental poker without a TTP based on homomorphic encryption. In: Johansson, T., Maitra, S. (eds.) INDOCRYPT 2003. LNCS, vol. 2904, pp. 280–294. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Chong, S., Myers, A.C.: Security policies for downgrading. In: ACM Conference on Computer and Communications Security, pp. 198–209 (October 2004)Google Scholar
  10. 10.
    Chong, S., Myers, A.C.: Language-based information erasure. In: Proc. IEEE Computer Security Foundations Workshop (June 2005) (to appear)Google Scholar
  11. 11.
    Cinnéide, M.Ó.: Automated refactoring to introduce design patterns. In: Proc. ACM International Conference on Software Engineering, pp. 722–724 (2000)Google Scholar
  12. 12.
    Crépeau, C.: A secure poker protocol that minimizes the effect of player coalitions. In: Williams, H.C. (ed.) CRYPTO 1985. LNCS, vol. 218, pp. 73–86. Springer, Heidelberg (1986)Google Scholar
  13. 13.
    Crépeau, C.: A zero-knowledge poker protocol that achieves confidentiality of the players’ strategy or how to achieve an electronic poker face. In: Odlyzko, A.M. (ed.) CRYPTO 1986. LNCS, vol. 263, pp. 239–247. Springer, Heidelberg (1987)Google Scholar
  14. 14.
    Dam, M., Giambiagi, P.: Confidentiality for mobile code: The case of a simple payment protocol. In: Proc. IEEE Computer Security Foundations Workshop, pp. 233–244 (July 2000)Google Scholar
  15. 15.
    Denning, D.E.: A lattice model of secure information flow. Comm. of the ACM 19(5), 236–243 (1976)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Comm. of the ACM 20(7), 504–513 (1977)zbMATHCrossRefGoogle Scholar
  17. 17.
    Domingo-Ferrer, J.: A new privacy homomorphism and applications. Information Processing Letters 60(5), 277–282 (1996)CrossRefMathSciNetGoogle Scholar
  18. 18.
    Edwards, J.: Implementing electronic poker: A practical exercise in zero-knowledge interactive proofs. Master’s thesis, Dept. of Computer Science, University of Kentucky (1994)Google Scholar
  19. 19.
    Focardi, R., Gorrieri, R.: Classification of security properties. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  20. 20.
    Giambiagi, P., Dam, M.: On the secure implementation of security protocols. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 144–158. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  21. 21.
    Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symp. on Security and Privacy, pp. 11–20 (April 1982)Google Scholar
  22. 22.
    Goldwasser, S., Micali, S.: Probabilistic encryption and how to play mental poker keeping secret all partial information. In: Proc. ACM Symp. Theory of Computing, pp. 365–377 (1982)Google Scholar
  23. 23.
    Gutmann, P.: Lessons learned in implementing and deploying crypto software. In: Proc. USENIX Security Symp., pp. 315–325 (August 2002)Google Scholar
  24. 24.
    Hanna, R., Rideout, A., Ziegler, D.: Secure peer-to-peer texas hold’em. Course project, MIT (2003), http://web.mit.edu/ardonite/6.857/
  25. 25.
    Heintze, N., Riecke, J.G.: The SLam calculus: programming with secrecy and integrity. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 365–377 (January 1998)Google Scholar
  26. 26.
    Heldal, R., Hultin, F.: Bridging model-based and language-based security. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 235–252. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  27. 27.
    Heldal, R., Schlager, S., Bende, J.: Supporting confidentiality in UML: A profile for the Decentralized Label Model. In: Proc. International Workshop on Critical Systems Development with UML, pp. 56–70 (2004)Google Scholar
  28. 28.
    Kurosawa, K., Katayama, K., Ogata, W.: Reshufflable and laziness tolerant mental card game protocol. IEICE Transactions E80-A(1), 72–78 (1997)Google Scholar
  29. 29.
    Kurosawa, K., Katayama, Y., Ogata, W., Tsujii, S.: General public key residue cryptosystems and mental poker protocols. In: Damgård, I.B. (ed.) EUROCRYPT 1990. LNCS, vol. 473, pp. 374–388. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  30. 30.
    Li, P., Zdancewic, S.: Downgrading policies and relaxed noninterference. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 158–170 (January 2005)Google Scholar
  31. 31.
    Li, P., Zdancewic, S.: Practical information-flow control in web-based information systems. In: Proc. IEEE Computer Security Foundations Workshop (June 2005) (to appear)Google Scholar
  32. 32.
    Mantel, H., Sands, D.: Controlled declassification based on intransitive noninterference. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 129–145. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  33. 33.
    Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 228–241 (January 1999)Google Scholar
  34. 34.
    Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: Proc. ACM Symp. on Operating System Principles, pp. 129–142 (October 1997)Google Scholar
  35. 35.
    Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification. In: Proc. IEEE Computer Security Foundations Workshop, pp. 172–186 (June 2004)Google Scholar
  36. 36.
    Myers, A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: Jif: Java information flow. Software release (July 2001-2004), Located at http://www.cs.cornell.edu/jif
  37. 37.
    Pottier, F., Simonet, V.: Information flow inference for ML. ACM TOPLAS 25(1), 117–158 (2003)CrossRefGoogle Scholar
  38. 38.
    Ryan, P.: Mathematical models of computer security. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 1–62. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  39. 39.
    Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21(1), 5–19 (2003)CrossRefGoogle Scholar
  40. 40.
    Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 174–191. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  41. 41.
    Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proc. IEEE Computer Security Foundations Workshop, pp. 200–214 (July 2000)Google Scholar
  42. 42.
    Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: Proc. IEEE Computer Security Foundations Workshop (June 2005) (to appear)Google Scholar
  43. 43.
    Schindelhauer, C.: A toolbox for mental card games (1998), http://citeseer.ist.psu.edu/schindelhauer98toolbox.html
  44. 44.
    Shamir, A., Rivest, R., Adleman, L.: Mental poker. Mathematical Gardner, 37–43 (1981)Google Scholar
  45. 45.
    Simonet, V.: The Flow Caml system. Software release. Located at (July 2003), http://cristal.inria.fr/~simonet/soft/flowcaml/
  46. 46.
    Tse, S., Washburn, G.: Cryptographic programming in Jif. Course project (2003), http://www.cis.upenn.edu/~stse/bank/main.pdf
  47. 47.
    Viega, J., McGraw, G.: Building Secure Software: How to Avoid Security Problems the Right Way. Addison-Wesley, Reading (2001)Google Scholar
  48. 48.
    Zdancewic, S.: Challenges for information-flow security. In: Proc. Programming Language Interference and Dependence (PLID) (August 2004)Google Scholar
  49. 49.
    Zdancewic, S., Zheng, L., Nystrom, N., Myers, A.C.: Untrusted hosts and confidentiality: Secure program partitioning. In: Proc. ACM Symp. on Operating System Principles, pp. 1–14 (October 2001)Google Scholar
  50. 50.
    Zheng, L., Chong, S., Myers, A.C., Zdancewic, S.: Using replication and partitioning to build secure distributed systems. In: Proc. IEEE Symp. on Security and Privacy, pp. 236–250 (May 2003)Google Scholar
  51. 51.
    Zheng, L., Myers, A.C.: End-to-end availability policies and noninterference. In: Proc. IEEE Computer Security Foundations Workshop (June 2005) (to appear)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Aslan Askarov
    • 1
  • Andrei Sabelfeld
    • 1
  1. 1.Dept. of Computer ScienceChalmers University of TechnologyGöteborgSweden

Personalised recommendations