Abstract:
One area that has been particularly productive in the rapidly growing field of formal analysis of cryptographic protocols is development of special-purpose model checkers. These tools use variants of the Dolev-Yao model to search through different concurrent executions of a protocol in the face of a network controlled by an attacker who can read, alter, and redirect traffic using operations available to an honest principal. These tools have been extremely effective at finding non-intuitive flaws in protocol design.
