Formalization of security

Gilles Barthe

Proof assistants are often used to validate that designs and implementations meet their expected security properties. A further motivation for using proof assistants is to support…