  Almost fifty years ago, D.E. Bell and L. LaPadula published the first formal
model of a secure system, known today as the Bell-LaPadula (BLP) model. BLP is
described as a state machine by means of first-order logic and set theory. The
authors also formalize two state invariants known as security condition and
*-property. Bell and LaPadula prove that all the state transitions preserve
these invariants.
  In this paper we present a fully automated proof of the security condition
and the *-property for all the model operations. The model and the proofs are
coded in the {log} tool. As far as we know this is the first time such proofs
are automated. Besides, we show that the {log} model is also an executable
prototype. Therefore we are providing an automatically verified executable
prototype of BLP.
