Shapes: Surveying Crypto Protocol Runs 1
Joshua D. Guttman · 2013
Abstract. Given a cryptographic protocol, and some assumptions, can we present everything that can happen, subject to these assumptions? The assumptions may include: (i) some behavior assumed to have occurred, (ii) some keys assumed to be uncompromised, and (iii) some values assumed to have been freshly chosen. An object representing these types of information is called a skeleton. The shapes for a skeleton A are the minimal, essentially different executions that are compatible with the assumptions in A. The set of shapes for an A is frequently but not always finite. Given a finite set of shapes for A, it is evident whether a security goal such as authentication or confidentiality holds for A. In this paper, we describe a search that finds the shapes, starting from a protocol and a skeleton A. The search is driven by the challenge-response patterns formal-ized in the strand space authentication tests. 1. Initial Examples We develop here a search technique for finding the minimal, essentially different exe-cutions possible in a protocol, starting from some initial behavioral assumptions. This search gives counterexamples to false authentication and confidentiality assertions. Al-ternatively, the search proves these properties, when they hold and the search terminates, as it commonly though not universally does. We start with intuitive analyses, using Blanchet’s Simple Example Protocol [2] (see Fig. 1), and then proceed to formalize and justify them. Blanchet’s protocol SEP requires an initiator A to generate a fresh symmetric key k, sign and encrypt it for a chosen responder B, and await reception of a message {|s|}k.2 Any responder B will await a message containing a signed and encrypted k, at which point it will select a secret s to transmit encrypted with k. A strand is a finite sequence of transmissions and receptions,