Model checkers such as FDR have been extremely effective in checking for, and finding, attacks on cryptographic protocols – see, for example, and many of the papers in . Their use in proving protocols has, on the other hand, generally been limited to