We begin by given a brief introduction to the NRL Protocol Analyzer. We then compare the rules of the analyzer with the rules outlined in the previous section. We go on to augment the analyzer rules to capture the necessary formalism. We give informal arguments on the mapping between our definitions and analysis using the analyzer.