Nivel de seguridad 5 del CC. Diseño y prueba semiformal. El análisis incluye toda la implementación. La garantía está complementada por un modelo formal, una presentación semiformal de las especificaciones funcionales, un diseño de alto nivel y una demostración semiformal de la correspondencia. La búsqueda de vulnerabilidades debe asegurar una relativa resistencia a los ataques de penetración. Son también necesarios un análisis de canales protegidos y un diseño modular.
