Automated Proof of Bell–LaPadula Security Properties