A (restricted) quantifier elimination for security protocols

While reasoning about security protocols, most of the difficulty of reasoning relates to the complicated semantics (with freshness of nonces, multisessions, etc.). While logics for security protocols need to be abstract (without explicitly dealing with nonces, encryption, etc.), ignoring details may result in rendering any verification of abstract properties worthless. We would like the verification problem for the logic to be decidable as well, to allow for automated methods for detecting attacks. From this viewpoint, we study a logic with session abstraction and quantifiers over session names. We show that interesting security properties like secrecy and authentication can be described in the logic. We prove the existence of a normal form for runs of tagged protocols. This leads to a quantifier elimination result for the logic which establishes the decidability of the verification problem for tagged protocols, when we assume a fixed finite set of nonces.