Dr Hoang Nguyen

Associate Professor in Cyber Security

Computer Science

h.n.nguyen@swansea.ac.uk

Office - 411
Fourth Floor
Computational Foundry
Bay Campus

Available For Postgraduate Supervision

Research Links

https://orcid.org/0000-0003-0260-1697

Google Scholar

About

Dr Hoang Nga Nguyen is an Associate Professor in Cyber Security at Swansea University (UK). His current research agenda includes cybersecurity in automotive and autonomous systems. His recent work concentrates on developing model-based and simulation-based techniques to facilitate verification and validation, respectively, of security and safety requirements. His research project portfolio includes VRBMAS, ACID, Ditto, QRNG for CAV, Secure CAV, and AutoCHERI. They have been funded by EPSRC, RSSB, InnovateUK, and Digital Catapult. He is an associate member of the Verification & Validation of Autonomous Systems network and a member of the European Technical Working Group on Formal Methods in Railway Control. Currently, he is a participant in the DBbD TAP programme.

Publications

Research Highlights

Nguyen, H. & Rakib, A. (2023). Formal Modelling and Verification of Probabilistic Resource Bounded Agents. Journal of Logic, Language and Information, 32(5), 829-859.
https://doi.org/10.1007/s10849-023-09405-1, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa64995
http://dx.doi.org/10.1007/s10849-023-09405-1
Nguyen, H., Isobe, Y., Moller, F., Nguyen, H., & Roggenbach, M. (2012). Safety and Line Capacity in Railways – An Approach in Timed CSP. In Integrated Formal Methods (pp. 54-68). Springer-Verlag.
https://doi.org/10.1007/978-3-642-30729-4_5, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa13710
http://www.cs.swan.ac.uk/~csfm/ifm12.pdf
Nguyen, H., James, P., Moller, F., Nguyen, H., Roggenbach, M., Schneider, S., Treharne, H., Trumble, M., & Williams, D. (2014). Verification of Scheme Plans Using CSP || B. Software Engineering and Formal Methods -204).
https://doi.org/10.1007/978-3-319-05032-4_15, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa20838
Nguyen, H., James, P., Moller, F., Nguyen, H., Roggenbach, M., Schneider, S., & Treharne, H. (2014). Techniques for modelling and verifying railway interlockings. International Journal on Software Tools for Technology Transfer, 16(6), 685-711.
https://doi.org/10.1007/s10009-014-0304-7, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa21770
James, P., Moller, F., Nguyen, H., Roggenbach, M., Schneider, S., & Treharne, . (2014). Decomposing scheme plans to manage verification complexity. In FORMS/FORMAT- 10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems
SU Repository: https://cronfa.swan.ac.uk/Record/cronfa37077
Mahmood, S., Nguyen, H., & Shaikh, S. (2022). Systematic threat assessment and security testing of automotive over-the-air (OTA) updates. Vehicular Communications, 35, 100468
https://doi.org/10.1016/j.vehcom.2022.100468, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61038
Kalutarage, H., Nguyen, H., & Shaikh, S. (2017). Towards a threat assessment framework for apps collusion. Telecommunication Systems, 66(3), 417-430.
https://doi.org/10.1007/s11235-017-0296-1, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61043
Nguyen, H., Payre, W., Perelló-March, J., Sabaliauskaite, G., Jadidbonab, H., Shaikh, S., & Birrell, S. (2022). How system failures and ransomwares affect drivers' trust and attitudes in an automated car? A simulator study. In AHFE International (pp. 453-460). AHFE International.
https://doi.org/10.54941/ahfe1002764, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61831
Alechina, N., Logan, B., Nguyen, H., & Raimondi, F. (2017). Model-checking for Resource-Bounded ATL with production and consumption of resources. Journal of Computer and System Sciences, 88, 126-144.
https://doi.org/10.1016/j.jcss.2017.03.008, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61979
Alechina, N., Bulling, N., Logan, B., & Nguyen, H. (2017). The virtues of idleness: A decidable fragment of resource agent logic. Artificial Intelligence, 245, 56-85.
https://doi.org/10.1016/j.artint.2016.12.005, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61980

All Research

Journal Articles

Jayaratne, D., Kamtam, S., Shaikh, S., Ramli, M., Lu, Q., Mepparambath, R., Nguyen, H., & Rakib, A. (2024). A simulation framework for automotive cybersecurity risk assessment. Simulation Modelling Practice and Theory, 136, 103005
https://doi.org/10.1016/j.simpat.2024.103005, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa67382
Pickford, J., Attale, R., Shaikh, S., Nguyen, H., & Harrison, L. (2024). Systematic Risk Characterisation of Hardware Threats to Automotive System. ACM Journal on Autonomous Transportation Systems, 1(4), 1-36.
https://doi.org/10.1145/3661315, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa66221
Nguyen, H. & Rakib, A. (2023). Formal Modelling and Verification of Probabilistic Resource Bounded Agents. Journal of Logic, Language and Information, 32(5), 829-859.
https://doi.org/10.1007/s10849-023-09405-1, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa64995
http://dx.doi.org/10.1007/s10849-023-09405-1
Taylor, S., Ahmad, F., Nguyen, H., Shaikh, S., Bryans, J., & Wartnaby, C. (2023). A comparative analysis of multi‐criteria decision methods for secure beacon selection in vehicular platoons. Transactions on Emerging Telecommunications Technologies, 34(11)
https://doi.org/10.1002/ett.4841, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa63997
http://dx.doi.org/10.1002/ett.4841
Bryans, J., Liew, L., Nguyen, H., Sabaliauskaite, G., & Shaikh, S. (2023). Formal Template-Based Generation of Attack–Defence Trees for Automated Security Analysis. information, 14(9)
https://doi.org/10.3390/info14090481, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa64161
Kirk, R., Nguyen, H., Bryans, J., Shaikh, S., & Wartnaby, C. (2023). A formal framework for security testing of automotive over-the-air update systems. Journal of Logical and Algebraic Methods in Programming, 130, 100812
https://doi.org/10.1016/j.jlamp.2022.100812, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61305
Taylor, S., Ahmad, F., Nguyen, H., & Shaikh, S. (2022). Vehicular Platoon Communication: Architecture, Security Threats and Open Challenges. Sensors, 23(1), 134
https://doi.org/10.3390/s23010134, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa62213
Mahmood, S., Nguyen, H., & Shaikh, S. (2022). Systematic threat assessment and security testing of automotive over-the-air (OTA) updates. Vehicular Communications, 35, 100468
https://doi.org/10.1016/j.vehcom.2022.100468, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61038
Kalutarage, H., Nguyen, H., & Shaikh, S. (2017). Towards a threat assessment framework for apps collusion. Telecommunication Systems, 66(3), 417-430.
https://doi.org/10.1007/s11235-017-0296-1, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61043
Alechina, N., Logan, B., Nguyen, H., & Raimondi, F. (2017). Model-checking for Resource-Bounded ATL with production and consumption of resources. Journal of Computer and System Sciences, 88, 126-144.
https://doi.org/10.1016/j.jcss.2017.03.008, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61979
Alechina, N., Bulling, N., Logan, B., & Nguyen, H. (2017). The virtues of idleness: A decidable fragment of resource agent logic. Artificial Intelligence, 245, 56-85.
https://doi.org/10.1016/j.artint.2016.12.005, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61980
Nguyen, H., Alechina, N., Logan, B., & Rakib, A. (2015). Alternating-time temporal logic with resource bounds. Journal of Logic and Computation, 28(4), 631-663.
https://doi.org/10.1093/logcom/exv034, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61988
Nguyen, H., James, P., Moller, F., Nguyen, H., Roggenbach, M., Schneider, S., & Treharne, H. (2014). Techniques for modelling and verifying railway interlockings. International Journal on Software Tools for Technology Transfer, 16(6), 685-711.
https://doi.org/10.1007/s10009-014-0304-7, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa21770

Book Chapters

Nguyen, H., James, P., Moller, F., Nguyen, H., Roggenbach, M., Schneider, S., Treharne, H., Trumble, M., & Williams, D. (2014). Verification of Scheme Plans Using CSP || B. Software Engineering and Formal Methods -204).
https://doi.org/10.1007/978-3-319-05032-4_15, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa20838
Mahmood, S., Nguyen, H., & Shaikh, S. (n.d.) Automotive Cybersecurity Testing: Survey of Testbeds and Methods. Studies in Big Data (pp. 219-243). Springer International Publishing
https://doi.org/10.1007/978-3-030-65722-2_14, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa63978
http://dx.doi.org/10.1007/978-3-030-65722-2_14

Conference Contributions

Nguyen, H., Payre, W., Perelló-March, J., Sabaliauskaite, G., Jadidbonab, H., Shaikh, S., & Birrell, S. (2022). How system failures and ransomwares affect drivers' trust and attitudes in an automated car? A simulator study. In AHFE International (pp. 453-460). AHFE International.
https://doi.org/10.54941/ahfe1002764, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61831
Payre, W., Perellomarch, J., Sabaliauskaite, G., Jadidbonab, H., Shaikh, S., Nguyen, H., & Birrell, S. (2022). Understanding drivers' trust after software malfunctions and cyber intrusions of digital displays in an automated car. In Human Factors in Transportation (pp. 320-328). AHFE International.
https://doi.org/10.54941/ahfe1002463, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61832
Kirk, R., Nguyen, H., Bryans, J., Shaikh, S., Evans, D., & Price, D. (2021). Formalising UPTANE in CSP for Security Testing. In 2021 IEEE 21st International Conference on Software Quality, Reliability and Security Companion (QRS-C)IEEE.
https://doi.org/10.1109/qrs-c55045.2021.00124, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa63976
http://dx.doi.org/10.1109/qrs-c55045.2021.00124
Taylor, S., Ahmad, F., Nguyen, H., Shaikh, S., Evans, D., & Price, D. (2021). Vehicular Platoon Communication: Cybersecurity Threats and Open Challenges. In 2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W)IEEE.
https://doi.org/10.1109/dsn-w52860.2021.00015, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa63977
Bryans, J., Liew, L., Nguyen, H., Sabaliauskaite, G., Shaikh, S., & Zhou, F. (2020). A Template-Based Method for the Generation of Attack Trees. In Information Security Theory and Practice (pp. 155-165). Springer International Publishing.
https://doi.org/10.1007/978-3-030-41702-4_10, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61837
Chen, L., James, P., Kirkwood, D., Nguyen, H., Nicholson, G., & Roggenbach, M. (2016). Towards integrated simulation and formal verification of rail yard designs - an experience report based on the UK East Coast Main Line. In 2016 IEEE International Conference on Intelligent Rail Transportation (ICIRT)IEEE.
https://doi.org/10.1109/icirt.2016.7588753, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61986
James, P., Moller, F., Nguyen, H., Roggenbach, M., Treharne, H., & Wang, X. (2016). OnTrack: The Railway Verification Toolset. In Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications (pp. 294-296). Springer International Publishing.
https://doi.org/10.1007/978-3-319-47169-3_21, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61984
Cheah, M., Shaikh, S., Bryans, J., & Nguyen, H. (2016). Combining Third Party Components Securely in Automotive Systems. In Information Security Theory and Practice (pp. 262-269). Springer International Publishing.
https://doi.org/10.1007/978-3-319-45931-8_18, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61982
Asăvoae, I., Nguyen, H., Roggenbach, M., & Shaikh, S. (2016). Utilising K Semantics for Collusion Detection in Android Applications. In Lecture Notes in Computer Science (pp. 142-149). Springer International Publishing.
https://doi.org/10.1007/978-3-319-45943-1_10, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61987
Nguyen, H. (2016). Towards Automated Android App Collusion Detection. In 1st International Workshop on Innovations in Mobile Privacy and Security
SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61985
https://ceur-ws.org/Vol-1575/
Bulling, N. & Nguyen, H. (2015). Model Checking Resource Bounded Systems with Shared Resources via Alternating Büchi Pushdown Systems. In PRIMA 2015: Principles and Practice of Multi-Agent Systems (pp. 640-649). Springer International Publishing.
https://doi.org/10.1007/978-3-319-25524-8_47, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61989
Alechina, N., Bulling, N., Logan, B., & Nguyen, H. (2015). On the boundary of (un)decidability: decidable model-checking for a fragment of Resource Agent Logic. In IJCAI'15: Proceedings of the 24th International Conference on Artificial IntelligenceAAAI Press.
SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61990
https://dl.acm.org/doi/10.5555/2832415.2832457
Haxthausen, A., Nguyen, H., & Roggenbach, M. (2015). Comparing Formal Verification Approaches of Interlocking Systems. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification (pp. 160-177). Springer International Publishing.
https://doi.org/10.1007/978-3-319-33951-1_12, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61983
Alechina, N., Logan, B., Nguyen, H., Raimondi, F., & Mostarda, L. (2015). Symbolic model-checking for resource-bounded ATL. In AAMAS'15: International Conference on Autonomous Agents and Multiagent SystemsACM Digital Library.
SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61991
https://dl.acm.org/doi/10.5555/2772879.2773448
Alechina, N., Logan, B., Nguyen, H., & Raimondi, F. (2015). Symbolic model-checking for single resource RB+-ATL. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)
SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61992
http://ijcai.org/Proceedings/15/Papers/155.pdf
Alechina, N., Logan, B., Nguyen, H., & Raimondi, F. (2014). Decidable model-checking for a resource logic with production of resources. In ECAI 2014 : 21st European Conference on Artificial IntelligenceIOS Press.
https://doi.org/10.3233/978-1-61499-419-0-9, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61993
James, P., Moller, F., Nguyen, H., Roggenbach, M., Schneider, S., & Treharne, . (2014). Decomposing scheme plans to manage verification complexity. In FORMS/FORMAT- 10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems
SU Repository: https://cronfa.swan.ac.uk/Record/cronfa37077
Nguyen, H., Isobe, Y., Moller, F., Nguyen, H., & Roggenbach, M. (2012). Safety and Line Capacity in Railways – An Approach in Timed CSP. In Integrated Formal Methods (pp. 54-68). Springer-Verlag.
https://doi.org/10.1007/978-3-642-30729-4_5, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa13710
http://www.cs.swan.ac.uk/~csfm/ifm12.pdf

Supervision

Model-Based Security Testing Approaches for Hardware Security (current)

PhD

Other supervisor: Prof Siraj Shaikh

Taught Modules

CSCM68 Embedded Systems Security

Embedded systems are information processing systems embedded into enclosing products such as cars, telecommunication or fabrication equipment. They are essential for providing ubiquitous information, one of the key goals of modern information technology. The aim of this module is to provide an overview of embedded system design, to relate the most important topics in embedded system design to each other, and to obtain an appreciation of the model based approach to embedded systems design. The lab provides hands-on experience in the design of embedded systems. Due to the labs' hardware requirements, the number of places available for this module is limited. Places will be allocated during the first week of teaching; the allocation criteria will be announced in the first lecture.

Key Grants and Projects

Securing connected vehicles with Digital Security by Design technologies (AutoCHERI) 2022 - 2024

, with Co-I: Siraj Shaikh, £214K

Dr Hoang Nguyen

Email address

Research Links

About

Research Highlights

All Research

Model-Based Security Testing Approaches for Hardware Security (current)

CSCM68 Embedded Systems Security