The NRL protocol analysis tool: a position paper

The author gives a brief description of the NRL protocol analysis tool, and contrasts its approach with other approaches. The NRL protocol analysis tool was developed in order to assist in security proofs for protocols. However, it has also proved to be useful in pointing out previously undiscovered flaws in already published protocols. The successes using the protocol analysis tool suggests, that in many cases a hybrid approach, relying upon human intuition when possible, and providing mechanical assistance when necessary, will provide the most practical advantage