NOTICE: Due to a lapse in annual appropriations, most of this website is not being updated. Learn more.

Form submissions will still be accepted but will not receive responses at this time. Sections of this site for programs using non-appropriated funds (such as NVLAP) or those that are excepted from the shutdown (such as CHIPS and NVD) will continue to be updated.

U.S. flag

An official website of the United States government

Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Secure .gov websites use HTTPS
A lock ( ) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.

PUBLICATIONS

Formal Verification of Bootstrapping Remote Secure Key Infrastructures (BRSKI) Protocol Using AVISPA

Published

Author(s)

Monika Singh, Mudumbai Ranganathan

Abstract

The last decade has seen significant growth in the number of IoT devices. These devices can connect to each other and networks. The process through which a new IoT device connects to the network and subsequently enables its services is called bootstrapping. A single entity connecting large numbers of new IoT devices to networks makes manual bootstrapping infeasible. It requires an automated system to enable a new device to be located and securely onboard the network. The Bootstrapping Remote Secure Key Infrastructure (BRSKI) protocol is one of the well-known protocols that provides a way for secure device onboarding. In this work, we present the first formal security analysis of the BRSKI protocol using a verification tool called AVISPA (Automated Validation of Internet Security Protocols and Applications). AVISPA provides a formal security validation of any network protocol by building and analyzing the formal security models of that protocol’s operations.
Citation
Technical Note (NIST TN) - 2123
Report Number
2123
NIST Pub Series
Technical Note (NIST TN)
Pub Type
NIST Pubs

Download Paper

DOI Link

Keywords

Authentication, AVISPA, Bootstrapping, HLPSL, SPAN, Formal Verification, X.509 certificates.
Protocol design and standardization, Network security and robustness, Network modeling and analysis, Internet of Things (IoT) and Cybersecurity and privacy

Citation

Singh, M. and Ranganathan, M. (2020), Formal Verification of Bootstrapping Remote Secure Key Infrastructures (BRSKI) Protocol Using AVISPA, Technical Note (NIST TN), National Institute of Standards and Technology, Gaithersburg, MD, [online], https://doi.org/10.6028/NIST.TN.2123 (Accessed October 9, 2025)

Issues

If you have any questions about this publication or are having problems accessing it, please contact [email protected].

Created October 6, 2020, Updated October 7, 2020
Was this page helpful?