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

Jarred Ligatti, Ph.D.

Committee Member

Yao Liu, Ph.D.

Keywords

authentication, Formal methods, key-establishment, protocol verification, secrecy, security

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.

Share

COinS