A Language and a Notion of Truth for Cryptographic Properties
Simon Kramer · 2003
Motivation Protocol designers commonly specify a cryptographic protocol jointly by (1) a semi-formal description of its behaviour (local properties) in terms of protocol narrations, and by (2) an informal prescription of its intended goals (global properties) in natural language. Informal specifications present three major drawbacks: (1) they do not have a well-defined, and thus a well-understood meaning; (2) they do not allow for the verification of internal correctness (referring to an internal notion of truth), i.e., the virtue that the conjunction of local properties implies each global property, typically by means of a proof system; and (3) they do not allow for the verification of external correctness (referring to an external notion of truth requiring a formal protocol model), i.e., the virtue that a proposed implementation (protocol model) satisfies each global property, typically by means of model checking. In formal specifications of cryptographic protocols, local and global properties are expressed either explicitly as such in terms of a logical (or property-based) language, or implicitly as code, resp. as encodings in a protocol modelling (or model-based) language. Examples of such encodings are equations between instantiations of protocol schemata, and predicates defined inductively on the traces those instantiations may exhibit [1]. However, such encodings present four major drawbacks: (1) they have to be found; worse, (2) they may not even exist; (3) they are neither directly comparable with other encodings in the same or other protocol modelling languages, nor with properties expressed explicitly in terms of logical languages; and (4) they are difficult to understand because the intuition of the encoded property is implicit in the encoding. Informal language and protocol modelling languages are patently inadequate for expressing and comparing cryptographic properties. It is our belief that only a logical language equipped with an appropriate notion of truth, i.e., a cryptographic logic, will produce the necessary adequacy therefore. A number of logics have been proposed in this aim so far, ranging from ad-hoc special-purpose cryptographic logics [2, the so-called BAN-logic] and [8, a unification of several BAN-logics], over varieties of classical modal and first-order logic used for the special purpose of cryptographic protocol analysis [4, temporal modalities], [5, epistemic modalities], and [6, deontic modalities], resp. [7, first-order], to combinations thereof, e.g., [3, epistemic post-conditions]. However in our opinion and w.r.t. our understanding of adequacy, each of these logics fails to be adequate due to limitations of scope (and style), i.e., the power to express (intuitively, succinctly, and endogenously1) arbitrary cryptographic goals, and / or grain, i.e., the power to discriminate sufficient detail in the analysis of cryptographic protocols. These limitations originate in design decisions of syntactical (language-defining operators) and / or semantic (meaning-defining notion of truth) nature.