×

An integrative framework to protocol analysis and repair: Bellare-Rogaway model + planning + model checker. (English) Zbl 1148.94434

Summary: A modified version of the M. Bellare and P. Rogaway [Lect. Notes Comput. Sci. 773, 232–249 (1994; Zbl 0870.94019)] adversarial model is encoded using Asynchronous Product Automata (APA). A model checker tool, Simple Homomorphism Verification Tool (SHVT), is then used to perform state-space analysis on the automata in the setting of planning problem. The three-party identity-based secret public key protocol (3P-ID-SPK) of H. W. Lim and K. G. Paterson [“Secret public key protocols revisited”, in: Security Protocols Workshop 2006 (to appear)], which claims to provide explicit key authentication, is used as a case study. We then refute its heuristic security argument by revealing a previously unpublished flaw in the protocol using SHVT. We then show how our approach can automatically repair the protocol. This is, to the best of our knowledge, the first work that integrates an adversarial model from the computational complexity paradigm with an automated tool from the computer security paradigm to analyse protocols in an artificial intelligence problem setting – planning problem – and, more importantly, to repair protocols.

MSC:

94A62 Authentication, digital signatures and secret sharing
68Q60 Specification and verification (program logics, model checking, etc.)

Citations:

Zbl 0870.94019
PDFBibTeX XMLCite