Formal Analysis of Julia Key Agreement Protocol
Sivaraman, Navya ; Nadjm-Tehrani, Simin and Johansson, Thomas LU
(2025)
26th International Conference on Information and Communications Security, ICICS 2024
In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
15057 LNCS.
p.171-190
- Abstract
The evolution of the fifth-generation network (5G) increases the demand and use of Internet of Things (IoT) devices extensively. The increased number of IoT devices increases the possibility of new attack surfaces, and thus even resource-constrained IoT devices need secure communication. In this work, we consider the Julia Key Agreement (JKA) protocol, which has been proposed as a secure and efficient protocol for communication among resource-constrained IoT devices. We formally model two variants of the JKA protocol and verify the intended security requirements, such as mutual authentication, forward secrecy, backward secrecy, and resilience to key impersonation attacks, using the Tamarin prover. Our formal analysis shows that the JKA... (More)
The evolution of the fifth-generation network (5G) increases the demand and use of Internet of Things (IoT) devices extensively. The increased number of IoT devices increases the possibility of new attack surfaces, and thus even resource-constrained IoT devices need secure communication. In this work, we consider the Julia Key Agreement (JKA) protocol, which has been proposed as a secure and efficient protocol for communication among resource-constrained IoT devices. We formally model two variants of the JKA protocol and verify the intended security requirements, such as mutual authentication, forward secrecy, backward secrecy, and resilience to key impersonation attacks, using the Tamarin prover. Our formal analysis shows that the JKA protocol is susceptible to replay attacks under the Dolev-Yao threat model. We also expand the threat model by including several strong threat assumptions to discover interesting attack vectors.
(Less)
- author
- Sivaraman, Navya
; Nadjm-Tehrani, Simin
and Johansson, Thomas
LU
- organization
- publishing date
- 2025
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- Formal verification, IoT security, Key Agreement protocol, Tamarin
- host publication
- Information and Communications Security - 26th International Conference, ICICS 2024, Proceedings
- series title
- Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
- editor
- Katsikas, Sokratis ; Xenakis, Christos ; Lambrinoudakis, Costas and Kalloniatis, Christos
- volume
- 15057 LNCS
- pages
- 20 pages
- publisher
- Springer Science and Business Media B.V.
- conference name
- 26th International Conference on Information and Communications Security, ICICS 2024
- conference location
- Mytilene, Greece
- conference dates
- 2024-08-26 - 2024-08-28
- external identifiers
-
- scopus:85215327330
- ISSN
- 1611-3349
- 0302-9743
- ISBN
- 9789819788002
- DOI
- 10.1007/978-981-97-8801-9_9
- language
- English
- LU publication?
- yes
- additional info
- Publisher Copyright: © The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.
- id
- c03ced5a-83e4-4eb3-95d4-9338b18517d1
- date added to LUP
- 2025-04-23 11:06:16
- date last changed
- 2025-07-02 17:42:02
@inproceedings{c03ced5a-83e4-4eb3-95d4-9338b18517d1,
abstract = {{<p>The evolution of the fifth-generation network (5G) increases the demand and use of Internet of Things (IoT) devices extensively. The increased number of IoT devices increases the possibility of new attack surfaces, and thus even resource-constrained IoT devices need secure communication. In this work, we consider the Julia Key Agreement (JKA) protocol, which has been proposed as a secure and efficient protocol for communication among resource-constrained IoT devices. We formally model two variants of the JKA protocol and verify the intended security requirements, such as mutual authentication, forward secrecy, backward secrecy, and resilience to key impersonation attacks, using the Tamarin prover. Our formal analysis shows that the JKA protocol is susceptible to replay attacks under the Dolev-Yao threat model. We also expand the threat model by including several strong threat assumptions to discover interesting attack vectors.</p>}},
author = {{Sivaraman, Navya and Nadjm-Tehrani, Simin and Johansson, Thomas}},
booktitle = {{Information and Communications Security - 26th International Conference, ICICS 2024, Proceedings}},
editor = {{Katsikas, Sokratis and Xenakis, Christos and Lambrinoudakis, Costas and Kalloniatis, Christos}},
isbn = {{9789819788002}},
issn = {{1611-3349}},
keywords = {{Formal verification; IoT security; Key Agreement protocol; Tamarin}},
language = {{eng}},
pages = {{171--190}},
publisher = {{Springer Science and Business Media B.V.}},
series = {{Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}},
title = {{Formal Analysis of Julia Key Agreement Protocol}},
url = {{http://dx.doi.org/10.1007/978-981-97-8801-9_9}},
doi = {{10.1007/978-981-97-8801-9_9}},
volume = {{15057 LNCS}},
year = {{2025}},
}