The necessitation rule permits boxing a theorem in a modal proof system. It does not permit boxing an arbitrary temporary assumption. Under an arithmetic interpretation, it uses the external first of the derivability conditions: an actual proof of supplies a proof that has a proof. This distinction matters when proving the Internal form of Löb's theorem.
New to topics? Read the docs here!