Sound Abstractions For Security Protocol Verification