Two of the goals of using weakest preconditions are to verify that authentication protocols meet their stated postconditions (as was done with the STS and the Needham-Schroeder protocols) and possibly to write authentication protocols which meet a desired set of postconditions. It is also hoped that both of these tasks can be fully or, at least, partially automated.
The advantages of the weakest preconditions for protocol verification are that they seem to require a minimum of premises (in contrast to the SvO logic) and a minimum of idealizations (in contrast to the BAN logics). The more premises and idealizations that must be included the more likely it is that one of them will be incorrect or assume to much and thereby hide a flaw in the protocol.
However, several features of the current weakest preconditions complicate the verification, and possibly the writing, of authentication protocols. The use of a not for several of the weakest preconditions means that these preconditions cannot be met by a single operation, but rather every operation must be examined to assure that it doesn't introduce a condition which would violate the not.
In many cases the same postcondition can be met by several different operations, which often require different preconditions. (For example, different encryption schemes means there are several ways of proving who sent a message.) This will make automatic generation of protocols more difficult because there will be several, often nearly equivalent, methods of meeting the desired postconditions leading to many potential protocols. One partial solution is to restrict the options in advance. For example, only allowing one type of key to be used.
Another important task should be the verification of the weakest preconditions themselves. Although based on the SvO logic which is sound, the mixture of axioms and semantics used in defining the weakest preconditions makes them suspect. Additionally, they incorporate several features (such as constructing shared secrets) which are not clearly presented in the SvO logic.