In this paper we presented a weakest precondition calculus for the verification of authentication of authentication protocols. The benefits of this approach to protocol verification include automatic generation of protocol preconditions, analysis of only recipient beliefs, and detailed specification of the protocol steps. In this section we present some of our thoughts on the benefits and drawbacks of this approach. We then present a brief discussion outlining an approach to formal protocol derivation as a derivative of this work.