Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security Protocols

As more resources are added to computer networks, and as more vendors look to the World Wide Web as a viable marketplace, the importance of being able to restrict access and to ensure some kind of acceptable behavior even in the presence of malicious adversaries becomes paramount.