 Burrows–Abadi–Needham logic

Burrows–Abadi–Needham logic, often abbreviated as BAN logic, is a formal system used for reasoning about authentication and security protocols. It was developed by Michael Burrows, Martyn Abadi, and Roger Needham in the early 1990s and is particularly focused on the properties of cryptographic protocols, especially those involving keys, messages, and entities in a distributed system.