To infinity and beyond or, avoiding the infinite in security protocol analysis

ABSTRACT

We investigate conditions under which an infinite set of atomic messages can be replaced with one or two values without affecting the correctness of a security protocol. The work is conducted using the strand spaces formalism, but the results apply to all protocol analysis techniques, and should be of particular value to those using model checking.The implications of the central result are discussed.

REFERENCES

• 1: H. Comon-Lundh and V. Cortier. Security Properties: Two Agents Are Sufficient. In Proceedings of the 12th European Symposium on Programming (ESOP 2003), volume 2618 of Lecture Notes in Computer Science. Springer-Verlag, Apr. 2003.
• 2: N. A. Durgin, P. D. Lincoln, J. C. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In Workshop on Formal Methods and Security Protocols (FMSP'99), The 1999 Federated Logic Conference (FLoC'99), July 1999.
• 3: M. Franklin and M. Reiter. A linear protocol failure for RSA with exponent three. 1995. Presented at the Rump Session of Crypto '95, Santa Barbara, CA.
• 4: Joshua D. Guttman , F. Javier Thayer, Protocol Independence through Disjoint Encryption, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.24, July 03-05, 2000
• 5: J. D. Guttman and F. J. Thayer Fábrega. The Sizes of Skeletons. Mtr, The MITRE Corporation, Bedford, MA, January 2005.
• 6: J. A. Heather. 'Oh! . . . Is it really you?'--- Using rank functions to verify authentication protocols. Department of Computer Science, Royal Holloway, University of London, December 2000.
• 7: James Heather , Gavin Lowe , Steve Schneider, How to prevent type flaw attacks on security protocols, Journal of Computer Security, v.11 n.2, p.217-244, May 2003
• 8: James Heather , Steve Schneider, Equal To The Task?, Proceedings of the 7th European Symposium on Research in Computer Security, p.162-177, October 14-16, 2002
• 9: James Heather , Steve Schneider, A decision procedure for the existence of a rank function, Journal of Computer Security, v.13 n.2, p.317-344, March 2005
• 10: 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
• 11: Roger M. Needham , Michael D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, v.21 n.12, p.993-999, Dec. 1978 [doi>10.1145/359657.359659]
• 12: A. W. Roscoe , P. J. Broadfoot, Proving security protocols with model checkers by data independence techniques, Journal of Computer Security, v.7 n.2-3, p.147-190, Jan. 1999
• 13: 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
• 14: F. Javier Thayer Fábrega, Strand spaces: proving security protocols correct, Journal of Computer Security, v.7 n.2-3, p.191-230, Jan. 1999

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)

General Terms:
Algorithms, Security, Verification

Keywords:
model checking, security protocols, strand spaces