liu.seSearch for publications in DiVA
1232 of 3
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
Towards Practical Formal Verification of Cryptographic Protocol Specifications and Implementations
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.ORCID iD: 0000-0002-3055-9951
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: urn:nbn:se:liu:diva-211228DOI: 10.3384/9789180759632ISBN: 9789180759625 (print)ISBN: 9789180759632 (electronic)OAI: oai:DiVA.org:liu-211228DiVA, id: diva2:1931892
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
List of papers
1. Extending the Authentication Hierarchy with One-Way Agreement
Open this publication in new window or tab >>Extending the Authentication Hierarchy with One-Way Agreement
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
Series
Proceedings - IEEE Computer Security Foundations Symposium (CSF), ISSN 1940-1434, E-ISSN 2374-8303
Keywords
authentication, network-protocols, protocol-verification, formal-methods, verification
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-197049 (URN)10.1109/CSF57540.2023.00025 (DOI)001061509400015 ()9798350321920 (ISBN)9798350321937 (ISBN)
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
2. Provably Secure Communication Protocols for Remote Attestation
Open this publication in new window or tab >>Provably Secure Communication Protocols for Remote Attestation
2024 (English)In: Proceedings of the 19th International Conference on Availability, Reliability and Security, New York, NY, USA, 2024Conference paper, Published paper (Refereed)
Abstract [en]

Remote Attestation is emerging as a promising technique to ensure that some remote device is in a trustworthy state. This can for example be an IoT device that is attested by a cloud service before allowing the device to connect. However, flaws in the communication protocols associated with the remote attestation mechanism can introduce vulnerabilities into the system design and potentially nullify the added security. Formal verification of protocol security can help to prevent such flaws. In this work we provide a detailed analysis of the necessary security properties for remote attestation focusing on the authenticity of the involved agents. We extend beyond existing work by considering the possibility of an attestation server (making the attestation process involve three parties) as well as requiring verifier authentication. We demonstrate that some security properties are not met by a state-of-the-art commercial protocol for remote attestation for our strong adversary model. Moreover, we design two new communication protocols for remote attestation that we formally prove fulfil all of the considered authentication properties.

Place, publisher, year, edition, pages
New York, NY, USA: , 2024
Keywords
Remote Attestation, Formal Protocol Verification, Tamarin Prover, Authentication, Security Models, Protocol Attack
National Category
Computer Systems
Identifiers
urn:nbn:se:liu:diva-207831 (URN)10.1145/3664476.3664485 (DOI)9798400717185 (ISBN)
Conference
The International Conference on Availability, Reliability and Security
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)
Available from: 2024-09-26 Created: 2024-09-26 Last updated: 2025-01-28
3. Analysing TLS Implementations Using Full-Message Symbolic Execution
Open this publication in new window or tab >>Analysing TLS Implementations Using Full-Message Symbolic Execution
2025 (English)In: Secure IT Systems: 29th Nordic Conference, NordSec 2024 Karlstad, Sweden, November 6–7, 2024 Proceedings / [ed] Leonardo Horn Iwaya, Liina Kamm, Leonardo Martucci, Tobias Pulls, Springer, 2025, Vol. 15396, p. 283-302Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we present a methodology for performing thorough analysis of TLS protocol implementations using dynamic symbolic execution. This method explores all possible inputs by treating entire messages as symbolic using KLEE. We are able to analyse the message parsing logic in detail, showing fulfilment of requirements from the protocol specification. This has previously not been performed for whole messages in complex protocols such as TLS. We tackle several problems that cause state space explosion by providing appropriate abstractions of implementation primitives. Additionally, we explore how protocol design choices impact the feasibility of analysis and argue for a strict TLS specification. We have applied our method to the ServerHello message parsing in several versions of the WolfSSL TLS 1.3 implementation. Our analysis revealed two vulnerabilities in the client implementation which were both assigned CVEs, one of them marked as high severity.

Place, publisher, year, edition, pages
Springer, 2025
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 15396
Keywords
Dynamic Symbolic Execution; Program Analysis; Protocol Analysis; Transport Layer Security
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-211257 (URN)10.1007/978-3-031-79007-2_15 (DOI)9783031790065 (ISBN)9783031790072 (ISBN)
Conference
29th Nordic Conference, NordSec 2024 Karlstad, Sweden, November 6–7, 2024
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)
Available from: 2025-01-30 Created: 2025-01-30 Last updated: 2025-01-30

Open Access in DiVA

fulltext(3338 kB)81 downloads
File information
File name FULLTEXT01.pdfFile size 3338 kBChecksum SHA-512
0dd95a8fd8b4c74f022fda3a82ea60c4542786db54d980b98d6c803eb4e1817edba2cc24e925d58aa0242bbd755ecc81752716f3b306999015744c658009759e
Type fulltextMimetype application/pdf
Order online >>

Other links

Publisher's full text

Authority records

Wilson, Johannes

Search in DiVA

By author/editor
Wilson, Johannes
By organisation
Software and SystemsFaculty of Science & Engineering
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 81 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: 299 hits
1232 of 3
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