Formal-Analysis-of-an-Authentication-Protocol-against-External-Cloud-Based-Denial-of-Service- DoS -Attack