Security verification of network protocols

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 cr...

Full description

Saved in:
Bibliographic Details
Main Author: Chong, Yew Heng
Other Authors: Zhang Tianwei
Format: Final Year Project
Language:English
Published: Nanyang Technological University 2021
Subjects:
Online Access:https://hdl.handle.net/10356/148831
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Nanyang Technological University
Language: English
id sg-ntu-dr.10356-148831
record_format dspace
spelling sg-ntu-dr.10356-1488312021-05-17T13:40:29Z Security verification of network protocols Chong, Yew Heng Zhang Tianwei School of Computer Science and Engineering tianwei.zhang@ntu.edu.sg Engineering::Computer science and engineering::Computer systems organization::Computer-communication networks 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. Bachelor of Engineering (Computer Science) 2021-05-17T13:40:29Z 2021-05-17T13:40:29Z 2021 Final Year Project (FYP) Chong, Y. H. (2021). Security verification of network protocols. Final Year Project (FYP), Nanyang Technological University, Singapore. https://hdl.handle.net/10356/148831 https://hdl.handle.net/10356/148831 en SCSE20-0463 application/pdf Nanyang Technological University
institution Nanyang Technological University
building NTU Library
continent Asia
country Singapore
Singapore
content_provider NTU Library
collection DR-NTU
language English
topic Engineering::Computer science and engineering::Computer systems organization::Computer-communication networks
spellingShingle Engineering::Computer science and engineering::Computer systems organization::Computer-communication networks
Chong, Yew Heng
Security verification of network protocols
description 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.
author2 Zhang Tianwei
author_facet Zhang Tianwei
Chong, Yew Heng
format Final Year Project
author Chong, Yew Heng
author_sort Chong, Yew Heng
title Security verification of network protocols
title_short Security verification of network protocols
title_full Security verification of network protocols
title_fullStr Security verification of network protocols
title_full_unstemmed Security verification of network protocols
title_sort security verification of network protocols
publisher Nanyang Technological University
publishDate 2021
url https://hdl.handle.net/10356/148831
_version_ 1701270563899572224