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
Extending the Authentication Hierarchy with One-Way Agreement
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering. Sectra Commun, Linkoping, Sweden.ORCID iD: 0000-0002-3055-9951
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.ORCID iD: 0000-0003-1916-3398
Linköping University, Department of Electrical Engineering, Information Coding. Linköping University, Faculty of Science & Engineering. Sectra Commun, Linkoping, Sweden.ORCID iD: 0000-0001-5888-1291
2023 (English)In: 2023 IEEE 36th Computer Security Foundations Symposium (CSF), Los Alamitos, CA, USA: IEEE Computer Society, 2023, p. 214-228Conference paper, Published paper (Refereed)
Abstract [en]

Providing authenticated interactions is a key responsibility of most cryptographic protocols. When designing new protocols with strict security requirements it is therefore essential to formally verify that they fulfil appropriate authentication properties. We identify a gap in the case of protocols with unilateral (one-way) authentication, where existing properties are poorly adapted. In existing work, there is a preference for defining strong authentication properties, which is good in many cases but not universally applicable. In this work we make the case for weaker authentication properties. In particular, we investigate one-way authentication and extend Lowe's authentication hierarchy with two such properties. We formally prove the relationship between the added and existing properties. Moreover, we demonstrate the usefulness of the added properties in a case study on remote attestation protocols. This work complements earlier work with additional generic properties that support formal verification of a wider set of protocol types.

Place, publisher, year, edition, pages
Los Alamitos, CA, USA: IEEE Computer Society, 2023. p. 214-228
Series
Proceedings - IEEE Computer Security Foundations Symposium (CSF), ISSN 1940-1434, E-ISSN 2374-8303
Keywords [en]
authentication, network-protocols, protocol-verification, formal-methods, verification
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:liu:diva-197049DOI: 10.1109/CSF57540.2023.00025ISI: 001061509400015ISBN: 9798350321920 (electronic)ISBN: 9798350321937 (print)OAI: oai:DiVA.org:liu-197049DiVA, id: diva2:1789863
Conference
2023 IEEE 36th Computer Security Foundations Symposium (CSF), Jul 07 2023 to Jul 10 2023, Dubrovnik, Croatia
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)
Note

Funding: Wallenberg AI, Autonomous Systems and Software Program (WASP) - Knut and Alice Wallenberg Foundation

Available from: 2023-08-21 Created: 2023-08-21 Last updated: 2025-01-28Bibliographically approved
In thesis
1. Towards Practical Formal Verification of Cryptographic Protocol Specifications and Implementations
Open this publication in new window or tab >>Towards Practical Formal Verification of Cryptographic Protocol Specifications and Implementations
2025 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Modern computer systems communicate using protocols. Protocols are critical to security as they are the interface over which systems are accessible to the outside world. Cryptography is what enables secure communication even over insecure channels, and cryptographic protocols are the basis for modern internet security. Encryption enables confidentiality even if eavesdropping is possible, and cryptographic signatures can provide authenticity even if messages can be mimicked, modified, or reproduced.

Designing secure cryptographic protocols remains challenging. Many protocols once believed to be secure have since been broken and redesigned. The highest guarantees of security are achieved using formal methods, where mathematical logic is used for reasoning. Modern formal methods research tools have proven effective in finding and proving the absence of flaws in protocols, yet they are challenging to use. Correctly implementing large, complex protocols is also a challenge, and many vulnerabilities have been caused by errors introduced during the implementation phase. Formal software verification remains a daunting task which often requires manual effort by formal methods experts.

This licentiate thesis contributes towards providing formal protocol analysis methods that are intended to be more practical and useful for industrial application. Both the design phase of protocols and the analysis of protocol implementations are covered, showing how modern tools can be used to perform thorough analysis. The analysis discovers design and implementation flaws in modern commercial cryptographic protocols which are reported to the developers.

The analysis demonstrates challenges as well as the opportunities of adopting more formal methods for the analysis of protocols. Challenges which are tackled in this thesis include specifying an accurate model and selecting security properties for remote attestation proto-cols, and circumventing state space explosion during symbolic execution of protocol implementations. Opportunities include the ability to provide a more thorough analysis of protocol specifications as well as implementations in order to cover requirements which are difficult to test.

To make verification goals and assumptions more clear, this thesis also presents precise formulations of authentication which are appropriate for verification in the formal model. The authentication properties are suitable for protocols which perform one-way authentication of one of the agents, and complement existing mutual authentication definitions.

Place, publisher, year, edition, pages
Linköping: Linköping University Electronic Press, 2025. p. 31
Series
Linköping Studies in Science and Technology. Licentiate Thesis, ISSN 0280-7971 ; 2011
National Category
Computer Systems
Identifiers
urn:nbn:se:liu:diva-211228 (URN)10.3384/9789180759632 (DOI)9789180759625 (ISBN)9789180759632 (ISBN)
Presentation
2025-02-28, Ada Lovelace, B-building, Campus Valla, Linköping, 13:15 (English)
Opponent
Supervisors
Note

Funding: This work was partially supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.

Available from: 2025-01-28 Created: 2025-01-28 Last updated: 2025-01-30Bibliographically approved

Open Access in DiVA

fulltext(367 kB)474 downloads
File information
File name FULLTEXT01.pdfFile size 367 kBChecksum SHA-512
dd01b71bf66486c824bcfb3b974c35818adadc272994433facf5195146978668c219d1900ae58804eee12c2703e154b7d296f2bd01a84d3eb6c5c55ee15ff856
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Authority records

Wilson, JohannesAsplund, MikaelJohansson, Niklas

Search in DiVA

By author/editor
Wilson, JohannesAsplund, MikaelJohansson, Niklas
By organisation
Software and SystemsFaculty of Science & EngineeringInformation Coding
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 481 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 282 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