Rule-based assumptions derivation of authentication protocols

Authentication protocol can be formally specified by using BAN logic. By using formal specification, we can analyse the protocol mathematically. Before the analysis can be done, we need to have some assumptions. If inadequate assumptions are used, the analysis might at a complete loss, and if we over assume, the analysis might not needed anymore. This paper presents preliminary result of our investigation on developing rules to derive assumptions from an authentication protocol written in BAN logic.