7th European Symposium on Research in Computer Security (ESORICS 2002)
Equal To The Task?
James Heather, Steve Schneider
Keywords : cryptographic protocols, rank functions, strand spaces, data independence, inequality tests, RSA, formal methods in security, security models, security verification
Abstract : Many methods of analysing security protocols have been proposed, but most such methods rely on analysing a protocol running only a finite network. Some, however - notably, data independence, the strand spaces model, and the rank functions model - can be used to prove correctness of a protocol running on an unbounded network. Roscoe and Broadfoot in [17] show how data independence techniques may be used to verify a security protocol running on an unbounded network. They also consider a weakness inherent in the RSA algorithm, discovered by Franklin and Reiter [3], and show that their data independence approach cannot deal with an intruder endowed with the ability to exploit this weakness. In this paper, we show that neither can the use of honest ideals in the strand spaces model or the use of rank functions in the CSP model be easily adapted to cover such an intruder. In each case, the inequality tests required to model the new intruder cause problems when attempting to extend analysis of a finite network to cover an unbounded network. The results suggest that more work is needed on adapting the intruder model to allow for cryptographic attacks.
(Pages 162-177)