The PQC4MED project, funded by the German Federal Ministry of Education and Research under grant number 16KIS1043, ran from 1 November 2019 to 31 January 2023. Its aim was to design, model and demonstrate an update infrastructure that would allow medical devices to transition to future quantum‑resistant cryptographic algorithms, also known as post‑quantum cryptography (PQC). The sub‑project “Security Models and Cryptographic Functionalities for PQC Technologies” was carried out by the Karlsruhe Institute of Technology (KIT), specifically the Institute for Information Security and Reliability (KASTEL), under the leadership of Prof. Jörn Müller‑Quade. KASTEL’s role was to develop a formally verifiable model of the update process and to advance the research toward provable security.

The technical work built on KASTEL’s existing expertise in formal protocol modelling and long‑term security analysis. Earlier studies had addressed updatable encryption and key‑reuse across primitive instantiations, but none had considered updates to algorithms that were unknown at system design time. The team therefore defined a sequence of component updates that preserves system functionality. They identified that an atomic update from a classical to a quantum‑resistant state inevitably creates an intermediate phase: initially all components operate with classical cryptography; during the transition they can communicate using both classical and PQC; finally, after all components have been updated, the system relies solely on the chosen PQC scheme. This staged approach guarantees that no component is left in an insecure configuration. The modelling also incorporated dependencies between components, ensuring that updates occur in an order that respects these relationships.

A key technical outcome was the integration of the FrodoKEM post‑quantum key encapsulation mechanism into the model. KASTEL presented the FrodoKEM design to the consortium, allowing the team to evaluate its suitability for secure element updates in endoscopic imaging systems. The modelling group, comprising Dr. Carmen Kempka (WIBU), Martin Böhning (CRS, subcontracted by Schölly), and Astrid Ottenhues (KASTEL), met regularly to translate practical update scenarios into formal specifications. Feedback loops with the consortium, conducted through virtual workshops and regular teleconferences, refined the update procedures and ensured that security criteria derived from formal analysis were reflected in the demonstrator design.

The demonstrator, conceived jointly with consortium partners, was intended to showcase the feasibility of the update infrastructure. Although the COVID‑19 pandemic caused schedule shifts and delayed the final release of NIST PQC candidates, the modelling and security analysis were completed within the extended project period. The final deliverables include a formally verified update protocol, a set of use‑case definitions based on endoscopic imaging, and a detailed security assessment aligned with NIST and BSI recommendations.

Collaboration involved multiple stakeholders. KIT/KASTEL led the formal modelling and security analysis. The consortium included the Institute for Biomedical Engineering (WIBU), the Center for Research in Security (CRS), and the company Schölly, which provided secure element expertise. The project also engaged with national standard bodies such as the German Federal Office for Information Security (BSI) and the National Institute of Standards and Technology (NIST) to align the PQC selection and update procedures with emerging standards. Regular meetings—initially in person at the kickoff on 5 November 2019, later virtually—kept all partners aligned. The project’s timeline was extended by a cost‑neutral extension to accommodate pandemic‑related disruptions, ensuring that the final model and demonstrator met the original objectives.