Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting