Dette projekt har til formål at levere den første fuldstændige sikkerhedsanalyse af MLS både på det kryptografiske niveau og på implementeringsniveau i software, svarende til det, der allerede findes for TLS og Signal.
Forskerne ønsker at undersøge, om MLS faktisk er sikkert i praksis, også i nye versioner der er beskyttet mod fremtidige kvantecomputere. Projektet bygger videre på tidligere forskning fra Aarhus Universitet og samarbejdspartnere som Cryspen.
Ved hjælp af avancerede formelle metoder skal projektet skabe matematiske og maskinverificerede sikkerhedsbeviser for MLS. Samtidig vil forskningen undersøge, hvordan formel verifikation kan gøre det lettere at opnå sikkerhedscertificeringer som Common Criteria, der ofte kræves i offentlige og militære systemer.
Projektet forbinder dermed grundforskning, industriel brug og sikkerhedscertificering for at styrke sikre og åbne kommunikationssystemer.