SAT-based Model Checking for Security Protocols Analysis