Proving Information Security via Logics