A rewriting-based inference system for the NRL protocol analyzer: grammar generation