Before revision: The Dolev-Yao model is a formal model used to prove properties of interactive cryptographic protocols.
After revision: The Dolev–Yao model is a formal model used to prove properties of interactive cryptographic protocols.