Before revision: The Dolev–Yao model is a formal model used to prove properties of interactive cryptographic protocols.
After revision: , named after its authors Danny Dolev and Andrew Yao,The Dolev–Yao model is a formal model used to prove properties of interactive cryptographic protocols.