Extending the Dolev-Yao Intruder for Analyzing an Unbounded Number of Sessions