Model checking the security of multi-protocol systems

摘要

Many security protocols have been shown to have serious design flaws, even a long time after their publication. For this reason, several automatic verification methods have been proposed. As far as we know, all these methods deal with the verification of mono-protocol systems. On the contrary, modern computer systems employ different security protocols in the same environment. In this paper, we present a methodology to automatically verify the security of multiprotocol systems based on model checking. We also describe its application to a multi-protocol system composed by SET (by VISA & Mastercard) and 2KP (by IBM).