A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties | Publicación