Text

Analisis protokol Pu dan Li dengan Tamarin Prover

---

Abstrak:
Protokol Pu dan Li merupakan salah satu protokol autentikasi antara unmanned aerial vehicles (UAV) dan ground station (GS). Protokol autentikasi ini berfungsi untuk menjamin bahwa hanya UAV sah yang dapat berkomunikasi dengan GS melalui jaringan publik. Pu dan Li mengklaim bahwa protokolnya tahan terhadap serangan cloning attack, tampering attack, man in the middle attack, dan replay attack pada komunikasi publik. Namun klaim tersebut tidak dianalisis secara formal oleh Pu dan Li, sehingga diperlukan analisis formal untuk membuktikan aspek keamanan yang diklaim. Pada analisis informal, pemodelan dan analisis dilakukan kurang terstruktur dan kurang objektif, sehingga perlu dilakukan analisis formal yang menggunakan pemodelan matematis dalam mendefinisikan protokol dan aspek keamanan yang memberikan hasil lebih objektif dari analisis informal. Tujuan dari penelitian ini adalah menganalisis secara formal aspek keamanan kerahasiaan dan autentikasi dari protokol Pu dan Li. Kedua aspek tersebut dapat menunjukkan apakah protokol tahan terhadap serangan yang disebutkan sebelumnya. Analisis formal dilakukan dengan menggunakan alat verifikasi Tamarin Prover.

Abstract:
Pu and Li protocols are one of the authentication protocols between unmanned aerial vehicles (UAV) and ground stations (GS). This authentication protocol serves to guarantee that only authorized UAVs can communicate with the GS over the public network. Pu and Li claim that the protocol is resistant to cloning attacks, tampering attacks, man in the middle attacks, and replay attacks on public communications. However, these claims were not formally analyzed by Pu and Li, making it necessary to conduct a formal analysis to prove the claimed security aspects. In informal analysis, the modeling and analysis are less structured and less objective, thus requiring a formal analysis that utilizes mathematical modeling to define the protocol and security aspects, providing more objective results than informal analysis. The aim of this study is to formally analyze the confidentiality and authentication security aspects of the Pu and Li protocols. Both of these aspects can indicate whether the protocol is resistant to the aforementioned attacks. Formal analysis was performed using Tamarin Prover's verification tool.

---

Availability

Detail Information

Series Title

--

Call Number

2023 LAZ a

Publisher

Bogor : Politeknik Siber dan Sandi Negara., 2023

Collation

xiv, 48 halaman

Language

Indonesia

ISBN/ISSN

--

Classification

Rekayasa Sistem Kriptografi

Content Type

-

Media Type

-

Carrier Type

-

Edition

--

Subject(s)

analisis formal
Tamarin Prover
Protokol autentikasi Pu dan Li
Unmanned Aerial Vehicles (UAV)

Specific Detail Info

--

Statement of Responsibility

Lazuardi Aulia Fahrensa

Other version/related

File Attachment

Comments

---

You must be logged in to post a comment