Abstract:

A construction scheme of the changeable intruder model is proposed. By defining the concept of abstract terms and their operation rules. The changeable intruder model (CIM) can greatly reduce the complexity of algebraic operations for intruders. And the CIM defines the intruder action library and the attack rule selection algorithm, which enables the analysts construct a changeable intruder model according to different protocols. As the actions of the intruder are composable, the CIM is able to dynamically adjust the intruder models. Changeable intruder model ensures both efficiency and correctness of the protocol analysis for model checkers.

Key words: security protocols, intruder model, algebraic operations, rewrite rules