Abstract:
This paper discusses the BAN logic and the GNY logic whlch is an improvement of the first one. These two logics are applied to explain protocols step by step, with all initial assumptions made explicit and with the final states clearly set out. We focus on the differences between the logics, especially the approach used, the formulas and the logical postulates applied. Examples on how the logics are applied to proof protocols are also provided.