Towards Post-Quantum Security for Cyber-Physical Systems: Integrating PQC into Industrial M2M Communication
This is the accompanying code for the paper "Towards Post-Quantum Security for Cyber-Physical Systems: Integrating PQC into Industrial M2M Communication" that appeared in Journal of Computer Security (DOI: 10.3233/JCS-210037); also available in Cryptology ePrint Archive: Report 2021/1563.
In our extended version, we provide a symbolic proof of confidentiality and authentication properties for quantum-resistant OPC UA variants. Our security analysis is based on the renowned formal verification tool ProVerif and the recently introduced protocol verifier Verifpal. The provided models allow the users to reproduce and extend the results reported in our work. Please cite the above paper when reporting, reproducing or extending the results.
This software is a research prototype, solely developed for and published as part of the publication cited above. It will neither be maintained nor monitored in any way.
- ProVerif (2.02pl1)
- Verifpal (0.21.4 or above)
Towards Post-Quantum Security for Cyber-Physical Systems is open-sourced under the AGPL-3.0 license. See the LICENSE file for details.
For a list of other open source components included in Towards Post-Quantum Security for Cyber-Physical Systems, see the file 3rd-party-licenses.txt.