Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution