An intruder model with message inspection for model checking security protocols

Model checking security protocols is based on an intruder model that represents the eavesdropping or interception of the exchanged messages, while at the same time performs attack actions against the ongoing protocol session(s). Any attempt to enumerate all messages that can be deduced by the intruder and the possible actions in all protocol steps results in an enormous branching of the model's state space. In current work, we introduce a new intruder model that can be exploited for state space reduction, optionally in combination with known techniques, such as partial order and symmetry reduction. The proposed intruder modeling approach called Message Inspection (MI) is based on enhancing the intruder's knowledge with metadata for the exchanged messages. In a preliminary simulation run, the intruder tags the analyzed messages with protocol-specific values for a set of predefined parameters. This metadata is used to identify possible attack actions, for which it is a priori ...

• Type: Journal
• Year: 2010
• Where: COMPSEC
• Authors: Stylianos Basagiannis, Panagiotis Katsaros, Andrew Pombortsis
• Keywords: Attack Actions, COMPSEC 2010, Intruder Model, Model Checking Security