LTL Model Checking for Security Protocols