A model of computation for the NRL Protocol Analyzer
Catherine A. Meadows · 2002
We develop a model of computation for the NRL Protocol Analyzer by modifying and extending the model of computation for Burrows, Abadi, and Needham (BAN) logic (M. Burrows et al., 1990) developed by M. Abadi and M. Tuttle (1991). We use the results to point out the similarities and differences between the NRL Protocol Analyzer and BAN logic, and discuss the issues this raises with respect to the possible integration of the two.>