Constraint solving for bounded-process cryptographic protocol analysis

ABSTRACT

The reachability problem for cryptographic protocols with non-atomic keys can be solved via a simple constraint satisfaction procedure.

REFERENCES

• 1: Roberto M. Amadio , Denis Lugiez, On the Reachability Problem in Cryptographic Protocols, Proceedings of the 11th International Conference on Concurrency Theory, p.380-394, August 22-25, 2000
• 2: AMADIO, R., LUGIEZ, D., AND VANACKERE, V. On the symbolic reduction of processes with cryptographic functions. Tech. Rep. 4147, INRIA, March 2001.
• 3: Michele Boreale, Symbolic Trace Analysis of Cryptographic Protocols, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.667-681, July 08-12, 2001
• 4: Nancy Durgin , Patrick Lincoln , John Mitchell , Andre Scedrov , Iliano Cervesato, Relating Strands and Multiset Rewriting for Security Protocol Analysis, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.35, July 03-05, 2000
• 5: DURGIN, N., LINCOLN,P.,MITCHELL, J., AND SCEDROV, A. Undecidability of bounded security protocols. In Workshop on Formal Methods and Security Protocols (1999), FLOC.
• 6: Marcelo Fiore , Martín Abadi, Computing Symbolic Models for Verifying Cryptographic Protocols, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, p.160, June 11-13, 2001
• 7: FREIER, A., KARLTON,P.,AND KOCHER, P. The SSL protocol. Version 3.0. http://home.netscape.com/eng/ssl3/.
• 8: L. Gong, Using one-way functions for authentication, ACM SIGCOMM Computer Communication Review, v.19 n.5, p.8-11, Oct. 1989 [doi>10.1145/74681.74682]
• 9: Nevin Heintze , J. D. Tygar, A Model for Secure Protocols and Their Compositions, IEEE Transactions on Software Engineering, v.22 n.1, p.16-30, January 1996 [doi>10.1109/32.481514]
• 10: HUIMA, A. Efficient infinite-state analysis of security protocols. In Workshop on Formal Methods and Security Protocols (1999), FLOC.
• 11: Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
• 12: Lawrence C. Paulson, The inductive approach to verifying cryptographic protocols, Journal of Computer Security, v.6 n.1-2, p.85-128, Sept. 1998
• 13: Michaël Rusinowitch , Mathieu Turuani, Protocol Insecurity with Finite Number of Sessions is NP-Complete, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, p.174, June 11-13, 2001
• 14: Dawn Xiaodong Song, Athena: a New Efficient Automatic Checker for Security Protocol Analysis, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.192, June 28-30, 1999
• 15: J. Thayer , J. Herzog , J. Guttman, Honest Ideals on Strand Spaces, Proceedings of the 11th IEEE Computer Security Foundations Workshop, p.66, June 09-11, 1998
• 16: THAYER,F.,HERZOG, J., AND GUTTMAN, J. Strand spaces: Why is a security protocol correct? In IEEE Symposium on Security and Privacy (1998), pp. 160-171.

INDEX TERMS

Primary Classification:
  E. Data
  E.3 DATA ENCRYPTION
      Subjects: Public key cryptosystems

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol architecture (OSI model)

  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.6 Optimization
          Subjects: Constrained optimization

General Terms:
Algorithms, Design, Security