In this report we develop methods for analyzing key management and authentication protocols by using techniques developed for the solution of equations in a term-rewriting system. In particular, we describe a model of or class of protocols and possible attacks on those protocols as term-rewriting systems. We also describe a software tool based on the narrowing algorithm that can be used in the analysis of such protocols. We formally model a protocol and describe the results of using these techniques to analyze various security properties. Two security flaws were found. A corrected scheme was also formally modeled and verified by using these techniques. Keywords: Formal specification, Logic programming, Verification.