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
Provably Secure Communication Protocols for Remote Attestation
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
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.ORCID iD: 0000-0001-5888-1291
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
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 [en]
Remote Attestation, Formal Protocol Verification, Tamarin Prover, Authentication, Security Models, Protocol Attack
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:liu:diva-207831DOI: 10.1145/3664476.3664485ISBN: 9798400717185 (electronic)OAI: oai:DiVA.org:liu-207831DiVA, id: diva2:1901210
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
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

No full text in DiVA

Other links

Publisher's full text

Authority records

Asplund, MikaelJohansson, NiklasBoeira, Felipe

Search in DiVA

By author/editor
Wilson, JohannesAsplund, MikaelJohansson, NiklasBoeira, Felipe
By organisation
Software and SystemsFaculty of Science & EngineeringInformation Coding
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

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