| Summary: | Cryptographic security protocols are used to allow agents to communicate securely over an insecure network. Although security protocols are usually quite short, they often have subtle flaws in them which allow the protocol to be 'attacked' and security breached. Interactive inductive theorem proving has been used to verify properties of security protocols. However, trying to verify a flawed protocol will result in an attempt to prove an incorrect conjecture. A user might waste a lot of time proposing generalisations and lemmas etc. in a futile attempt to prove a falsehood. In addition, even if he suspects the protocol is flawed, it can be extremely difficult to find the attack (the sequence of messages needed to expose the flaw). What is required is an automated tool which can not only detect incorrect inductive conjectures, but also present a counterexample. This thesis describes the development of such a tool, CORAL, based on the refutation complete Comon-Nieuwenhuis method for 'proof by consistency'. We describe the testing of CORAL on some protocols known to be flawed, and a case study on a new protocol, in which CORAL discovered three previously unknown attacks. CORAL does not find attacks as fast as some competing approaches, but in its modelling of a group protocol, shows a flexibility other systems lack. This should make it suitable for a variety of future developments, including investigation some more unusual security protocols.
|
|---|
