Handling infeasible specifications of cryptographic protocols

In the verification of cryptographic protocols using the authentication logic of Burrows, Abadi, and Needham (1989) it is possible to write a specification which does not faithfully represent the real world situation. Such a specification, though impossible or unreasonable to implement, can go undetected and be verified to be correct. It can also lead to logical statements that do not preserve causality which in turn can have undesirable consequences. Such a specification, called an infeasible specification, can be subtle and hard to locate. The article shows how the logic of cryptographic protocols of Gong, Needham, and Yahalom (1990) can be enhanced with a notion of eligibility to preserve causality of beliefs and detect infeasible specifications. It is conceivable that this technique can be adopted in other similar logics