Stage de deuxième année de magistère d’informatique, réalisé au laboratoire d’informatique de SRI International, Menlo Park, Californie, Etats-Unis par David Monniaux, été 1997

Plan

1 Déroulement du stage 2 1.1 Présentation du laboratoire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Remerciements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Problèmes scientifiques 4 2.1 Cryptographie et communications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Moyens de preuve employés . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

A Décision des logiques BAN et GNY 7 A.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 A.2 Knowledge sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 A.3 Generalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 A.4 BAN logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 A.5 GNY logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 A.6 Automatic analyses in BAN logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 A.7 The rules of modified GNY logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 A.8 GNY analysis of some properties of the Needham-Shroeder protocol . . . . . . . . . . . . . . 23

B Problème à protocoles entrelacés et abstraction 27 B.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 B.2 A first abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

Résumé

Les réseaux informatiques utilisent un grand nombre de protocoles, dont certains (par exemple Kerberos) à sécurité garantie par de la cryptographie. Afin de s’assurer de leur fiabilité, on aimerait prouver celle-ci formellement dans un certain modèle simplifié. En particulier, on ne s’intéressera pas aux problèmes de fiabilité des primitives cryptographiques impliquées.

Une approche peu coûteuse est celle des logiques modales de croyances adaptées à ces analyses ; elles permettent d’éliminer certains mauvaises conceptions flagrantes. Je propose une méthode systématique pour l’automatisation de ce genre de logique, que j’applique à deux logiques particulièrement connues (BAN, GNY).

La démonstration de propriétés de sécurité dans un modèle plus ambitieux est largement plus pénible. Afin d’éviter de demande un effort humain trop important, on a essayé d’utiliser le plus possible les ressources du calcul par machine ; cependant, les connaissances sur la méthodologie à appliquer sont encore faibles. Je donne une abstraction mécanisable du problème.

Partie 1

Déroulement du stage

1.1 Présentation du laboratoire

1.1.1 Environnement

La compagnie SRI International^{1}, connue auparavant sous le nom de Stanford Research Institute, est une entreprise a but non lucratif, dont les activités sont le developpement d’applications scientifiques et le conseil à des organismes privés ou gouvernementaux.

Le laboratoire d’informatique^{2} (computer science laboratory) fait de la recherche théorique et appliquée dans les domaines suivants :

– méthodes formelles et preuve automatisée de théorèmes,

– logique linéaire et théorie de la preuve,

– sécurité des systèmes informatiques,

– communications a haut débit,

– émulation de circuits intégrés.

1.1.2 Méthodes formelles

Dès les années 70, SRI a développé une série de prouveurs de théorèmes : Boyer–Moore, EHDM, et maintenant PVS. PVS^{3} est un système comprenant

– un langage de définition, permettant d’exprimer, dans un style purement fonctionnel typé les fonctions étudiées, ainsi que les axiomes supposés et les lemmes et théorèmes que l’on veut établir ;

– un prouveur interactif, basé sur la logique classique (séquents), automatisant partiellement les tâches par des tactiques, et connaissant les propriétés de base des types usuels, comme les entiers, afin de les appliquer dans des procédures de décision.

Ce système sert à l’analyse de propriétés de circuits ou de programmes. Il peut être couplé à des modelcheckers pour certaines applications.

Les activités de l’équipe se dirigent donc dans les directions de :

– développements en théorie de la preuve,

– développement du logiciel PVS et d’accessoires,

– application de méthodes formelles a différents problèmes, en particulier à l’aide du logiciel PVS.

1.2 Remerciements

Merci à John Rushby pour l’organisation du stage et l’aide sur PVS, Natarajan Shankar pour ses précieux conseils toujours pertinents, Sam Owre pour sa patience dans l’aide aux pauvres débutants, Pat Lincoln pour ses conseils, Li Gong pour ses explications complémentaires, Judith Burgess pour la solution des problèmes administratifs et matériels et le logement, Sergey Berezin et Drew Dean pour le soutien moral, et tous ceux qui ont contribué à GNU Emacs et ses modules additionnels, TEX et les programmes qui gravitent autour, L^{A}TEX^{4} et ses packages, et Objective CAML.

1. Voir http://www.sri.com.

2. Voir http://www.csl.sri.com.

3. Divers articles sur PVS, ainsi que les manuels du système, sont disponibles à http://www.csl.sri.com/pvs.

html.

4. Pour la petite histoire, j’ai rencontré Leslie Lamport à l’université de Stanford !

Partie 2

Problèmes scientifiques

2.1 Cryptographie et communications

Nous nous intéressons a des systèmes de communication ou d’authentification réputés sûrs ; par exemple, des réseaux de telephonie mobile, de paiement par carte bancaire, de micro-ordinateurs dans un réseau local. Les critères de construction de ces systèmes sont de deux catégories :

1^{o} le système doit fournir des performances (vitesse de transmission, temps de réponse) acceptables, tout en restant d’un coût raisonnable;

2^{o} le système doit être sûr. On étudie le plus souvent le second point en séparant la sécurité des primitives cryptographiques (fonctions de chiffrement, de hachage...) et la sécurité des protocoles qui les emploient. Tandis qu’on a porté une attention considérable sur la sécurité des primitives cryptographiques^{1} des protocoles publiés et utilisés présentent des fautes graves de sécurité.

Les méthodes formelles d’analyse permettent d’attaquer le problème de la preuve de sécurité suivant différents degrés de coût et de performance.

2.1.1 Logiques modales

Au bas de l’échelle des coûts, nous trouvons certaines logiques modales permettant de débusquer quelques erreurs assez facilement ; ces logiques sont essentiellement utiles lorsqu’elles donnent des résultats négatifs, car cela montre que l’on a négligé d’introduire certaines présuppositions sur le système étudié. Par exemple, la littérature ([BAN89], [GNY90]) montre comment une analyse grâce à ces logiques peut montrer que certains protocoles ne fonctionnent que sous des hypothèses fortes (par exemple, qu’une vieille communication sur le même réseau n’a pas été percée).

Les faiblesses de ces logiques sont :

– elles s’appuient sur une idéalisation parfois contestable du protocole ;

– elles ne s’intéressent qu’à des problèmes sémantiques du protocole.

D’un autre côté, ces logiques sont facilement implémentables. L’annexe A contient mes résultats sur des procédures de décision effectives pour certaines de ces logiques, dérivées d’une même méthode de transformation en un système de chaînage avant à théorie finie ; en particulier, je propose pour la première fois une procédure de décision de la logique GNY.

2.1.2 Preuve de théorèmes

Ici, nous nous intéressons à un modèle formel (i.e. mathématique) de ce qu’est un protocole et un intrus. Différents modèles peuvent être considérés.

[Pau97] considère un modèle où l’intrus contrôle le réseau et un nombre quelconque de principaux communiquent en utilisant le protocole (exécutions entrelacées ou interleaved runs). Ce modèle est très fort ; en effet, il suppose que l’intrus peut

– écouter tous les messages communiqués,

– intercepter certains messages et empêcher leur retransmission, ou les retransmettre plus tard, – émettre tout message qu’il peut constituer au

1. [Sch96], contient une description détaillée des primitives les plus courantes et des références sur leur sécurité.

vu des données qu’il a en sa possession.

Je propose dans B.1.1 un modèle général sous forme d’un système de transitions.

Les conditions exigées à l’issue du protocole sont diverses :

– certaines données confidentielles ne doivent pas entrer en possession de l’intrus,

– les principaux doivent être en possession des données correctes.

Le théorème à prouver est alors très complexe.

[Pau97] prouve des propriétés au prix d’un travail humain important et de stratégies avancées de preuve semi-automatique. [Bol97] propose plutôt de ramener le problème a un cas fini par abstraction.

Des modèles plus faibles sont proposés ; par exemple, [Bol97] considère une seule exécution du protocole en parallèle.

2.2 Moyens de preuve employés

2.2.1 Difficultés de la preuve de theorèmes, en particulier dans le cas de PVS

Le problème de décider si une formule est démontrable ou non est indécidable dans les logiques suffisamment puissantes pour exprimer ce à quoi nous nous intéressons. En conséquence, les prouveurs semi-automatisés de théorèmes^{2} sont des systèmes interactifs, où l’utilisateur pilote le programme. Les différences principales, du point de vue de l’utilisateur voulant vérifier des problèmes réels, sont surtout dans le degré d’automatisation, ou, pour parler plus pratiquement, la grosseur de l’ensemble des théorèmes que le système prouve de lui-même. La difficulté réside dans le fait que, tandis que nous basons les raisonnements mathématiques sur des définitions rigoureuses, notre pensée est guidée par l’aspect intuitif des concepts rencontrés ; par exemple, nous raisonnons intuitivement sur les entiers naturels, sans nous ramener à une definition par un type inductif avec une constante zéro et un constructeur unaire successeur . Le problème est que la machine raisonne comme cela.

Le système PVS est assez performant sur des exemples intéressants en informatique par son utilisation de procédures de décision sur les types couramment rencontrés (entiers...). Un problème est que dès que l’on sort de ces types, même si l’on reste dans des types assez intuitifs pour nous comme les permutations d’un ensemble fini, par exemple, le système devient très maladroit.

La difficulté principale vient du problème d’instancier des variables dont on ne peut connaître a priori la valeur. Par exemple, l’axiome ∀x, A(x) ⇒ B, indique que pour démontrer B, on peut démontrer A(x) pour un certain x. Mais quel x ? PVS a quelques heuristiques à ce sujet, mais cela reste un problème ennuyeux y compris dans des cas où l’instanciation est intuitive pour un humain.

2.2.2 Chaînage avant

Étant donné la simplicité des logiques d’analyse de protocole, j’ai cherché à nous affranchir de ces contraintes en construisant des systèmes de chaînage avant (voir annexe A) dont la théorie engendrée est finie et facilement énumérable.

2.2.3 Abstraction

Pour le cas plus complexe du modèle de protocoles entrelacés (annexe B), j’essaye de trouver une abstraction finie du problème. Le théorème abstrait est alors prouvé — s’il est vrai, bien entendu — par model-checking. L’abstraction, bien choisie, fait que cela implique le théorème concret.

L’abstraction dans un système à transitions d’états^{3} est une technique par laquelle on regroupe les états concrets sur des états abstraits. On peut considérer une fonction des états concrets vers les états abstraits (par exemple, envoyer ℤ_{−} sur un état abstrait Z-*, 0 sur 0 et ℤ_{+} sur Z+*. Plus généralement, on considère une relation entre les états concrets et les états abstraits. Cela est particulièrement intéressant avec les états abstraits organisés en réseau ; ainsi, on pourrait envoyer 0 sur à la fois 0, Z-, Z+. Z- est alors la borne supérieure de 0 et Z- *. C’est ce que nous faisons dans B.2 avec un treillis de clôtures.

2. Citons, outre PVS, Coq [BBC^{+}97], Isabelle, HOL...

3. Patrick Cousot notamment a développé l’analyse de programmes par interprétation abstraite. Voir [Cou97] pour une introduction.

Je propose une abstraction finie du problème de n protocoles (définis de façon raisonnable) lancés avec entrelacement des transmissions. Le problème de cette abstraction est qu’elle peut être trop grossière pour certains protocoles ; de plus, il reste le problème de la démonstration pour n quelconque.

2.2.4 Model-checking

Lorsque le domaine sémantique dans lequel nous analysons le système est fini (après abstraction, si besoin est), et d’un cardinal raisonnable, nous pouvons utiliser des techniques de model-checking, qui cherchent à vérifier les formules par exploration systématique de l’espace d’état. Évidemment, ces méthodes nécessitent des optimisations avancées afin de rester en un temps acceptable y compris sur des domaines très grands.

[MCJ97] illustre l’utilisation du model-checker SMV pour l’analyse de protocoles cryptographiques. Cependant, il semble que le problème du non-déterminisme infini de l’intrus (cf annexe B) a été négligé dans cet article.

Annexe A

Texte du rapport technique sur la décision des logiques BAN et GNY

A.1 Introduction

A.1.1 The issues

Most real-life networks are bound to be inherently insecure. The communication media might be wiretapped; some of the communicating machines might get compromised, and the data they hold fall into the hand of intruders. We see here two essential tasks: users’ data transmitted at all time mustn’t be decipherable, and compromission of part of the network architecture or machines at an instant in time shouldn’t yield risks later or for other machines.

Cryptographic protocols address those needs. Those protocols are built from cryptographic primitives (symmetric encryption schemes such as DES or RC4, public-key schemes such as RSA, hash functions such as MD5; see [Sch96] for general information on those topics) the security of which can be attacked by cryptanalysis. The methods used here assume the security of the primitives; we shall only deal with attacks on the protocol itself rather than the primitives involved.

Many other concerns interfere with the design of cryptographic communication protocols. Ease of networking in real environments containing hundreds of machines is to be taken care of; failures in machines must be dealt with; operating systems must be taken into account … and efficiency must be met. Performance concerns deter the protocol designer from using too many computationnally expensive encryption steps^{1}. For those reasons, many protocols are proposed. Claims are made about them, such as “at the end of this round, this machine knows that it must use that key to communicate with that other machine”.

Many approaches to the problem of analysing those protocols, finding bugs in them or proving some safety properties on them have been proposed. Some of them, as proposed in [Pau97, Bol97], tackle the very general task of ensuring that in no circumstance critical bits of information can leak to an intruder, going as far as considering multiple interleaved runs^{2}. Simpler formalisms include modal logics of belief, as outlined in [BAN89] and improved in [GNY90]. (Partially) automated systems for protocol analysis have been proposed [Bra95, Bra96, Pau97, CS96, Sch97, KW96]. Those logics analysis the protocol in an abstract model, on properties such as “after this step, the machine A ‘knows’ that the key K_{ab} is a secret key to be used between it and B”; reasoning steps are such as “if I get a message encrypted with a secret key only myself and A know, then that messages must be originating from myself or A”. We propose here a general method to decide several of those logics.

(see [Sch96] for details) involve especially long computations such as taking powers in ℤ/nℤ. In that case, it is really important that the number of encryptions used be minimal, if the protocol is to be used with a high frequency or on a slow computation unit such as a smart card.

2A run of the protocol is an instance of the use of the protocol. For instance, if the protocol is a safe mail transmission protocol, each sending of a mail constitutes a run of the protocol.

1Some cryptographic primitives, such as RSA encryption

A.2 Knowledge sets

A.2.1 The problem

An idealization of reality

In the general problem of analysis of cryptographic protocols, one has to define the potential knowledge of the intruder. An approach that sticks to reality would be to define encrypted data type as they are in reality (eg as, for instance, 64-bit data). The problem with that approach is that in that a naive formalization of it, the intruder always wins. Those types being finite, the intruder “possesses” all the elements, and analysis will fail for the reason that the intruder can simply guess the correct value. Correct formalizations would include a notion of probability; for instance, while it is true that an intruder may guess a 64-bit value, the probability of that, 2^{−64}, is so small that it is close to zero. Alas, such probabilistic analysis tends to be quite complex.

We therefore use an idealized model. Pieces of data are considered as terms over an algebra of constructors, maybe quotiented by some simplifications (such as encryption then decryption with the same key yields the original piece of data). The universe of data that an intruder possesses is the closure of what it receives by some rules. The intruder is not allowed to guess anything; it can only construct what it can from the pieces of data it received.

An objection to that model is that the intruder is still allowed to “guess” which piece of data is to be sent in the whole universe it can compute. For instance, if the intruder possesses X, and the secret is X concatenated with itself n times, in which n is a secret integer, then our model says that the intruder possesses the secret. That supposes he can somehow guess n. This is not a real problem in the case of cryptographic protocols defined in the usual ways: all the data is represented as “small” terms, and no data is “hidden” in such ways that circumvent the model.

Formal definitions

We want an algorithm that, given a (finite) initial set I of terms, taken on an algebra the signature of which contains:

• pairing (•, •)

• encryption {•}_{•}

and a term t, computes whether t is in the closure I by the following rules — which we note I ⊢ t :

• construction rules

– pairing \frac{X Y}{(X, Y)},

– encryption \frac{X K}{\{X\}_{K}} .

• destruction rules

– splitting \frac{(X, Y)}{X Y},

– decryption \frac{\{X\}_{K} K}{X} ,

We here consider symmetric^{3} encryption; publickey^{4} encryption could be considered by extending the approach.

An easy approach is described in [Bol97]. It consists in computing the closure I′ of I by the “decomposition” operations (splitting and decryption), which is finite. Then, determining whether

3An encryption scheme is said to be secret-key or symmetric if the same key can be used for encryption and decryption. Such systems include DES, RC4 etc …, see [Sch96]. The main problem with such systems is that they need at least some secure initial transmission of data to take place apart from them: one has to get the key to both ends of the transmission.

4An encryption scheme is said to be public-key or asymmetric if keys are organized in couples (p, s). Messages encrypted with p can only be decrypted with s. An user possessing s, the private key, and keeping it secret may publish p, the public key; other people may then send messages to him, encrypted with p, knowing that they can’t be decrypted by any other person. The RSA cryptosystem (see [Sch96]) also has the interesting property that the public key decrypts messages encrypted with the private key, but only the private key allows encrypting meaningful messages. Thus the private key may be used as an authentication secret: messages meaningfully^{5}encrypted with it, which can be checked by anybody possessing the (published) public key, may then believe they were sent by the owner of the private key.

5We mean by meaningfully encrypted that, though an intruder may output any kind of data and pretend it is the encryption of something, the format of the expected data has enough redudancy that it excludes random data that would be the result of the decryption of such.

a term belongs in C by backward-chaining^{6} on the “composition” operations (pairing and encryption). That method is based on the following theorem:

I ⊢ t ⟺ I ⊢_{d} I′ ⊢_{c} C

where ⊢ denotes derivation by all the rules, ⊢_{d} decomposition and ⊢_{c} composition (see [Bol97] for a proof — it is basically a cut-free, or normalization, theorem). Sadly, this theorem only holds in the framework of [Bol97], where keys can’t have a structure (that is, can’t be composite). For instance, if we derive

\begin{matrix}\{X\}_{(K,K′)} & \begin{matrix}K & K′ \\ (K, K′) \end{matrix} \\ X \end{matrix},

we must do one composition step (pairing) before one decomposition step (decryption).

A.2.2 Our approach

We now propose a decision procedure for the more general case where we allow keys to be composite.The idea is that if we reach some data encrypted with some key, we try to build up that key. That form of search can of course be achieved by special tactics; for the sake of ease and clarity of proofs, and implementation in general-purpose forwardchaining^{7} systems, we prefer to implement that in the logic itself. We add another symbol, goal. ⊡X means qualitatively that “we would like to prove X”. We define ⊢′ by the following rules:

• \frac{X Y ⊡ (X, Y)}{(X, Y)},

\frac{H_{1} … H_{n}}{C}

\frac{H_{1} … H_{n}}{C}

• \frac{(X, Y)}{X Y},

• \frac{\{X\}_{K} K}{X} ,

• \frac{X K ⊡ \{X\}_{K}}{\{X\}_{K}} ,

• \frac{⊡ (X, Y)}{⊡X ⊡ Y} ,

• \frac{\{X\}_{K}}{⊡K}
• \frac{⊡ \{X\}_{K}}{⊡X ⊡ K}

We then state

Theorem 1 For all set Γ of hypotheses and formula t (on the original algebra),

Γ ⊢ t ⟺ Γ, ⊡t ⊢′ t.

The proof is given more generally in the next section.

Here is an example: K, K′, {X}_{(K,K′)} ⊢ X is reached by

\begin{aligned}\{X\}_{(K,K′)} & \begin{matrix}{⊡ \{X\}_{(K,K′)} \atop ⊡ (K, K′)} & K & K′ \\ (K, K′) \end{matrix} \\ & X \end{aligned}.

Theorem 2 Forward-chaining^{8} the rules of ⊢′ is a decision procedure.

It’s a consequence of the preceding theorem and the following lemma:

Property 3 For all rule

\frac{H_{1} ⋯ H_{n}}{C}

of ⊢′,

M(C) ≤ max{M(H_{1}), …, M(H_{n})} − 1.

The measure M is defined inductively in tab. A.1. The theorem ensures the correctness and completeness of the method, and the lemma ensures the termination.

8That is, generating the whole theory by repeatedly trying to apply each rule, till nothing new is produced, then checking whether the desired formula is in that theory.

6We call backward-chaining rules rules of the form in which all the variables in the hypotheses are found in the conclusion. In a backward-chaining system, when one wants to check whether a formula is provable, he tries to match that formula against all such conclusions; if a match succeeds, he tries to prove the hypotheses of the rules he used.

7We call forward-chaining rules rules of the form in which all the variables in the conclusion C are found in the hypotheses H_{1} … H_{n}. Such systems allow the computation of the whole inferrable theory by repeatedly attempting to unify the hypotheses of a rule with some already proved formulas, and if possible adding its conclusion with the correct variable instanciations.

\begin{matrix}t & M(t) \\ α & 1 \\ (X, Y) & max\{M(X), M(Y)\} + 1 \\ \{X\}_{K} & max\{M(X), M(K)\} + 1 \\ ⊡X & M(X) + 1 \end{matrix}

Table A.1: The measure M for knowledge set derivations.

A.3 Generalization

We try to generalize that method to more complex systems of rules. We still use the same idea that all destruction may take place before all construction. The only problem with that and composite keys is that these keys may need to be constructed. We trigger the construction of only the keys we need to achieve the destruction.

More generally, we deal with two categories of rules^{9}:

• construction rules, in which all the variables of the hypothesis are found in the conclusion (those rules are automatically backwardchainable);

• destruction rules, in which all the variables of the conclusion found in the hypothesis (those rules are automatically forwardchainable); for those rules, we distinguish the data hypotheses (which can be one or more) and the optional key hypotheses; the variables in the key hypotheses are a subset of those in the data hypotheses.

A constraint for our method to work is that it must always be possible to find a normal derivation; that is, for all set of hypotheses Γ and formula t so that Γ ⊢ t, there must be a derivation so that there’s no construction rule to be used as the root rule of the sub-derivation for a data hypothesis of a destruction rule.^{10}

Informally, that means that you must be able to derive anything that is derivable without having to construct something and destruct it afterwards; for instance, in

\begin{matrix}{(X, Y) \atop X} & {(X, Y) \atop Y} \\ (X, Y) \end{matrix}

we construct a pair just to destruct it afterwards. Our transformation turns the construction rule

\frac{H_{1} ⋯ H_{n}}{C}

into a pair

\frac{⊡C H_{1} ⋯ H_{n}}{C}

and

\frac{⊡C}{⊡H_{1} ⋯ ⊡ H_{n}}

and adds to the destruction rule

\frac{D_{1} ⋯ D_{m} K_{1} ⋯ K_{n}}{C} ,

where the one or more D_{i} are data hypotheses and the zero or more H_{i} are key hypotheses, the triggering rule

\frac{D_{1} ⋯ D_{m}}{⊡K_{1} ⋯ ⊡ K_{n}} .

See A.2.2 for examples.

Theorem 4 Such a system verifies for all set of hypotheses Γ and formula t,

Γ ⊢ t ⟺ Γ, ⊡t ⊢′ t;

all t such a Γ ⊢ t can be reached by forwardchaining^{11} on ⊢′ .

The second claim is evident, given the structure of the rules. The right-to-left way of the first claim comes from the rules whose conclusions are nongoal formulas are rules from the original system,

ble yields a normal derivation. This is the case of the knowledge sets and BAN logic. However, this constraint is unecessarily strong, and for instance fails to capture logics where this condition is not true for all construction-destruction pairs, but where the remaining pairs can be transformed into a destruction rule. such as GNY logic (see A.5.2). We call that later condition the strong normal derivation property.

11Termination of the forward-chaining strategy may be ensured using a step-decreasing measure property, as we do on our examples.

9This partition of the set of rules into two such categories is very similar to that of [KW96], where they are called respectively growing and shrinking rules. We developped our framework independently of the cited work, of which we became aware shortly afterwards.

10A stronger constraint is that when a construction rule is used to produce a data hypothesis of a destruction rule, both rules can be removed (i.e. it is never necessary to construct some object to split it up afterwards); doing so until impossi-

weakened by adding extra hypotheses. The other way is a consequence of the following lemma:

Lemma 5 If Γ ⊢ t then ⊡t, Γ ⊢′ t; we then even have t ⊢′ t if there exists a normal derivation Γ ⊢ t that doesn’t end with a construction rule.

Proof by induction on the structure of a normal derivation of Γ ⊢ t :

• for axioms, it’s evident;

• if the bottom rule is a construction rule

\frac{H_{1} ⋯ H_{n}}{t}

as we have ⊡t we can apply the corresponding rule

\frac{⊡t H_{1} ⋯ H_{n}}{t}

at the bottom of the derivations of ⊡H_{i}, Γ ⊢′ H_{i} of the induction hypothesis; the ⊡H_{i} are derived using

\frac{⊡C}{⊡H_{1} ⋯ ⊡ H_{n}};

• if the bottom rule is a destruction rule

\frac{D_{1} ⋯ D_{m} K_{1} ⋯ K_{n}}{t}

then for any i the sub-derivation of D_{i} is normal and doesn’t end with a construction rule (we act on a normal derivation); then we have Γ ⊢′ D_{i}; we then use the triggering rule

\frac{D_{1} ⋯ D_{m}}{⊡K_{1} ⋯ ⊡ K_{n}}

then the induction hypothesis to get the ⊡K_{i}, Γ ⊢′ K_{i}; we apply the original destruction rule at the bottom of those.

A.4 BAN logic

A.4.1 Description

The simple BAN logic, named after its proponents, Burrows, Abadi and Needham (see [BAN89]), though not very powerful, is easy to use. It deals with beliefs that principals (i.e. machines communicating on the network) can hold about the status of the distribution of communication keys.

Formula Meaning
P |≡ X  P believes X
P ◁ X  P sees X
P |∼ X  P once said X
P |⇒ X P has jurisdiction over X
♯(X)  X is fresh
P ⟷^{K} Q K is a symmetric encryption key

for P and Q (which commute)

↦^{+P} P  P has K as public key
P ⟷^{X} Q X is a secret shared by

by P and Q (which commute)

{X}_{K}  X encrypted with K
{X}_{K^{−1}} X encrypted with the private key

corresponding to the public key K

⟨X⟩_{Y}  X combined with Y
(X, Y) pair of X and Y

Table A.2: The meaning of the symbols of BAN logic. P and Q are principals, X and Y formulas, K a key.

Following the works of [CS96], we propose an actual decision procedure for an useful fragment of the logic, and a proof of its adequacy.

The BAN logic (see [BAN89]) rules, on the symbols defined in A.4.1, are the following:

• Message-meaning rules

– \frac{P |≡ Q ⟷^{K} P P ◁ \{X\}_{K}}{P |≡ Q|∼ X}

– \frac{P |≡ ↦^{+Q} Q P ◁ \{X\}_{K^{−1}}}{P |≡ Q|∼ X}

– \frac{P |≡ Q ⟷^{Y} P P ◁ ⟨X⟩_{Y}}{P |≡ Q|∼ X}

• Belief production rules

– \frac{P |≡ ♯(X) P |≡ Q|∼ X}{P |≡ Q|≡ X}
– \frac{P |≡ Q|⇒ X P |≡ Q|≡ X}{P |≡ X}

• Conjunction of beliefs creating and splitting rules^{12}

– \frac{P |≡ X P |≡ Y}{P |≡ (X, Y)}

12We could extend these rules into a scheme of rules deal-

– \frac{P |≡ (X, Y)}{P |≡ X}  \frac{P |≡ (X, Y)}{P |≡ Y}
– \frac{P |≡ Q|≡ X P |≡ Q|≡ Y}{P |≡ Q|≡ (X, Y)}
– \frac{P |≡ Q|≡ (X, Y)}{P |≡ Q|≡ X}  \frac{P |≡ Q|≡ (X, Y)}{P |≡ Q|≡ Y}

• Other conjunction splitting rules

– \frac{P |≡ Q|∼ (X, Y)}{P |≡ Q|∼ X}  \frac{P |≡ Q|∼ (X, Y)}{P |≡ Q|∼ Y}
– \frac{P ◁ (X, Y)}{P ◁ X}  \frac{P ◁ (X, Y)}{P ◁ Y}

• Message interpretation rules

– \frac{P ◁ ⟨X⟩_{Y}}{P ◁ X}
– \frac{P |≡ Q ⟷^{K} P P ◁ \{X\}_{K}}{P ◁ X}
– \frac{P |≡ ↦^{+Q} Q P ◁ \{X\}_{K^{−1}}}{P ◁ X}
– \frac{P |≡ ↦^{+P} P P ◁ \{X\}_{K}}{P ◁ X}

• Freshness extension rule

\frac{P |≡ ♯(X)}{P |≡ ♯((X, Y))}  \frac{P |≡ ♯(Y)}{P |≡ ♯((X, Y))}

A.4.2 Transformation

Apply our technique, we get the following set of rules:

• Message-meaning rules

– \frac{P |≡ Q ⟷^{K} P P ◁ \{X\}_{K}}{P |≡ Q|∼ X}

– \frac{P |≡ ↦^{+Q} Q P ◁ \{X\}_{K^{−1}}}{P |≡ Q|∼ X}

– \frac{P |≡ Q ⟷^{Y} P P ◁ ⟨X⟩_{Y}}{P |≡ Q|∼ X}

• Belief production rules

– \frac{P |≡ ♯(X) P |≡ Q|∼ X}{P |≡ Q|≡ X}

provides.

– \frac{P |≡ Q|∼ X}{⊡P |≡ ♯(X)}
– \frac{P |≡ Q|⇒ X P |≡ Q|≡ X}{P |≡ X}
– \frac{P |≡ Q|⇒ X}{⊡P |≡ Q|≡ X}

• Conjunction of beliefs creating and splitting rules

– \frac{⊡P |≡ (X, Y) P |≡ X P |≡ Y}{P |≡ (X, Y)}
– \frac{P |≡ (X, Y)}{P |≡ X P |≡ Y}
– \frac{⊡P |≡ (X, Y)}{⊡P |≡ X ⊡ P |≡ Y}
– \frac{⊡P |≡ Q|≡ (X, Y) P |≡ Q|≡ X P |≡ Q|≡ Y}{P |≡ Q|≡ (X, Y)}
– \frac{P |≡ Q|≡ (X, Y)}{P |≡ Q|≡ X P |≡ Q|≡ Y}
– \frac{⊡P |≡ Q|≡ (X, Y)}{⊡P |≡ Q|≡ X ⊡ P |≡ Q|≡ Y}

• Other conjunction splitting rules

– \frac{P |≡ Q|∼ (X, Y)}{P |≡ Q|∼ X P |≡ Q|∼ Y}
– \frac{P ◁ (X, Y)}{P ◁ X P ◁ Y}

• Message interpretation rules

– \frac{P ◁ ⟨X⟩_{Y}}{P ◁ X}

– \frac{P |≡ Q ⟷^{K} P P ◁ \{X\}_{K}}{P ◁ X}

– \frac{P |≡ ↦^{+Q} Q P ◁ \{X\}_{K^{−1}}}{P ◁ X}

– \frac{P |≡ ↦^{+P} P P ◁ \{X\}_{K}}{P ◁ X}

• Freshness extension rules

– \frac{⊡P |≡ ♯((X, Y)) P |≡ ♯(X)}{P |≡ ♯((X, Y))}
– \frac{⊡P |≡ ♯((X, Y)) P |≡ ♯(Y)}{P |≡ ♯((X, Y))}

ing with conjunctions of beliefs through any level of •|≡ • indirection, as the “rationality” rule of GNY (see [GNY90])

\begin{matrix}f & M(f) \\ P |≡ X & M(X) + 1 \\ P ◁ X & M(X) + 3 \\ P |∼ X & M(X) + 2 \\ P |⇒ X & M(X) + 3 \\ ♯(X) & M(X) \\ P ⟷^{K} Q & 1 \\ ↦^{+P} P & 1 \\ P ⟷^{X} Q & 1 \\ \{X\}_{K} & 1 \\ \{X\}_{K^{−1}} & M(X) + 1 \\ ⟨X⟩_{Y} & max\{M(X), M(Y)\} + 1 \\ (X, Y) & max\{M(X), M(Y)\} + 1 \\ ⊡X & M(X) + 1 \end{matrix}

Table A.3: The definition of M for BAN logic.

– \frac{⊡P |≡ ♯((X, Y))}{⊡P |≡ ♯(X) ⊡ P |≡ ♯(Y)}

The same result as for knowledge sets hold, following from the general theorem proved in the precedent section and a well-chosen measure (see tab. A.4.2). Applications of this method on the examples from [BAN89] are given in appendix A.6.

A.4.3 Implementation

We implemented a preprocessor, taking BAN-like code as input and outputting source for L^{A}TEX and for the PVS theorem prover^{13}. Then, using a forward-chaining strategy in PVS, we prove automatically all the provable goals. On unprovable ones, the strategy halts with all it could prove, of which the user may get a glimpse of the missing assumption; the user then has to track the error, usually a typing error or too weak assumptions. The “goal” statements forward-chained by the system may be useful in that task, because they are formulae that would be interesting to prove.

For the humor note, our system was actually very good at catching typos in the description of the protocols.

As we noted, we had to instantiate the BAN quantifiers. Most of the time it was obvious (along the lines of A ⟷^{K} B becoming A ⟷^{K_{ab}} B). That’s why we don’t thing the omission of quantifiers is really a problem, according in our experience with the protocols.

A.5 GNY logic

A.5.1 Definitions

The GNY logic, named after its authors, Li Gong, Roger Needham and Raphael Yahalom is a logic of belief similar to BAN, but which addresses some deficiencies in that latter one. Again, we won’t give it an extensive review and refer the reader to [GNY90] ; see also Li Gong’s PhD thesis [Gon90].

The symbols for that logic are summarily described in tab. A.4 and the rules listed in appendix A.7. An additionnal rule is the rationality rule: all the rules of the logic may be applied with any preceding chain of belief modality. That is, for all rule

\frac{H_{1} … H_{n}}{C}

and new principal variable name P, we have a rule

\frac{P |≡ H_{1} … P |≡ H_{n}}{P |≡ C} .

We consider the closure of the rules by this metarule.

The encryptions considered have the following properties:

• {{X}_{K}}_{K}^{−1} ≡ X

• {{X}_{+K}}_{−K} ≡ X

A.5.2 Adding some extra rules

The original GNY logic does not match the normal form criterion of A.3 because of the simplifications possible with encryption (see the former paragraph). For instance, we have

\begin{matrix}P ∋ K & P ∋ \{X\}_{K} \\ P ∋ \{\{X\}_{K}\}_{K}^{−1} \end{matrix} P6 P ∋ X simplification

That is, we sometimes have to construct the decryption of a piece of data just to apply a (destructive) simplification rule. We add a rule P6’

13Any forward-chaining system will do. We implemented an efficient forward-chaining tactic in PVS for that task.

Symbol  Meaning

Beliefs and conveyance

P |≡ X  P believes X
P ◁ X  P is told X
P ∋ X  P possesses X
P |∼ X  P once conveyed X

Properties of formulae

♯(X)  X is fresh
ϕ(X)  X is recognizable

Keys and secrets

P ⟷^{S} Q  S is a secret^{a} shared by P and Q
↦^{+P} P  +K is a public key of P ’s

Message constructors

{X}_{K}  X encrypted with K^{b}
{X}_{K}^{−1}  X decrypted with K^{c}
(X, Y)  the pair of X and Y

Jurisdiction

P |⇒ X  P has jurisdiction over X
P |⇒ P |≡ ⋆ P is honest and competent
(X⇝C)  X leading to C

Detection of replays

⋆X  X was not originated here

aShared secrets are most often shared symmetric keys. bK may here be either a symmetric, a public (+K) or a

private key (−K).

cK here must be a symmetric key. Decryption of {X}_{+K} is done by encrypting it with −K.

Table A.4: The meaning of the symbols of GNY logic, where P and Q range over principals, X and Y over formulas, K over keys; +X and −X are respectively the public and the private keys in a pair. that stands for the former derivation. We add similar rules in similar other cases, making up the ⊢′ derivation system.

Calling ⊢_{≡} the original GNY logic modulo the encryption simplifications, ⊢_{+} our augmented derivation system, and simplified formulae those on which no more left-to-right ≡ rewritings can be made, we have the following:

Property 6 For all set Γ of simplified hypotheses, all formula t, Γ ⊢_{≡} t if and only if Γ ⊢_{+} t.

A.5.3 Transformation  into  a

forward-chaining system

We divide our rules according to the classification laid out in A.3; equivalence rules are considered as a special case of destruction rules. We then apply the transformation laid out in A.3, making up the ⊢′_{+} system.

We first define a measure^{14} M over the formulae of this logic, according to tab. A.5. This measure satisfies the following strict decrease property:

Property 7 For all rule

\frac{H_{1} ⋯ H_{n}}{C}

of ⊢′_{+}, except the equivalence rules, we have:

M(C) ≤ max{M(H_{1}), …, M(H_{n})} − 1.

That property implies the following:

Lemma 8 Throughout the non-equivalence steps of a derivation, the length of the belief modality chain decreases.

We propose the following strategy to decide quantifier-free GNY logic: forward-chain all rules of ⊢′_{+} until no new derived formula gets added.

Theorem 9 This strategy is a decision procedure.

M(T (t_{1}, …, t_{n})) = α_{T} + ∑_{i} M(t_{i})

14The definition of that measure was done manually; but one could have automated that step by looking for coefficients α_{T} defining a measure M so that for all constructor T, of arity n, and so that property 7 holds. It amounts to generating a set of linear inequalities (one per rule) in the unknown α_{T} and solving it.

t  M(t)

Beliefs and conveyance

P |≡ X  M(X)
P ◁ X  20 + M(X)
P ∋ X  M(X)
P |∼ X  3 + M(X)

Properties of formulae

♯(X)  2 + M(X)
ϕ(X)  M(X)

Keys and secrets

P ⟷^{S} Q  0
↦^{+P} P  0
+K  0
−K  0

Message constructors

{X}_{K}  3 + M(C) + M(K)
{X}_{K}^{−1}  3 + M(C) + M(K)
(X, Y)  1 + M(X) + M(Y)
F (X, Y) 2 + M(X) + M(Y)
H(X)  2 + M(X)

Jurisdiction

P |⇒ X  1 + M(X)
P |⇒ P |≡ ⋆ 0
(X⇝C)  M(C)

Detection of replays

⋆X  1 + M(X)

Proof direction

⊡X  1 + M(X)

Table A.5: The measure M used, defined inductively on the formulae.

• it terminates, since

– there exists a finite number of rules that can be applied, since there is a finite number of original rules and there’s a upper bound on the depth of the modality chains concerned by the rationality rule, following from lemma 8;

– the number of rules that can be applied in such a derivation is bounded because:

∗ the number of non-equivalence steps is, because of property 7;

∗ the number of equivalence steps is, because repeatedly applying equivalence rules from an initial formula yields to a finite set of derived formulae; our system can’t derive already derived formulae;

• it’s complete and correct, following from property 6 and theorem 4.

A.5.4 A practical implementation

Any sufficiently fast and convenient forwardchaining engine would do; however, as we didn’t have that kind of tool available at the time we did that work, we quickly implemented such an engine for our problem.

Transformations

Internally, we use forward-chaining on the ⊢′_{+} rules. When attempting to decide whether Γ ⊢ t, the algorithm converts the problem into Γ, ⊡t ⊢′_{+} t and tries to solve it.

A side-effect of this transformation is that in the case of failure, the system may give some crude clues as what extra assumptions would have been needed: just collect the formulae f so that f ≠ t and ⊡f but not f have been derived.

Avoiding combinatorial explosion

In this paragraph, we don’t consider the rationality rule.

Implementing a working forward-chaining strategy for this problem is not as trivial as it seems. For instance, trying all possible rules in the fashion that to try a n-ary rule you match it against all the

do

for all rule R having d data hypotheses

k key hypotheses

do for all d-uple D of “old” formulae do

if D matches the data hypotheses pattern then

if the key hypotheses are in

the “old” formulae then put the conclusions into

the “new” formulae

add the “new” formulae that were not already in the “old” formulae to the “old” formulae

until no more formulae are added

Figure A.1: Practical GNY logic decision procedure.

n-uples of already derived formulae, until it ends, leads to prohibitive costs (in our case, n = 6, which makes the number of matchings grow in D^{7}, where D is the number of derivable formulae).

A first optimization we tried was based on the fact that one needn’t test all possible n-uples, but only ones containing at least one “new” formula; that is, a formula made during the last application of the rules. This is not sufficient, since it reduces only to d^{6} …

Our implementation is based on the fact that to instanciate all the variables in a rule, you needn’t consider all the hypotheses; especially, in the modified versions of the construction rules, only one “goal” hypothesis suffices; in the destruction and trigger rules, only the data hypotheses are needed. In the GNY logic, there are at most two data hypotheses. Our algorithm is in fig. A.1.

To refine that algorithm even more, the pattern matching over d-uples is replaced by d successive pattern matchings, and any failure of one the k searches ends the search process with a negative answer.

Such an algorithm is at most in D^{d+1}(log D)^{k}.

The rationality rule

The rationality rule can be implemented by a recursive call: if a formula P |≡ X is present, call the forward-chaining algorithm on all the formulae whose root are P |≡ • or ⊡P |≡ • .

A translator

Instead of doing all the translation job from rules to program by hand, which would have been very tedious and prone to random and hard to catch typos, we preferred to program a translator from the set of rules to the target programming language to build the inference engine. That way, the only part that is subject to random typos is the relatively small set of rules; errors in the translator would result in systematic errors in the set of effectively applied rules and would get spotted. This translator outputs Objective CAML^{15} code, but it would be easily adaptable to any strongly typed functional programming language.

The resulting code, along with some support modules (lexer/parser, pretty-printer …) is then compiled and makes a protocol analysis tool. A sample run is given in appendix A.8, on which we measured the following computation times:

Machine / CPU  runtime system
native bytecode
SparcStation 20 50 MHz  3.1  11.9
P6  200 MHz  0.6  3.0

The program

As in the sample shown in appendix A.8, our program takes an input of assumptions, then of protocol steps (which are turned into GNY formulas) and of desired conclusions. The program then tests each of the conclusions, and reports a proof in cases of success. In cases when the conclusion is unreachable, it outputs a hint to extra needed assumptions as described in A.5.4.

A.5.5 Other possible implementation

Again, any fast-forward chaining system will do. We considered adding a back-end to the translator into a controlled-rewriting system,^{16}taking advan-

15Objective CAML is an implementation of the CAML dialect of the ML functional programming language, de-

velopped at INRIA. See http://pauillac.inria.fr/ocaml/

for more information.

16For instance, the system Maude (see [CELM96]). We tested the possibility of it on the simpler problem of knowledge sets.

A.6. AUTOMATIC ANALYSES IN BAN LOGIC 17

tage of the advanced pattern-matching algorithms of such systems, but adequate performance from our cruder implementation had us conclude that such step wasn’t necessary.

A.6 Automatic analyses in BAN logic

A.6.1 The Otway-Rees protocol

Protocol

\begin{matrix}1 & A → B & \{(Na, Nc)\}Kas \\ 2 & B → S & (\{(Na, Nc)\}Kas , \{(Nb, Nc)\}Kbs ) \\ 3 & S → B & (\{(Na, A \underleftrightarrow{Kab} B, B |∼ Nc)\}Kas , \{(Nb, A \underleftrightarrow{Kab} B, A|∼ Nc)\}Kbs ) \\ 4 & B → A & \{(Na, A \underleftrightarrow{Kab} B, B |∼ Nc)\}Kas \end{matrix}

Assumptions

A|≡ A \underleftrightarrow{Kas} S S |≡ A \underleftrightarrow{Kas} S B |≡ B \underleftrightarrow{Kbs} S S |≡ B \underleftrightarrow{Kbs} S S |≡ A \underleftrightarrow{Kab} B A|≡ S |⇒ A \underleftrightarrow{Kab} B B |≡ S |⇒ A \underleftrightarrow{Kab} B A|≡ S |⇒ B |∼ Nc B |≡ S |⇒ A|∼ Nc A|≡ ♯(Na) B |≡ ♯(Nb) A|≡ ♯(Nc)

Goals

A|≡ A \underleftrightarrow{Kab} B B |≡ A \underleftrightarrow{Kab} B A|≡ B |≡ Nc B |≡ A|∼ Nc

A.6.2 The Needham-Shroeder shared-keys protocol

Protocol

\begin{matrix}1 & S → A & \{(N_{a}, A ⟷^{K_{ab}} B, ♯(A ⟷^{K_{ab}} B), \{A ⟷^{K_{ab}} B\}_{K_{bs}})\}_{K_{as}} \\ 2 & A → B & \{A ⟷^{K_{ab}} B\}_{K_{bs}} \\ 3 & B → A & \{(N_{b}, A ⟷^{K_{ab}} B)\}_{K_{ab}} \\ 4 & A → B & \{(N_{b}, A ⟷^{K_{ab}} B)\}_{K_{ab}} \end{matrix}

Assumptions

A|≡ A ⟷^{K_{as}} S

B |≡ B ⟷^{K_{bs}} S

S |≡ A ⟷^{K_{as}} S

S |≡ B ⟷^{K_{bs}} S

S |≡ A ⟷^{K_{ab}} B

A|≡ S |⇒ A ⟷^{K_{ab}} B

B |≡ S |⇒ A ⟷^{K_{ab}} B

A|≡ S |⇒ ♯(A ⟷^{K_{ab}} B)

A|≡ ♯(N_{a}) B |≡ ♯(N_{b})

S |≡ ♯(A ⟷^{K_{ab}} B)

B |≡ ♯(A ⟷^{K_{ab}} B)

Goals

A|≡ A ⟷^{K_{ab}} B

B |≡ A ⟷^{K_{ab}} B

A|≡ B |≡ A ⟷^{K_{ab}} B

B |≡ A|≡ A ⟷^{K_{ab}} B

A.6.3 The Kerberos protocol

Protocol

\begin{matrix}1 & S → A & \{(T_{s}, A ⟷^{K_{ab}} B, \{(T_{s}, A ⟷^{K_{ab}} B)\}_{K_{bs}})\}_{K_{as}} \\ 2 & A → B & (\{(T_{s}, A ⟷^{K_{ab}} B)\}_{K_{bs}} , \{(T_{a}, A ⟷^{K_{ab}} B)\}_{K_{ab}}) \\ 3 & B → A & \{(T_{a}, A ⟷^{K_{ab}} B)\}_{K_{ab}} \end{matrix}

Assumptions

A|≡ A ⟷^{K_{as}} S

B |≡ B ⟷^{K_{bs}} S

S |≡ A ⟷^{K_{as}} S

S |≡ B ⟷^{K_{bs}} S

S |≡ A ⟷^{K_{ab}} B

A|≡ S |⇒ A ⟷^{K_{ab}} B

B |≡ S |⇒ A ⟷^{K_{ab}} B

A|≡ ♯(T_{s}) B |≡ ♯(T_{s}) B |≡ ♯(T_{a}) A|≡ ♯(T_{a})

Goals

A|≡ A ⟷^{K_{ab}} B

B |≡ A ⟷^{K_{ab}} B

A|≡ B |≡ A ⟷^{K_{ab}} B

B |≡ A|≡ A ⟷^{K_{ab}} B

There’s a minor error in [BAN89]. The authors claim to derive A|≡ B |≡ A ⟷^{K_{ab}} B, which is incorrect with the assumptions they have written. One has to add the very reasonable hypothesis A|≡ ♯(N_{a}) (A should indeed believe that the timestamp it gives, T_{a}, is correct!) to have it work. This has been detected (independently) in [CS96] and [Sch97].

A.6.4 The wide-mouthed frog protocol

Protocol

\begin{matrix}1 & A → S & \{(T_{a}, A ⟷^{K_{ab}} B)\}_{K_{as}} \\ 2 & S → B & \{(T_{s}, A|≡ A ⟷^{K_{ab}} B)\}_{K_{bs}} \end{matrix}

Assumptions

A|≡ A ⟷^{K_{as}} S

B |≡ B ⟷^{K_{bs}} S

S |≡ A ⟷^{K_{as}} S

S |≡ B ⟷^{K_{bs}} S

A|≡ A ⟷^{K_{ab}} B

B |≡ A|⇒ A ⟷^{K_{ab}} B

B |≡ S |⇒ A|≡ A ⟷^{K_{ab}} B

S |≡ ♯(T_{a}) B |≡ ♯(T_{s})

Goals

A|≡ A ⟷^{K_{ab}} B

B |≡ A ⟷^{K_{ab}} B

B |≡ A|≡ A ⟷^{K_{ab}} B

A.6.5 The Needham-Shroeder public-key protocol

Protocol

\begin{matrix}1 & S → A & \{↦^{+B} B\}_{K_{s}^{−1}} \\ 2 & A → B & \{N_{a}\}_{K_{b}} \\ 3 & S → B & \{↦^{+A} A\}_{K_{s}^{−1}} \\ 4 & B → A & \{⟨(N_{a}, A ⟷^{N_{b}} B)⟩_{N_{a}}\}_{K_{a}} \\ 5 & A → B & \{⟨(N_{b}, A ⟷^{N_{a}} B, B |≡ A ⟷^{N_{b}} B)⟩_{N_{b}}\}_{K_{b}} \end{matrix}

Assumptions

A|≡ ↦^{+A} A

A|≡ ↦^{+S} S

B |≡ ↦^{+B} B

B |≡ ↦^{+S} S

S |≡ ↦^{+A} A

S |≡ ↦^{+B} B

S |≡ ↦^{+S} S

A|≡ S |⇒ ↦^{+B} B

B |≡ S |⇒ ↦^{+A} A

A|≡ ♯(N_{a}) B |≡ ♯(N_{b})

A|≡ A ⟷^{N_{a}} B

B |≡ A ⟷^{N_{b}} B

A|≡ ♯(↦^{+B} B)

B |≡ ♯(↦^{+A} A)

Goals

A|≡ ↦^{+B} B

B |≡ ↦^{+A} A

A|≡ B |≡ A ⟷^{N_{b}} B

B |≡ A|≡ A ⟷^{N_{a}} B

B |≡ A|≡ B |≡ A ⟷^{N_{b}} B

Here, we had to deal with another minor problem. The authors seem to use a rule, correct for the informal semantics of the logic, but unsaid in the specification, that

\frac{P |≡ ⟨X⟩_{Y} P |≡ ♯(Y)}{P |≡ ♯(⟨X⟩_{Y})}.

A.6. AUTOMATIC ANALYSES IN BAN LOGIC 19 We had to replace instances of ⟨X⟩_{Y} by ⟨(Y, X)⟩_{Y} , and we get the correct results.

A.7 The rules of modified GNY logic

The rules with a “primed” name are those added to original GNY logic to match the “normal form” requirement (see section A.3); this transformation is described in A.5.2.

For better readbility, the destruction rules have been typeset in the following fashion:

\frac{D_{1} ⋯ D_{m} K_{1} ⋯ K_{n}}{C};

moreover, rules

\frac{H_{1} ⋯ H_{m}}{C_{1} ⋯ C_{n}}

are short for n rules

\frac{H_{1} ⋯ H_{m}}{C_{i}} .

A.7.1 Being-told rules

• T1 is a destruction rule:

\frac{P ◁ ⋆X}{P ◁ X}

• T2 is a destruction rule:

\frac{P ◁ (X, Y)}{P ◁ X P ◁ Y}

• T3 is a destruction rule:

\frac{P ◁ \{X\}_{K} P ∋ K}{P ◁ X}

• T4 is a destruction rule:

\frac{P ◁ \{X\}_{+K} P ∋ −K}{P ◁ X}

• T5 is a destruction rule:

\frac{P ◁ F (X, Y) P ∋ X}{P ◁ Y}

• TZ is a destruction rule:

\frac{P ◁ (X⇝Y)}{P ◁ X}

The TZ rule, though of obviously right informal meaning, is not in the original GNY paper; nevertheless it is necessary to run the logic and obtained the results advertised in that paper.

A.7.2 Possession rules

• P1 is a destruction rule:

\frac{P ◁ X}{P ∋ X}

• P2 is a construction rule:

\frac{P ∋ X P ∋ Y}{P ∋ (X, Y) P ∋ F (X, Y)}

• P3 is a destruction rule:

\frac{P ∋ (X, Y)}{P ∋ X P ∋ Y}

• P4 is a construction rule:

\frac{P ∋ X}{P ∋ H (X)}

• P5 is a destruction rule:

\frac{P ∋ F (X, Y) P ∋ X}{P ∋ Y}

• P6 is a construction rule:

\frac{P ∋ X P ∋ K}{P ∋ \{X\}_{K} P ∋ \{X\}_{K}^{−1}}

• P6’ is a destruction rule:

\frac{P ∋ \{X\}_{K} P ∋ K}{P ∋ X}

• P7 is a construction rule:

\frac{P ∋ +K P ∋ X}{P ∋ \{X\}_{+K}}

• P8 is a construction rule:

\frac{P ∋ −K P ∋ X}{P ∋ \{X\}_{−K}}

• P8’ is a destruction rule:

\frac{P ∋ \{X\}_{+K} P ∋ −K}{P ∋ X}

A.7.3 Freshness rules

• F1 is a construction rule:

\frac{P |≡ ♯(X)}{P |≡ ♯((X, Y)) P |≡ ♯((Y, X)) P |≡ ♯(F (X))}

• F2 is a construction rule:

\frac{P |≡ ♯(X) P ∋ K}{P |≡ ♯(\{X\}_{K}) P |≡ ♯(\{X\}_{K}^{−1})}

• F2’ is a destruction rule:

\frac{P |≡ ♯(\{X\}_{K}) P ∋ K}{P |≡ ♯(X)}

• F3 is a construction rule:

\frac{P |≡ ♯(X) P ∋ +K}{P |≡ ♯(\{X\}_{+K})}

• F4 is a construction rule:

\frac{P |≡ ♯(X) P ∋ −K}{P |≡ ♯(\{X\}_{−K})}

• F4’ is a destruction rule:

\frac{P |≡ ♯(\{X\}_{+K}) P ∋ −K}{P |≡ ♯(X)}

• F5 is an equivalence rule:

\frac{P |≡ ♯(+K)}{P |≡ ♯(−K)}

• F6 is an equivalence rule:

\frac{P |≡ ♯(−K)}{P |≡ ♯(+K)}

• F7 is a construction rule:

\frac{P |≡ ϕ(X) P |≡ ♯(K) P ∋ K}{P |≡ ♯(\{X\}_{K}) P |≡ ♯(\{X\}_{K}^{−1})}

• F8 is a construction rule:

\frac{P |≡ ϕ(X) P |≡ ♯(+K) P ∋ +K}{P |≡ ♯(\{X\}_{+K})}

• F9 is a construction rule:

\frac{P |≡ ϕ(X) P |≡ ♯(−K) P ∋ −K}{P |≡ ♯(\{X\}_{−K})}

• F10 is a construction rule:

\frac{P |≡ ♯(X) P ∋ X}{P |≡ ♯(H (X))}

• F11 is a destruction rule:

\frac{P |≡ ♯(H (X)) P ∋ H (X)}{P |≡ ♯(X)}

A.7.4 Recognizability rules

• R1 is a construction rule:

\frac{P |≡ ϕ(X)}{P |≡ ϕ((X, Y)) P |≡ ϕ((Y, X)) P |≡ ϕ(F (X))}

• R2 is a construction rule:

\frac{P |≡ ϕ(X) P ∋ K}{P |≡ ϕ(\{X\}_{K}) P |≡ ϕ(\{X\}_{K}^{−1})}

• R2’ is a destruction rule:

\frac{P |≡ ϕ(\{X\}_{K}) P ∋ K}{P |≡ ϕ(X)}

• R3 is a construction rule:

\frac{P |≡ ϕ(X) P ∋ +K}{P |≡ ϕ(\{X\}_{+K})}

• R4 is a construction rule:

\frac{P |≡ ϕ(X) P ∋ −K}{P |≡ ϕ(\{X\}_{−K})}

• R4’ is a destruction rule:

\frac{P |≡ ϕ(\{X\}_{+K}) P ∋ −K}{P |≡ ϕ(X)}

• R5 is a construction rule:

\frac{P |≡ ϕ(X) P ∋ X}{P |≡ ϕ(H (X))}

• R6 is a destruction rule:

\frac{P ∋ H (X)}{P |≡ ϕ(X)}

A.7. THE RULES OF MODIFIED GNY LOGIC 22

A.7.5 Message interpretation rules

• I1 is a destruction rule:

\frac{P ◁ ⋆ \{X\}_{K} P |≡ P ⟷^{K} Q P ∋ K P |≡ ϕ(X) P |≡ ♯((X, K))}{P |≡ Q|∼ X P |≡ Q|∼ \{X\}_{K} P |≡ Q ∋ K}

• I2 is a destruction rule:

\frac{P ◁ ⋆ \{(X, S)\}_{+K} P |≡ P ⟷^{S} Q P ∋ (−K, S) P |≡ ↦^{+P} P P |≡ ϕ((X, S)) P |≡ ♯((X, S, +K))}{P |≡ Q|∼ (X, S) P |≡ Q|∼ \{(X, S)\}_{+K} P |≡ Q ∋ +K}

• I3 is a destruction rule:

\frac{P ◁ ⋆H (X, S) P |≡ P ⟷^{S} Q P ∋ (X, S) P |≡ ♯((X, S))}{P |≡ Q|∼ (X, S) P |≡ Q|∼ H (X, S)}

• I4 is a destruction rule:

\frac{P ◁ \{X\}_{−K} P |≡ ↦^{+Q} Q P ∋ +K P |≡ ϕ(X)}{P |≡ Q|∼ X P |≡ Q|∼ \{X\}_{−K}}

• I5 is a destruction rule:

\frac{P ◁ \{X\}_{−K} P |≡ ↦^{+Q} Q P ∋ +K P |≡ ϕ(X) P |≡ ♯((X, +K))}{P |≡ Q ∋ (−K, X)}

• I6 is a destruction rule:

\frac{P |≡ Q|∼ X P |≡ ♯(X)}{P |≡ Q ∋ X}

• I7 is a destruction rule:

\frac{P |≡ Q|∼ (X, Y)}{P |≡ Q|∼ X P |≡ Q|∼ Y}

A.7.6 Jurisdiction rules

• J1 is a destruction rule:

\frac{P |≡ Q|⇒ C P |≡ Q|≡ C}{P |≡ C}

• J2 is a destruction rule:

\frac{P |≡ Q|∼ (X⇝C) P |≡ Q|⇒ Q|≡ ⋆}{P |≡ Q|≡ C}

• J3 is a destruction rule:

\frac{P |≡ Q|≡ Q|≡ C P |≡ Q|⇒ Q|≡ ⋆}{P |≡ Q|≡ C}

A.8. GNY ANALYSIS OF SOME PROPERTIES OF THE NEEDHAM-SHROEDER PROTOCOL 23

A.8 GNY analysis of some properties of the Needham-Shroeder protocol

PROTOCOL "Needham-Shroeder";
ASSUMPTIONS
A: P $ Kps;
B: P $ Np;
C: P |= P <-Kps-> S;
D: P |= #Np;
E: P |= %Q;
F: Q $ Kqs;
G: Q $ Nq;
H: Q |= Q <-Kqs-> S;
I: Q |= #Nq;
J: Q |= %Nq;
K: P |= S => (P <-K-> Q);
L: P |= S @@@;
M: P |= Q @@@;
N: Q |= S => (P <-K-> Q);
O: Q |= S @@@;
P: Q |= P @@@;
Q: S $ Kps;
R: S $ Kqs;
S: S $ K;
T: S |= (P <-Kps-> S);
U: S |= (Q <-Kqs-> S);
V: S |= P <-K-> Q;
MESSAGES
P->S: ( *P, *Q, *Np);
S->P: ( *{Np, Q, *K, ( *{K,P} Kqs ~> S |= P <-K-> Q)} Kps ~> S |= P <-K-> Q);
P->Q: ( *{*K, *P} Kqs ~> S |= P <-K-> Q);
Q->P: *{*Nq} K;
P->Q: ( *{*F(Nq)}K ~> P |= P <-K-> Q);
GOALS
P |= P <-K-> Q;
P $ Nq;
END

The L^{A}TEX code for this analysis report has been automatically generated, then manually touched up for better page layout.

A.8.1 Assumptions

A P ∋ K_{ps} B P ∋ N_{p}

C P |≡ P ⟷^{K_{ps}} S

D P |≡ ♯(N_{p}) E P |≡ ϕ(Q) F Q ∋ K_{qs} G Q ∋ N_{q}

H Q|≡ Q ⟷^{K_{qs}} S

I Q|≡ ♯(N_{q}) J Q|≡ ϕ(N_{q})

K P |≡ S |⇒ P ⟷^{K} Q

L P |≡ S |⇒ S |≡ ⋆ M P |≡ Q|⇒ Q|≡ ⋆

N Q|≡ S |⇒ P ⟷^{K} Q

O Q|≡ S |⇒ S |≡ ⋆ P Q|≡ P |⇒ P |≡ ⋆ Q S ∋ K_{ps} R S ∋ K_{qs} S S ∋ K

T S |≡ P ⟷^{K_{ps}} S

U S |≡ Q ⟷^{K_{qs}} S

V S |≡ P ⟷^{K} Q

A.8.2 Protocol steps

1. P → S : (⋆P, ⋆Q, ⋆N_{p})

2. S → P : (⋆ {(N_{p}, Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q))}_{K_{ps}} ⇝S |≡ P ⟷^{K} Q)

3. P → Q : (⋆ {(⋆K, ⋆P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q)

4. Q → P : ⋆ {⋆N_{q}}_{K}

5. P → Q : (⋆ {⋆F (N_{q})}_{K} ⇝P |≡ P ⟷^{K} Q)

A.8.3 Goals

• P |≡ P ⟷^{K} Q,

applying rule J1 to:

P |≡ S |⇒ P ⟷^{K} Q,

from hypothesis K.

P |≡ S |≡ P ⟷^{K} Q,

applying rule J3 to:

P |≡ S |≡ S |≡ P ⟷^{K} Q,

applying rule J2 to:

P |≡ S |∼ (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q),

applying rule I7 to:

P |≡ S |∼ (⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q)),

applying rule I7 to:

P |≡ S |∼ (Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q)),

applying rule I7 to:

P |≡ S |∼ (N_{p}, Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q)),

applying rule I1 to:

P ◁ ⋆ {(N_{p}, Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q))}_{K_{ps}},

applying rule TZ to:

P ◁ (⋆ {(N_{p}, Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q))}_{K_{ps}} ⇝S |≡ P ⟷^{K} Q),

from hypothesis Step #2.

P |≡ P ⟷^{K_{ps}} S,

from hypothesis C. P ∋ K_{ps},

from hypothesis A.

P |≡ ϕ((N_{p}, Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q))),

applying rule R1 to:

P |≡ ϕ((Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q))),

applying rule R1 to: P |≡ ϕ(Q),

from hypothesis E.

P |≡ ♯(((N_{p}, Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q)) , K_{ps})),

applying rule F1 to:

P |≡ ♯((N_{p}, Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q))),

applying rule F1 to: P |≡ ♯(N_{p}),

from hypothesis D.

P |≡ S |⇒ S |≡ ⋆,

from hypothesis L. P |≡ S |⇒ S |≡ ⋆,

from hypothesis L.

• P ∋ N_{q},

applying rule P1 to: P ◁ N_{q},

applying rule T1 to: P ◁ ⋆N_{q},

applying rule T3 to: P ◁ {⋆N_{q}}_{K},

applying rule T1 to: P ◁ ⋆ {⋆N_{q}}_{K},

from hypothesis Step #4. P ∋ K,

applying rule P1 to: P ◁ K,

applying rule T1 to: P ◁ ⋆K,

applying rule T2 to:

P ◁ (⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q)),

applying rule T2 to:

P ◁ (Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q)),

applying rule T2 to:

P ◁ (N_{p}, Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q)),

applying rule T3 to:

P ◁ {(N_{p}, Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q))}_{K_{ps}},

A.8. GNY ANALYSIS OF SOME PROPERTIES OF THE NEEDHAM-SHROEDER PROTOCOL 26

applying rule T1 to:

P ◁ ⋆ {(N_{p}, Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q))}_{K_{ps}},

applying rule TZ to:

P ◁ (⋆ {(N_{p}, Q, ⋆K, (⋆ {(K, P)}_{K_{qs}} ⇝S |≡ P ⟷^{K} Q))}_{K_{ps}} ⇝S |≡ P ⟷^{K} Q),

from hypothesis Step #2.

P ∋ K_{ps}, from hypothesis A.

Annexe B

Quelques idées sur les possibilités d’abstraction dans le problème des lancers de protocoles entrelacés

B.1 Definitions

B.1.1 A strong threat model

We assume that the intruder has full power over the communication network. All communication thus goes through and by the intruder. The intruder may choose to relay or not messages, to delay them, to modify them etc … The only restriction to its power is that it can’t send out data that is not in his knowledge at the moment of the sending — for instance, it can’t decrypt data encrypted with a key that it doesn’t own.

B.1.2 Protocol runs

Let D be the set of possible conveyable data. We have a knowledge production function k : P(D) → P(D) that, informally, computes the knowledge you can extract from a set of data. Such a function must verify

k ∘ k = k  (idempotence)
∀x, y ∈ P(D), x ⊂ y ⇒ k(x) ⊂ k(y) (monotonicity)
∀x ∈ P(D), x ⊂ k(x)  (expansion)

We call D̄ the image of k; that is, the set of knowledge closures; we put a complete lattice structure over it with

x ∨_{k} y = k(x ∪ y)

and x ∧ y = x ∩ y; the bottom element is ∅ and the top element is D.

Let ε ∈ D be a special value called the empty word; ∀x ∈ D̄, ε ∈ x.

Let P be the set of principals. Each principal p ∈ P has a local state, taken in the set S_{p}, runs according to a relation r_{p} ⊂ (S_{p} × D)^{2}. Informally, r_{p} ((s, m), (s′, m′)) means that when in state s and getting data m, p outputs message m′ and moves to state s′.

The global state space is

S = ∏_{p∈P} S_{p} × D̄.

and the stepping relation ⟶^{s} is defined as^{1}:

(s_{p})_{p∈P} , K_{I} ⟶^{s} (s′_{p})_{p∈P} , K′_{I}

⇔ ∃m ∈ K_{I}, ∃m′ ∈ D, ∃p_{0} ∈ P
\{ \begin{matrix}(s_{p_{0}}, m) ⟶^{r_{p}} (s′_{p_{0}}, m′) ∧ ∀p ≠ p_{0}, s′_{p} = s_{p} \\ K′_{I} = K_{I} ∨_{k} \{m′\} \end{matrix}

This definition is very broad, and even encompasses nondeterministic principals. Deterministic principals use a function f_{p} : (S_{p} × D) → (S_{p} × D) so that r_{p} is the graph of f_{p}.

B.1.3 Common encryption knowledge

Let’s consider D to be the free algebra on the constants in D_{0} with the following constructors: pairing (•, •) and symmetric-key encryption {•}_{•}. To

x ⟶^{R} y for (x, y) ∈ R.

1For a binary relation R, we’ll sometimes use the notation

limit confusion, we’ll write singletons built on this algebra between angle brackets. We define k(X) as the least fixpoint of the monotonic function (for the ⊂ ordering of +P(D))

X ↦ X ∪ ( ⋃_{⟨(x,y)⟩∈X}{⟨x⟩ , ⟨y⟩})

∪ ( ⋃_{⟨{x}_{k}⟩∈X / k∈X}{⟨x⟩})

∪ ( ⋃_{x,y∈X} {⟨(x, y)⟩ , ⟨{x}_{y}⟩}) .

Informally, k(X) is all that we can get from X through pairing, splitting, encrypting and decrypting with a key we possess.

B.1.4 Common implementations in this framework

Most of the times, we consider local states of the form

S_{p} = \underbrace{S_{p}}_{program counter} × \underbrace{D^{m_{p}}}_{registers}

where S_{p} is a (finite) set of steps and step relations r_{p} that so that for all initial local state s(σ, ρ_{1}, …, ρ_{m_{p}}), all incoming message m, all final local state s(σ′, ρ′_{1}, …, ρ′_{m_{p}}) and all outgoing message m′ so that r_{p} ((s, m), (s′, m′)), we have {m′, ρ′_{1}, …, ρ′_{m_{p}}} ⊂ k({m, ρ_{1}, …, ρ_{m_{p}}}).

B.2 A first abstraction

B.2.1 Informally

Let’s first consider a simple example. Let’s consider a protocol step in which a principal A receives a piece of data X and outputs the decryption of it with his private key −K_{a}. The intruder, at the beginning of this step, possesses {X}_{+K_{a}} and {Y }_{+K_{a}}. The intruder has to make a choice on what piece of data to submit to A for decryption. A problem is the high nondeterminism of that choice: the intruder may try any piece of data in its knowledge.

We abstract that problem into a model where the intruder may “magically” submit simultaneously all data to its knowledge to the principal for decryption. Clearly, the outcome of intruder knowledge, in that abstraction, is always bigger than the possible real outcome. Thus, this abstraction is conservative, in the sense that it overestimates the intruder’s knowledge.

B.2.2 Formally

Let’s suppose we have abstract relations r̂_{p} ⊂ (S̄_{p} × D̄)^{2} governing the principals that satisfy the abstraction property^{2}

S_{p} × D ⟶^{s} S_{p} × D
↓^{a_{p}⊗a_{D}}  ↓^{a_{p}⊗a_{D}}
Ŝ_{p} × D̄ ⟶^{ŝ} Ŝ_{p} × D̄

where a_{D} = {(x, y) ∈ D × D̄/x ∈ y} and a_{p} ⊂

S_{p} × Ŝ_{p}.^{3} The abstract global state space is

Ŝ = ( ∏_{p∈P} Ŝ_{p}) × D̄,

with the abstraction relation

a_{S} = (⨂_{p∈P} a_{p}) ⊗ =D̄

where =_{X} denotes the equality on X and the ab-

stract stepping relation ⟶^{ŝ} is defined as:

\begin{aligned}& (ŝ_{p})_{p∈P} , K_{I} ⟶^{ŝ} (ŝ′_{p})_{p∈P} , K′_{I} \\ ⇔ & ∃p_{0} ∈ P \{ \begin{matrix}(ŝ_{p_{0}}, K_{I}) ⟶^{r_{p}} (ŝ′_{p_{0}}, M′) \\ ∀p ≠ p_{0}, ŝ′_{p} = ŝ_{p} \\ K′_{I} = K_{I} ∨_{k} M′ \end{matrix} \end{aligned}

2We say that the abstraction property denoted by the diagram

A ⟶^{S} B
↓^{a_{A}}  ↓^{a_{B}}
A′ ⟶^{S′} B′

is satisfied when for all a ∈ A, b ∈ B, a′ ∈ A′ so that S(a, b) and a_{A}(a, a′) then there exists b′ so that S′(a′, b′) and a_{B}(b, b′).

3If we have r_{a} ⊂ A × A′ and r_{b} ⊂ B × B′, we note r_{a}⊗r_{b} = {((a, b), (a′, b′)) ∈ (A×B)×(A′×B′)/(a, a′) ∈ r_{a}∨(b, b′) ∈ r_{b}}. Similarly we define ⨂ over indexed products.

Then we have the following property:

S ⟶_{s} S
↓^{a_{S}}  ↓^{a_{S}}
Ŝ ⟶_{ŝ} Ŝ

This means that all states that map to unreachable abstract states are unreachable. Thus a safety property proved in the abstraction implies a safety property of the real protocol.

B.2.3 Abstraction of the common implementations

We abstract the local states to

Ŝ_{p} = Σ_{p} × D̄^{m_{p}}

by the abstraction a_{p} = D_{Σ_{p}} ⊗ a_{D}^{⊗m_{p}}. Then the “smallest” abstract step relation r̂_{p} is

((σ, ρ̂_{1}, …, ρ̂_{m_{p}}), m̂) ⟶^{r̂_{p}} ((σ′, ρ̂′_{1}, …, ρ̂′_{m_{p}}), m̂′)

⇔

\{ \begin{matrix}∀1 ≤ i ≤ m_{p}, \\ ρ̂′_{i} =  _{⋁k} ; \begin{matrix}((σ,ρ_{1},...,ρ_{mp}),m) & ⟶^{rp} & ((σ′,ρ′_{1},...,ρ′_{mp}),m′) \\ (σ,ρ_{1},...,ρ_{mp})⟶^{ap}(σ,ρ̂_{1},...,ρ̂_{mp}) \\ m⟶^{a_{D}}m̂ \end{matrix}\{ρ_{i}\} \\ m̂′ =  _{⋁k} ; \begin{matrix}((σ,ρ_{1},...,ρ_{mp}),m) & ⟶^{rp} & ((σ′,ρ′_{1},...,ρ′_{mp}),m′) \\ (σ,ρ_{1},...,ρ_{mp})⟶^{ap}(σ,ρ̂_{1},...,ρ̂_{mp}) \\ m⟶^{a_{D}}m̂ \end{matrix}\{m\}. \end{matrix}

B.2.4 A decision procedure for common-case abstraction

Definitions and properties

We consider the cases when the function k is defined as the closure by some formal rules making up the system ⊢_{k} — as in B.1.3, for instance, though more complex systems can easily be envisioned. We restrict ourselves to the cases where the system of rules matches the strong normal derivation property and a strictly decreasing order property.

We restrict ourselves to the cases where principal actions are of the following form: (r, s) where r is a formula whose leaves are either constants, register names seen as values or register names seen as destinations, to be used as a pattern to which incoming messages are matched; s is a formula whose leaves are either constants or register names seen as values, to be used as the reply.

Given a (finite) sequence l of principals, representing the interleaving of principal execution steps, which we will tag by number n representing their execution ordering and the name P of the principal involved, we construct the ⊢_{k,l} system of rules by prepending the following modalities to the ⊢_{k} rules:

• [n : P.R = X]: at step n, principal P ’s register R contains data X,

• [n : K_{I} ∋ X]: at step n, the intruder knows X.

The rules of the new system are those of ⊢_{k} with modalities, to which we add rules for the abstract protocol steps: a tagged step n.P : (r, s) is viewed as a rule

\frac{[n : K_{I} ∋ r] [n : P.R_{1} = X_{1}] … [n : P.R_{m} = X_{m}]}{[n + 1 : K_{I} ∋ s] [n + 1 : P.R_{1} = X_{1}] … [n + 1 : P.R_{q} = X_{q}]} ,

where [n : P.R_{1} = X_{1}] … [n : P.R_{m} = X_{m}] are constraints arising from the register values in the matches and [n : P.R_{1} = X_{1}] … [n : P.R_{m} = X_{m}] are the affectations made by the matching.

We require that for each of those rules, the consequences, taking off the modalities, can be derived in ⊢_{k} from the hypotheses, taking off the modalities. This informally means that the principals can only do “possible” computations, that is, computations along the lines of the ⊢_{k} system.

The resulting system, augmented, matches the strong normal derivation property and the strictly decreasing order property. Thus we can use forward-chaining on the derived system as a decision procedure in that abstraction.

If each principal can only make a finite number of steps in a run, for a given number of principals, the number of executable sequences is finite. Therefore, making up all the sequences and, for each, running the above decision procedure yields a decision procedure for the abstract whole problem.

Proofs

For any rule

\begin{aligned}M_{1}.H_{1} & … & M_{n}.H_{n} \\ & M_{C}.C \end{aligned} ⊢_{k,l}

of ⊢_{k,l} where the M_{x} are modalities, constraints on the principals’ computational power impose that

\begin{aligned}H_{1} & … & H_{n} \\ & ⋮ . ⊢_{k} \end{aligned} ; C.

We classify the H_{i} between data hypotheses and key hypotheses, according to their use in the former ⊢_{k}-derivation.

We complete the system into a new system ⊢_{k,l} by considering all the possible “annoying pairs” of construction/destruction rules. For instance, the ⊢_{k,l}-rule

{[3 : K_{I} ∋ X] \atop [4 : P.R_{1} = \{X\}_{K_{P}}^{−1} ]}

will be supplemented by the rule

{[3 : K_{I} ∋ \{X\}_{K_{P}}] \atop [4 : P.R_{1} = X]}.

If we have a strictly decreasing ordering ≤_{k} on ⊢_{k}, then we make a strictly decreasing ordering ≤_{k,l} on ⊢_{k,l} by taking the lexicographic product ordering of ≥ over the sequence numbers and ≤_{k}.

Bibliographie

[BAN89] Michael Burrows, Martin Abadi, and Roger Needham. A logic of authentication. Technical Report 39, Digital Equipment Corporation, Systems Research Centre, February 1989.

http://gatekeeper.dec.com/pub/DEC/SRC/
research-reports/abstracts/src-rr-039.
html

[BBC^{+}97] Bruno Barras, Samuel Boutin, Cristina Cornes, Judicael Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saibi, and Benjamin Werner. The Coq Proof Assistant Reference Manual : Version 6.1. INRIA (Rocquencourt) / CNRS / ENS-Lyon, May 1997.

ftp://ftp.inria.fr/INRIA/publication/RT/
RT-0203.ps.gz

[Bol97] Dominique Bolignano. Towards a mechanization of cryptographic protocol verification. In Orna Grumberg, editor, CAV’97: Computer Aided Verification, 9th International Conference, Haifa, Israel, volume 1254 of Lecture Notes in Computer Science, pages 131 – 142. Springer, June 1997.

[Bra95] Stephen H. Brackin. Deciding cryptographic protocol adequacy with HOL. In IWHOLTP: 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, volume 971 of Lecture Notes in Computer Science. Springer-Verlag, 1995.

[Bra96] Stephen H. Brackin. Automatic formal analyses of cryptographic protocols. In NISSC: 19th National Information Systems Security Conference, pages I.181 – 193, Baltimore, MD, October 1996. National Institute of Standards and Technology and National Computer Security Center.

[CELM96] M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In J. Meseguer, editor, Rewriting Logic and its Applications, First International Workshop, volume 4 of Electronic Notes in Theoretical Computer Science, pages 65–89. Elsevier Science B.V., September 1996. Only available electronically, to the subscribers of Theoretical Computer Science.

                                                       http://www1.elsevier.nl/mcs/tcs/pc/
                                                       volume4.htm

[Cou97] Patrick Cousot. Introduction a l’interprétation abstraite. Transparents à l’occasion de l’École Jeunes Chercheurs en Programmation, Mars 1997.

                                                       http://www.dmi.ens.fr/~cousot/cours/
                                                       compilation/Cours-9-Compil-4-1.ps.gz

[CS96] Dan Craigen and Mark Saaltink. Using eves to analyze authentication protocols. Technical Report TR-96-5508-05, ORA Canada, Ottawa, March 1996.

                                                       ftp://ora.on.ca/pub/doc/96-5508-05.dvi.
                                                       Z

[GNY90] Li Gong, Roger Needham, and Raphael Yahalom. Reasoning about belief in cryptographic protocols. In IEEE Symposium on Research in Security and Privacy, pages 234–248, Oakland, California, May 1990. IEEE Computer Society, IEEE Computer Society Press.

http://java.sun.com/people/gong/papers/
gny-oakland.ps.gz

[Gon90] Li Gong. Cryptographic Protocols for Distributed Systems. PhD thesis, University of Cambridge, Cambridge, England, April 1990.

http://java.sun.com/people/gong/papers/
phd-thesis.ps.gz

[KW96] D. Kindred and J. M. Wing. Fast, automatic checking of security protocols. In Second USENIX Workshop on Electronic Commerce, pages 41–52, Oakland, California, November 1996. USENIX.

http://www-cgi.cs.cmu.edu/afs/cs.cmu.
edu/project/venari/www/usenix96-submit.
html

[MCJ97] W. Marrero, E.M. Clarke, and S. Jha.

Model checking for security protocols. Technical Report CMU-SCS-97-139, Carnegie Mellon University, May 1997.

[Pau97] Lawrence C. Paulson. Proving properties of security protocols by induction. In 10th Computer Security Foundations Workshop, pages 70–83. IEEE Computer Society Press, 1997.

http://www.cl.cam.ac.uk/users/lcp/
papers/protocols.html

[Sch96] Bruce Schneier. Applied Cryptography.

John Wiley & Sons, 1996.

[Sch97] Johann Schumann. Automatic verification of cryptographic protocols with SETHEO. In 14th International Conference on Automated Deduction (CADE), Lecture Notes in Computer Science. Springer-Verlag, 1997.