liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal Analysis of Julia Key Agreement Protocol
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering. (IDA-SAS-RTSLAB)ORCID iD: 0000-0003-0123-1970
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering. (IDA-SAS-RTSLAB)ORCID iD: 0000-0002-1485-0802
Lund University, Sweden.ORCID iD: 0000-0003-1798-570X
2024 (English)In: 26th International Conference, ICICS 2024, Proceedings, Part II, Springer Nature, 2024Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer Nature, 2024.
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 15057
Keywords [en]
Key Agreement protocol, IoT security, Formal verification, Tamarin
National Category
Communication Systems
Identifiers
URN: urn:nbn:se:liu:diva-211016DOI: 10.1007/978-981-97-8801-9_9ISBN: 9789819788002 (print)ISBN: 9789819788019 (electronic)OAI: oai:DiVA.org:liu-211016DiVA, id: diva2:1928398
Conference
26th International Conference on Information and Communications Security, Mytilene, Greece, August 26–28, 2024
Available from: 2025-01-16 Created: 2025-01-16 Last updated: 2025-01-22

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records

Sivaraman, NavyaNadjm-Tehrani, Simin

Search in DiVA

By author/editor
Sivaraman, NavyaNadjm-Tehrani, SiminJohansson, Thomas
By organisation
Software and SystemsFaculty of Science & Engineering
Communication Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 24 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf