Data independent verification of crypto−protocols

Abstract It is only possible to model check very small implementations of cryptographic protocols (when measured by numbers of agents, nonces, etc.). It is highly desirable to have results which permit us to infer the security of much larger implementations from carefully-chosen small ones, and the specialised use of data independence provides one route to this type of result. I will report on the methods we use and some recent results and conjectures which provide generalisations.