Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents