Towards a Metalogic for Security Protocol Analysis