Prouver la sécurité informatique : la logique à la rescousse