Dolev–Yao model

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