Security verification of network protocols

• Main Author: Chong, Yew Heng
• Other Authors: Zhang Tianwei
• Format: Final Year Project
• Language: English
• Published: Nanyang Technological University 2021
• Subjects: Engineering::Computer science and engineering::Computer systems organization::Computer-communication networks
• Online Access: https://hdl.handle.net/10356/148831
• Institution: Nanyang Technological University

Network protocols define the security rules for secure communication between two computer system over a computer network. Cryptographic functions are used as a mean to protect the information transmitted from unauthorised eavesdropping or modifications. However, it is not easy to determine if the cryptographic functions are implemented and used correctly, especially so by just looking at the source code. In this report, we will look at ways to model these network protocols using a formal mathematical model such that their security properties can be evaluated with a higher degree of assurance. The focus will on Dolev-Yao model as it provide a simple framework to analyse network protocols. In this report, we will use the tool ProVerif to prove the security properties of network protocols formalised using Dolev-Yao model. We will use ProVerif to prove the security properties of two protocols - the naive handshake and the Needham- Schroeder public key. In particular, we will analyse the results of ProVerif for the Needham-Schroeder public key protocol as the protocol is proven to violate secrecy and authentication, two essential security properties all network protocols should adhere to. Finally, we discuss the capabilities of ProVerif in terms of how well it can model a network protocol and prove its security properties.