Graduation Year
2015
Document Type
Thesis
Degree
M.S.C.S.
Degree Name
MS in Computer Science (M.S.C.S.)
Degree Granting Department
Computer Science and Engineering
Major Professor
Hao Zheng, Ph.D.
Co-Major Professor
Jay Ligatti, Ph.D.
Committee Member
Yao Liu, Ph.D.
Keywords
Formal methods, security, secrecy
Abstract
Protocol verification is an exciting area of network security that intersects engineering and formal methods. This thesis presents a comparison of formal verification tools for security protocols for their respective strengths and weaknesses supported by the results from several case studies. The formal verification tools considered are based on explicit model checking (SPIN), symbolic analysis (Proverif) and theorem proving (Coq). We formalize and provide models of several well-known authentication and key-establishment protocols in each of the specification languages, and use the tools to find attacks that show protocols insecurity. We contrast the modelling process on each of the tools by comparing features of their modelling languages, verification efforts involved, and analysis results
Our results show that authentication and key-establishment protocols can be specified in Coq’s modeling language with an unbounded number of sessions and message space. However, proofs in Coq require human guidance. SPIN runs automated verification with a restricted version of the Dolev-Yao attacker model. Proverif has several advantages over SPIN and Coq: a tailored specification language, and better performance on infinite state space analysis.
Scholar Commons Citation
Palombo, Hernan Miguel, "A Comparative Study of Formal Verification Techniques for Authentication Protocols" (2015). USF Tampa Graduate Theses and Dissertations.
https://digitalcommons.usf.edu/etd/6008
