Most applications in the Internet such as e-banking and e-commerce use the SET and the NSL protocols to protect the communication channel between the client and the server. Then, it is crucial to ensure that these protocols respect some security properties such as confidentiality, authentication, and integrity. In this paper, we analyze the SET and the NSL protocols with respect to the confidentiality (secrecy) property. To perform this analysis, we use the interpretation functions-based method. The main idea behind the interpretation functions-based technique is to give sufficient conditions that allow to guarantee that a cryptographic protocol respects the secrecy property. The flexibility of the proposed conditions allows the verification of daily-life protocols such as SET and NSL. Also, this method could be used under different assumptions such as a variety of intruder abilities including algebraic properties of cryptographic primitives. The NSL protocol, for instance, is analyzed with and without the homomorphism property. We show also, using the SET protocol, the usefulness of this approach to correct weaknesses and problems discovered during the analysis. 1. Motivations and Background Intuitively, cryptographic protocols are communication protocols that involve cryptography to reach some specific security goals (authentication, secrecy, etc.). Today, these protocols are playing a key role in our daily life. Among others, they protect our banking transactions (e-commerce protocol), our access to private wired and wireless network, and our access to a variety of indispensable services (web, FTP, e-mail, etc.). Obviously, any flaws in such protocols can have heavy negative consequences on individuals and organizations. It is also a well-known fact that attacks exploiting cryptographic protocols flaws are generally very difficult to detect: tools such as intrusion detections and firewalls are helpless against them since it is difficult (even impossible some-times) to distinguish between legitimate and illegitimate users when the cryptographic protocol is flawed. Like any sensitive system, cryptographic protocols need to be seriously studied and their correctness should be rigorously analyzed and ideally proved. For that reason, formal specification and verification of security protocols have received much attention in recent years. Some of these works including comparative studies could be found in [1–10]. Today and after more of thirty years of hard work, international community has a better understanding of cryptographic protocols and better
References
[1]
M. J. Banks and J. L. Jacob, “Unifying theories of confidentiality,” in Proceedings of the International Symposium on Unifying Theories of Programming (UTP '10), vol. 6445 of Lecture Notes in Computer Science, pp. 120–136, 2010.
[2]
V. Cortier, S. Delaune, and P. Lafourcade, “A survey of algebraic properties used in cryptographic protocols,” Journal of Computer Security, vol. 14, no. 1, pp. 1–43, 2006.
[3]
V. Cortier, S. Kremer, and B. Warinschi, “A survey of symbolic methods in computational analysis of cryptographic systems,” Journal of Automated Reasoning, vol. 46, no. 3-4, pp. 225–259, 2011.
[4]
S. Escobar, C. Meadows, and J. Meseguer, “A rewriting-based inference system for the NRL protocol analyzer: grammar generation,” in Proceedings of the ACM Workshop on Formal Methods in Security Engineering (FMSE '05), pp. 1–12, ACM, New York, NY, USA, November 2005.
[5]
J. Feigenbaum, A. Johnson, and P. Syverson, “Probabilistic analysis of onion routing in a black-box model,” in Proceedings of the 6th ACM Workshop on Privacy in the Electronic Society (WPES '07), pp. 1–10, October 2007.
[6]
P. Lafourcade, V. Terrade, and S. Vigier, “Comparison of cryptographic verification tools dealing with algebraic properties,” in Proceedings of the 6th international conference on Formal Aspects in Security and Trust (FAST '09), pp. 173–185, Springer, Berlin, Germany, 2010.
[7]
C. Meadows, “What makes a cryptographic protocol secure?” in Proceedings of the European Symposium on Programming (ESOP '03), Springer, April 2003.
[8]
“Security and trust management,” in Proceedings of the 7th International Workshop (STM '11), C. Meadows, M. Carmen, and F. Gago, Eds., vol. 7170 of Lecture Notes in Computer Science, Springer, Copenhagen, Denmark, June 2011.
[9]
A. Sabelfeld and A. C. Myers, “Language-based information-flow security,” IEEE Journal on Selected Areas in Communications, vol. 21, no. 1, pp. 5–19, 2003.
[10]
A. Sinha, “A survey of system security in contactless electronic passports,” Journal of Computer Security, vol. 19, no. 1, pp. 203–206, 2011.
[11]
D. Dolev, S. Even, and R. M. Karp, “On the security of ping-pong protocols,” Information and Control, vol. 55, no. 1–3, pp. 57–68, 1982.
[12]
R. M. Amadio, D. Lugiez, and V. Vanackère, “On the symbolic reduction of processes with cryptographic functions,” Theoretical Computer Science, vol. 290, no. 1, pp. 695–740, 2003.
[13]
B. Blanchet, “An efficient cryptographic protocol verifier based on prolog rules,” in Proceedings of the 14th IEEE Workshop on Computer Security Foundations (CSFW '01), pp. 82–96, Novia Scotia, Canada, June 2001.
[14]
H. Comon-Lundh, F. Jacquemard, and N. Perrin, “Tree automata with one memory, set constraints, and ping-pong protocols,” in Proceedings of the 8th International Conference on Automata, Languages and Programming (ICALP '07), vol. 2076 of Lecture Notes in Computer Science, pp. 682–695, 2007.
[15]
H. Comon-Lundh and V. Shmatikov, “Intruder deductions, constraint solving and insecurity decision in presence of exclusive or,” in Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS '03), pp. 271–280, June 2003.
[16]
N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov, “Undecidability of bounded security protocols,” in Proceedings of the Workshop on Formal Methods and Security Protocols (FMSP '99), N. Heintze and E. Clarke, Eds., Trento, Italy, July 1999.
[17]
M. Fiore and M. Abadi, “Computing symbolic models for verifying cryptographic protocols,” in Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW '14), pp. 160–173, June 2001.
[18]
D. Kindred, Theory generation for security protocols, 1999.
[19]
G. Lowe, “Towards a completeness result for model checking of security protocols,” in Proceedings of the 11th IEEE Computer Security Foundations Workshop (CSFW '98), pp. 96–105, June 1998.
[20]
J. Millen and V. Shmatikov, “Constraint solving for bounded-process cryptographic protocol analysis,” in Proceedings of the 8th ACM Conference on Computer and Communications Security (CCS '01), pp. 166–175, November 2001.
[21]
M. Rusinowitch and M. Turuani, “Protocol insecurity with a finite number of sessions and composed keys is NP-complete,” Theoretical Computer Science, vol. 299, no. 1–3, pp. 451–475, 2003.
[22]
S. D. Stoller, “A bound on attacks on payment protocols,” in Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01), pp. 61–70, June 2001.
[23]
Y. Chevalier, R. Küsters, M. Rusinowitch, M. Turuani, and L. Vigneron, “Extending the Dolev-Yao intruder for analyzing an unbounded number of sessions,” vol. 2803, pp. 128–141.
[24]
L. C. Paulson, “Mechanized proofs for a recursive authentication protocol,” in Proceedings of the 10th IEEE Computr Security Foundations Workshop (CSFW '97), pp. 84–94, June 1997.
[25]
H. Houmani and M. Mejri, “Analysis of some famous cryptographic protocols using the interpretation-function-based method,” International Journal of Security and Its Applications, vol. 2, no. 4, pp. 99–116, 2008.
[26]
H. Houmani and M. Mejri, “Ensuring the correctness of cryptographic protocols with respect to secrecy,” in Proceedings of the International Conference on Security and Cryptography (SECRYPT '08), pp. 184–189, INSTICC Press, Porto, Portugal, July 2008.
R. M. Needham and M. D. Schroeder, “Using encryption for authentication in large networks of computers,” Communications of the ACM, vol. 21, no. 12, pp. 993–999, 1978.
[31]
R. Delicata and S. Schneider, “Temporal rank functions for forward secrecy,” in Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW '05), pp. 126–139, Washington, DC, USA, June 2005.
[32]
S. Schneider, “Verifying authentication protocols in CSP,” IEEE Transactions on Software Engineering, vol. 24, no. 9, pp. 741–758, 1998.
[33]
M. Abadi, “Secrecy by typing in security protocols,” Journal of the ACM, vol. 46, no. 5, pp. 749–786, 1999.
[34]
H. Houmani and M. Mejri, “Secrecy by interpretation functions,” Knowledge-Based Systems, vol. 20, no. 7, pp. 617–635, 2007.
[35]
B. Dutertre and S. Schneider, “Using a pvs embedding of csp to verify authentication protocols,” in Proceedings of the Theorem Proving in Higher Order Logics (TPHOL's '97), pp. 121–136, Springer, 1997.
[36]
D. E. Bell and L. J. La Padula, Secure Computer Systems: Mathematical Foundations, vol. I, The MITRE Corporation, 1973.
[37]
T. Y. C. Woo and S. S. Lam, “A lesson on authentication protocol design,” Operating Systems Review, pp. 24–37, 1994.
[38]
M. Debbabi, M. Mejri, N. Tawbi, and I. Yahmadi, “From protocol specifications to flaws and attack scenarios: an automatic and formal algorithm,” in Proceedings of the 2nd International Workshop on Enterprise Security, Massachusetts Institute of Technology (MIT), IEEE Press, Cambridge, Mass, USA, June 1997.
[39]
M. Debbabi, N. A. Durgin, M. Mejri, and J. C. Mitchell, “Security by typing,” International Journal on Software Tools for Technology Transfer, vol. 4, no. 4, pp. 472–495, 2003.
[40]
H. Comon-Lundh and R. Treinen, “Easy intruder deductions,” in Verification: Theory and Practice, vol. 2772/2004 of Lecture Notes in Computer Science, pp. 182–184, Springer, Berlin, Germany, 2004.
[41]
S. Delaune, “Easy intruder deduction problems with homomorphisms,” Information Processing Letters, vol. 97, no. 6, pp. 213–218, 2006.
[42]
P. Lafourcade, D. Lugiez, and R. Treinen, “Intruder deduction for the equational theory of Abelian groups with distributive encryption,” Information and Computation, vol. 205, no. 4, pp. 581–623, 2007.
[43]
G. Bella, F. Massacci, and L. C. Paulson, “Verifying the SET registration protocols,” IEEE Journal on Selected Areas in Communications, vol. 21, no. 1, pp. 77–87, 2003.
[44]
L. C. Paulson, “Verifying the SET protocol: overview,” in Proceedings of the International Conference on Formal Aspects of Security (FASec '03), vol. 2629 of Lecture Notes in Computer Science, pp. 4–14, 2003.
[45]
S. Brlek, S. Hamadou, and J. Mullins, “A flaw in the electronic commerce protocol SET,” Information Processing Letters, vol. 97, no. 3, pp. 104–108, 2006.
[46]
S. Schneider, “An operational semantics for timed CSP,” in Proceedings of the Chalmers Workshop on Concurrency, Report PMGR63, pp. 428–456, Chalmers University of Technology and University of G？teborg, 1992.
[47]
J. W. Bryans and S. Schneider, “Mechanical verification of the full needhamschroeder public key protocol,” Tech. Rep. CSD-TR-97-11, University of London, 1997.
