In this paper, we introduce a new type of functions to analyze cryptographic protocols statically for the property of secrecy: the Witness-Functions. A Witness-Function is a reliable protocol-dependent function intended to prove the correctness of a protocol through its growth. It bases its calculation on the static part of a message in a role-based specication and ignores the dynamic one by introducing the notion of derivative messages. It oers two interesting bounds that enable an analysis of protocols on an unbounded number of sessions. We give here the way to build these functions and we state the theorem of protocol analysis with the Witness-Functions.
Motivation and background
In this paper, we introduce a new static approach to analyze cryptographic protocols
with witness-functions for the property of secrecy. Intuitively, an increasing protocol
preserves the secret. In other words, if the security of any atomic message does not decrease
between receiving and sending steps of a protocol, the secret is never leaked. For that, we
should dene "good" metrics to evaluate the security of any atomic message. This way of
thinking has been considered in some previous works. In [
Hereafter, we give some denitions and conventions that will be used throughout the paper.
+ We denote by C = hM; ; j=; K; Lw; p:qi the context containing the parameters that aect the analysis of a protocol:
M : is a set of messages built from the algebraic signature hN , i where N is a set of atomic names (nonces, keys, principals, etc.) and is a set of allowed functions (enc:: encryption, dec:: decryption, pair:: concatenation (denoted by "." here), etc.). i.e. M = ThN ; i(X ). We use to denote the set of all possible substitution from X ! M. We denote by A all atomic messages in M; by A(m) the set of atomic messages (or atoms) in m and by I the set of agents (principals) including the intruder I. We denote by k 1 the reverse key of a key k and we consider that (k 1) 1 = k. : is the equational theory that describes the algebraic properties of the functions in by equations. e.g. dec(enc(x; y); y 1) = x. j= : is the inference system of the intruder under the equational theory. Let M be a set of messages and m a message. M j= m means that the intruder is able to infer m from M using her capacity. We extend this notation to traces as following: j= m means that the intruder can infer m from the messages exchanged in the trace . K : is a function from I to M, that assigns to any agent (principal) a set of atomic messages describing her initial knowledge. We denote by KC(I) the initial knowledge of the intruder, or simply K(I) where the context is clear.
Lw : is the security lattice (L; w; t; u; ?; >) used to attribute security levels to
messages. A concrete example of a lattice is (2I ; ; \; [; I; ;) that will be used to attribute
to a message the set of principals that are allowed to know it.
p:q : is a partial function that assigns a value of security (type) to a message in
M. Let M be a set of messages and m a message. We write pM q w pmq if 9m0 2
M:pm0q w pmq
+ Let p be a protocol, we denote by RG(p) the set of the generalized roles extracted from
p. A generalized role is a protocol abstraction where the emphasis is put on a particular
principal and all the unknown messages, and on which no verication could be done
by the agent, are replaced by variables. A generalized role ends always by a sending
step and an intruder I is introduced to describe that the received messages and the
sent messages are probably sent or received by the intruder. More details about the
role-based specication are in [
G G RG (pNSL)= m1 : A m2 : B m3 : A ! B : fNa:Agkb ! A : fB:Nagka :fB:Nbgka ! B : A:B:fNbgkb
To analyze a protocol, we need reliable functions to estimate the security level of every atomic message. In this section, we state sucient conditions allowing to guarantee that a function is reliable. We prove that an increasing protocol is correct with respect to the secrecy property when analyzed with such functions. 2.1
Denition 21 (Well-formed interpretation function) Let F be an interpretation function.
F is well-formed in C if: 8M; M1; M2 M; 8 2 A(M):
For an atom in a set of messages M , a well-formed interpretation function returns the bottom value "?" if appears in clear in M . It returns for it in the union of two sets, the minimum "u" of the two values calculated in each set seperately. It returns the top value ">" if does not appear at all in M .
Example 22 Let m1 = f g; m2 = f :Agkab , M = fm1; m2g and F a well-formed interpretation function.
F ( ; M ) = F ( ; fm1g [ fm2g) = F ( ; f g) u F ( ; f :Agkab )= ? u > = ? F ( ; M )= F ( ; fm1g [ fm2g)= F ( ; f g) u F ( ; f :Agkab )= > u F ( ; f :Agkab ) = F ( ; f :Agkab ) Denition 23 (Full-invariant-by-intruder interpretation function) Let F be an interpretation function.
F is full-invariant-by-intruder in C if: 8M M; m 2 M:M j=C m ) 8 2 A(m):(F ( ; m) w F ( ; M )) _ (pK(I)q w p q)
An interpretation function F is said to be full-invariant-by-intruder if when it assigns a security level to an atomic message in a set of messages M , this level cannot be decreased by the intruder. That is to say, the intruder cannot infer another message m from M in which the level of security of decreases (i.e. F ( ; m) w F ( ; M )) using her capacity in the context of verication, unless is initially intended to be known by the intruder (i.e. pK(I)q w p q). Denition 24 (Reliable interpretation function) Let F be an interpretation function and C be a context.
Let F be an interpretation function and p a protocol. p is F -increasing in C if: 8R:r 2 RG(p); 8 2 : X ! Mp we have:
F is C-reliable if F is well-formed and F is full-invariant-by-intruder in C: 8 2 A(Mp):F ( ; r+ ) w p q u F ( ; R )
A F -increasing protocol is a protocol where every involved principal (every substituted generalized role) never decreases the security levels of received components. When a protocol is F -increasing and F is a reliable function, it is intuitively easy to prove its correctness with respect to the secrecy property. In fact, if every agent appropriately protects her sent messages (if she initially knows the security level of a component, she has to encrypt it with at least one key having a similar or higher security level, and if she does not know its security level, she estimates it using a reliable function F ), the intruder can never reveal it.
Let p be a protocol and C a context.
We say that p discloses a secret 2 A(M) in C if: 9 2 [[p]]:( j=C
) ^ (pK(I)q 6w p q)
A secret disclosure consists in exploiting a valid trace of the protocol (denoted by [[p]]) by the intruder using her knowledge K(I) in the context of verication C, to infer a secret that she is not allowed to know (expressed by: pK(I)q 6w p q in the denition 26).
Let F be a C-reliable interpretation function and p a F -increasing protocol. We have: 8m 2 M:[[p]] j=C m ) 8
2 A(m):(F ( ; m) w p q) _ (pK(I)q w p q):
The lemma 27 expressess an intuitive result that for any atom in a message generated by an increasing protocol, its security level calculated by a reliable interpretation function is maintained greater than its initial value in the context, if the intruder is not initially allowed to know it. Thus, initially the atom has a certain security level. This value cannot be decreased by the intruder using her initial knowledge and received messages since a reliable function is full-invariant by intruder. In each new step of any valid trace, involved messages are better protected since the protocol is increasing. The proof is then run by induction on the size of the trace and uses the reliability properties of the interpretation function in every step.
Let F be a C-reliable interpretation function and p a F -increasing protocol.
p is C-correct with respect to the secrecy property.
In this section, we have shown that an increasing protocol is correct with respect to the secrecy property when analyzed with an interpretation function that is full-invariant by intruder and well-formed, or simply reliable. Please notice that compared to the sucient conditions stated in [11], we have one less. Houmani in [11] requested that a protocol must be increasing on the messages of the generalized roles of the protocol (that contain variables), and demanded from the interpretation function to resist to the problem of substitution of variables. Here, we free our functions from this restrictive condition in order to be able to build more functions. We relocate this condition in our new denition of an increasing protocol, that is requested now to be increasing on valid traces. The problem of substitution migrates to the protocol and becomes less harder to deal with. 3
Building reliable interpretation functions
As seen in the previous section, to analyze a protocol statically we need reliable
interpretation functions to evaluate the level of security of each atom in a message. In this section,
we propose a constructive way to build these functions. We rst show how to build a generic
class of reliable selections inside the protection of the most external key (or simply the
external key), then we provide specialized selections that are instances of this class, and nally
we show the way to build reliable selection-based interpretation functions. Similar techniques
have been used in some previous works and especially in [8,10,11] to build functions based on
the direct key of encryption and in [
Well-protected messages
We denote by EC the set of encryption functions and by E C the complementary set nEC in a context of verication C. In the denition 31, we dene the application keys that returns the encryption keys of any atom in a message m.
Denition 31 (Keys) Let M M, f 2 and m 2 M .
We dene the application Keys as follows:
Keys : A
M
! P (P(A)) Denition 32 (Equational theory, rewriting system and normal form) We assume that we can transform the equational theory given in the context of verication to a convergent rewriting system ! such that: 8m 2 M; 8 2 A(m); 8l ! r 2! ;
Keys( ; r)
Keys( ; l) (3.1.1)
The normal form of a message in the denition 32 is the one that has the smallest set of
encryption keys and eliminates all the unnecessary keys (e.g. e(k; d(k 1; m)) ! m). This
kind of rewriting systems orientation poses no problem with the most of equational
theories [
In the denition 33 we introduce the application Access where every element of Access( ; m) contains a set of required keys to decrypt in m after elimination of unnecessary keys by the normal form dened in 32.
Let M M, f 2 and m 2 M .
We dene the application Accessor as follows: Access : A
M ! P(P(A))
Access( ; ) Access( ; )
6=n and 2 A Access( ; fk(t1; :::; tn)) = fnk 1g i=[1Access( ; ti); if fk 2 EC and fk(t1; :::; tn) = fk(t1; :::; tn)+ Access( ; f (t1; :::; tn)) = [ Access( ; ti); if f 2 E C and fk(t1; :::; tn) = fk(t1; :::; tn)+ i=1 Access( ; f (t1; :::; tn)) = Access( ; f (t1; :::; tn)+), if not.
8M
M:Access( ; M ) =
[ Access( ; m) and Access( ; ;) = ;: m2M Access( ; m) = ffkac1; kab1g; fkac1g; fkac1; kab1; kef1gg.
Example 34 Let m be a message such that: m = ffA:D: gkab : :fA:E:fC: gkef gkab gkac ; In the denition 35, we dene a well-protected message. Informally, a well-protected message is a message such that every atom in it such that p q A ? is encrypted by at least one key k such that pk 1q w p q after elimination of unnecessary keys by the normal form dened in 32.
Let C be context of verication, m 2 M, M
is well-protected in m if:
is well-protected in M if:
8K 2 Access( ; m):pKq w p q
8
M and
In the denition 36, we dene Clear(m). Informally, Clear(m) is the set of all atoms that appear in clear in m after elimination of unnecessary keys by the normal form dened in 32. Denition 36 (Clear) Let m 2 M and M M.
Clear(m) = f 2 A(m)j ; 2 Access( ; m)g We extend this denition to sets as follows:
Let M be a set of well-protected messages in Clear(M ) =
[ Clear(m) m2M
The lemma 37 states that from a set of well-protected messages, all atomic messages beyond the knowledge of the intruder (i.e. pK(I)q 6w p q) remain well-protected in any message that the intruder could infer. In fact, since we operate on well-protected messages, every atom such that p q A ? is encrypted by at least one key k such that pk 1q w p q. So the intruder must retrieve k 1 before she sees not well-protected in any message. Yet, the key k 1, if it appears in M , should be in its turn encrypted by at least one key k0 such that pk0 1q w pk 1q since we operate on well-protected messages. The proof is then run by induction on the encryption keys.
Lemma 38 (Lemma of non-disclosure of atomic secrets in well-protected messages) Let M be a set of well-protected messages in M and an atomic message in M . We have:
M j=C
) pK(I)q w p q:
Proof. See the proof 914 in [
Well-protected messages and increasing protocols
The lemma 38 expresses an important result. It states that a set of well-protected messages never discloses a secret. Thus, an intruder cannot infer from this set of messages something that she is not initially allowed to know. The notion of well-protected messages is linked to the notion of increasing protocols. Indeed, having a reliable interpretation function F and a protocol p, p could not be F -increasing if it does not operate on a set of well-protected messages Mp. Thus, a F -increasing protocol does not leak secrets as established by the theroem 21. This could not happen if Mp is not well-protected. Thus, an atomic message that is not well-protected in Mp could be deduced by agents that have the decryption keys even if they are not intented to know it. To be coherent, a reliable interpretation function must give for a non-well-protected atom in any message m in Mp a value less than p q (e.g. F ( ; m) = ?). 3.3
Reliable selections in well-protected messages
Now, we will focus on building selections such that when they are composed to suitable homomorphisms, provide reliable interpretation functions. The denition 39 introduces the notion of a well-formed selection and the denition 310 introduces the notion of a fullinvariant-by-intruder selection.
Denition 39 (Well-formed selection) Let M; M1; M2 M such that M; M1 and M2 are well-protected.
Let S : A M 7 ! 2A be a selection.
We say that S is well-formed in C if: 8< S( ; f g) = A;
S( ; M1 [ M2) = S( ; M1) [ S( ; M2); : S( ; M ) = ;, if 2= A(M )
For an atom in a set of messages M , a well-formed selection returns all the atoms in M if M = f g. It returns for it in the union of two sets of messages, the union of the two selections performed in each set separately. It returns the empty set if the atom does not appear in M .
Let M M such that M is well-protected.
Let S : A M 7 ! 2A be a selection.
We say that S is full-invariant-by-intruder in C if: 8M M; m 2 M; we have:
The goal of a full-invariant-by-intruder selection is to create a full-invariant-by-intruder function when composed to an appropriate homomorphism that transforms its returned values into security levels. Since a full-invariant-by-intruder function is requested to resist to any attempt of the intruder to generate a message m from any set of messages M in which the level of security of an atom, that she is not allowed to know, decreases compared to it its value in M , a full-invariant-by-intruder selection is requested to resist to any attempt of the intruder to generate a message m from any set of messages M in which the selection associated to an atom, that she is not allowed to know, could be enlarged compared to the selection associated to this atom in M . This fact is expressed by the denition 310.
Let S : A M 7 ! 2A be a selection and C be a context of verication.
S is C-reliable if S is well-formed and S is full-invariant-by-intruder in C: 3.3.1
Reliable selections inside the protection of an external key Now, we dene a generic class of selections that we call SGEeKn and we prove that any instance of this class is C-reliable. Then we instantiate concrete selections from this class. Denition 312 ( SGEeKn: selection inside the protection of an external key) We denote by SGEeKn the class of all selections S that meet the following conditions: S( ; ) = A; S( ; m) = ;, if
62 A(m); 8 8 2 A(m); where m = fk(m1; :::; mn) : 2 A(m); where m = f (m1; :::; mn) : 8 >>1 [i n
S( ; m) = < S( ; fmg [ M ) = S( ; m) [ S( ; M ) S( ; m) ( 1 [i nA(mi)[fk 1gnf g) if fk 2 EC and pk 1q w p q and m = m+
S( ; mi) if fk 2 EC and pk 1q 6w p q and m = m+ (a) >1 [i nS( ; mi) if f 2 E C and m = m+ (b) >:S( ; m+) if m 6= m+ (c) (3.3.1) (3.3.2) (3.3.3) (3.3.4) (3.3.5)
For an atom in an encrypted message m = fk(m1; :::; mn), a selection S as dened above returns a subset (see " " in equation 3.3.3) among atoms that are neighbors of in m inside the protection of the most external protective key k including its reverse form k 1. The atom itself is not selected. This set of candidate atoms is denoted by 1 [i nA(mi)[fk 1gnf g in the equation 3.3.3. The most external protective key (or simply the external key) is the most external one that satises pk 1q w p q. By neighbor of in m, we mean any atom that travels with it inside the protection of the external key. Outside the protection of the external key, we have: no eective selection is performed; any two messages joined by an operation other than an encryption by the external key (e.g. a concatenation or an encryption by a weak key) are assimilated to two distinct messages and the selection returns the union of the two selections performed separately in each one (see the equations 3.3.4(a) and 3.3.4(b)); the selection in two sets of messages is the union of the two selections performed separately in each one(see the equation 3.3.5); the selection relative to a clear atom returns all atoms in M (see the equation 3.3.1); the selection relative to an atom that does not appear in a message returns the empty set(see the equation 3.3.2).
SGEeKn denes a generic class of selections since it does not identify what atoms to select precisely inside the protection of the external key. It identies only the atoms that are candidates for selection and among them we are allowed to return any subset.
Let S 2 SGEeKn and C be a context of verication. Let’s have a rewriting system ! such that 8m 2 M; 8 2 A(m) ^ 62 Clear(m); we have: (3.3.6)
8l ! r 2! ; S( ; r) S( ; l)
The condition on the rewriting system ! given by the equation 3.3.6 in the denition 313 is introduced to make sure that the selection in the normal form is the smallest among all forms of a given message. This prevents the selection S to select atoms that may be inserted maliciously by the intruder by manipulating the equational theory. Hence, we are sure that all selected atoms by S are honest and do not come by an intruder manipulation of the message. For example, let m = f :Cgkab be a message in a homomorphic cryptography (i.e. f :Cgkab = f gkab :fCgkab ). In the form f :Cgkab , the selection S( ; f :Cgkab ) may select C, but in the form f gkab :fCgkab , the selection S( ; f gkab :fCgkab ) may not. Then, we must make sure that the rewriting system ! we are using is oriented in such way that it chooses the form f gkab :fCgkab rather than the form f :Cgkab because there is no guarantee that C is a honest neighbor and that it had not been inserted maliciously by the intruder using the homomorphic property in the theory. We assume that the equational theory in the context of verication allows the extraction of a convergent rewriting system that meets this condition.
As for the proposition 313, it is quite easy to verify that by constuction a selection S that is instance of SGEeKn is well-formed. The proof of full-invariance-by-intruder is run by induction on the tree of construction of any message. The main idea of the proof is that the selection of the candidate atoms is performed inside the encryption by the most external protective key and therfore beyond the knowledge of the intruder, thus the intruder cannot alter when she does not detain this key. Besides, according to the lemma 38, in a set of well-protected messages the intruder can never infer this key since it is atomic. The intruder cannot neither use the equational theory to alter this selection for the reasons given in the remark 314. Therefore the set of atoms returned by S cannot be altered (enlarged) by the intruder as required by a full-invariant-by-intruder selection.
Example 315 Let be an atomic message and m a message such that p q = fA; Bg and m = fA:C: :Dgkab . 1Let S1; S2 and S3 be three selections such that: S1( ; m) = fkab1g, S2( ; m) = fA; C; kab g and S3( ; m) = fA; C; D; kab1g. These three selections are C-reliable. 3.4
Instantiation of reliable selections from the class SGEeKn
Now that we dened a generic class of reliable selections SGEeKn, we will instantiate some concrete selections from it, that are naturally reliable. Instantiating SGEeKn consists in dening selections that return precise sets of atoms among the candidates allowed by SGEeKn. 3.4.1 The selection SMEKAX : is the instance of the class SGEeKn that returns for an atom in a message m all its neighbors, that are principal identities, inside the protection of the external protective key k in addition to its reverse form k 1. (MAX means: the MAXimum of principal identities) 3.4.2 The selection SEEKK : is the instance of the class SGEeKn that returns for an atom in a message m only the reverse form of the external protective key. (EK means: External Key) 3.4.3 The selection SNEK : is the instance of the class SGEeKn that returns only its neighbors, that are principal identities, inside the protection of the external protective key. (N means: Neighbors)
Several other selections could be dened such that the selections inside the most internal key or inside all the keys together since they are all subselections inside the external key.
Let be an atom and m a message such that: p q = fA; Cg and m =fff :Cgkab :Bgkac :Dgkad SMEKAX ( ; m) = fC; B; kac1g; SEEKK ( ; m) = fkac1g; SNEK ( ; m) = fC; Bg 3.5
Specialized C-reliable selection-based interpretation functions
The following proposition gives the way to transform the elements returned by a selection to security levels.
: (2A) 7! Lw
( M 7!
> u 2M
if M = ; ( ) if not. such that: ( ) = f g if 2 I (Principal Identities) p q if not.
We have: FMEKAX = SMEKAX , FEEKK = SEEKK and FNEK =
The homomorphism dened in the proposition 317 returns for a principal in a selection, its identity. It returns for a key its level of security in the context of verication. ensures the mapping from the operator " " to the operator " w" in the lattice which enables an interpretation function to inherit the full-invariance-by-intruder from its associated selection. It ensures also the mapping from the operator " [" to the operator " u" in the lattice, which enables an interpretation function to be well-formed when its associated selection is wellformed. Generally, any function S remains reliable for any selection S that is an instance of SGEeKn.
Let be an atom, m a message and kab a key such that: p q = fA; Bg; m = fA:C: :Dgkab ; kab1 = kab; pkabq = fA; Bg;
1 ; SNEK ( ; m) = fA; C; Dg; SMEKAX ( ; m) = fA; C; D; kab1g; SEEKK ( ; m) = fkab g FEEKK ( ; m) = SEEKK ( ; m) = pkab1q = fA; Bg; FNEK ( ; m) = SNEK ( ; m) = fA; C; Dg; FMEKAX ( ; m) = SMEKAX ( ; m) = fA; C; Dgupkab1q = fA; C; Dg u fA; Bg = fA; C; D; Bg. 4
The Witness-Functions
In the previous section, we presented a constructive way of a class of selection-based
functions that have the required properties to analyze protocols statically. Unfortunatly, they
operate only on valid traces that contain closed messages. However, a static protocol analysis
should run over a nite set of messages of the generalized roles of the protocol because the set
of valid traces is innite. The nite set of the generalized roles contains variables. The
functions we dened are not "enough prepared" to analyze messages with variables because they
are not supposed to be full-invariant by substitution (or stable by substitution) [
Derivative message
Let m; m1; m2 2 M; X m = V ar(m); S1; S2 empty message.
2Xm ; 2 A(m); X; Y 2 Xm and be the
For the sake of simplication, we denote by @m the expression @Xm m. The operation of derivation in the denition 41 (denoted by @) is used to eliminate variables in a message. @X m consists in eliminating the variable X in m. @[X]m consists in eliminating all variables, except X, in m. Hence, X when overlined is considered as a constant in m. @m consists in eliminating all the variables in m.
Example 42 Let m = fA:X:Y gkab where A and kab are static and X and Y are two variables. We have: @m = fAgkab ; @X m = fA:Y gkab ; @[X]m = fA:Xgkab
Let m 2 MpG , X 2 Xm and m be a closed message.
For all 2 A(m ), 2 , we denote by: <8 > if
F ( ; @m) if : F (X; @[X]m) if 62 A(m ); 2 A(@m); 2 A(X ) ^
A message m in a generalized role is composed of two parts: a static part and a dynamic part. The dynamic part is described by variables. For an atom in the static part (i.e. @m), F ( ; @[ ]m ) removes the variables in m and gives it the value F ( ; @m). For anything that is not an atom of the static part, so comes by substitution of some variable X in m, F ( ; @[ ]m ) considers it as the variable itself, treated as a constant (as a block), and gives it the value F (X; @[X]m). It gives the top value for any atom that does not appear in m . For any F such that its associated selection is an instance of the class SGEeKn, F ( ; @[ ]m ) depends only on the static part of m since is never selected. The introduction of the derivation could suggest that we give to F ( ; m ) the value of F ( ; @[ ]m ) and hence we neutralize the variable eects. Unfortunately, this does not happen without undesirable "sideeects" because derivation causes a "loss of details". Let’s examine the following case in the example 44.
Example 44 Let m1 and m2 be two messages of a generalized role of a protocol p such that m1 = f :B:Xgkad and m2 = f :Y:Cgkad and p q = fA; Dg. Let m = f :B:Cgkad be in a valid trace generated by p. (fB; A; Dg fA; D; Cg if m comes by the substitution of X by C in m1 if m comes by the substitution of Y by B in m2 Hence FMEKAX ( ; @[ ]m) is not even a function on the closed message m since it may return more than one image for the same preimage. This leads us straightly to the witness-functions. 4.2
The Witness-Functions Denition 45 (Witness-Function) Let m 2 MpG , X 2 Xm and m be a closed message.
Let p be a protocol and F be a C-reliable interpretation function.
We dene a witness-function Wp;F for all 2 A(m ), 2 , as follows:
Wp;F ( ; m ) =
m02uMpG 9 02 :m0 0=m Wp;F is said to be a witness-function inside the protection of an external key when F is an interpretation function such that its associated selection is an instance of the class SGEeKn:
As seen in the example 44, the application dened in 43 is not necessary a function in the set MpG of messages generated by the generalized roles of p since a valid trace could have more than one source in MpG such that each source has a dierent static part. A witness-function is though a function since it looks for all the sources of any closed message and takes the minimum (the union). This minimum exists and is unique in the nite set MpG . Although a witness-function is protocol-dependent since it depends on messages in the generalized roles of the protocol, it is built in a standard way for any pair (protocol, interpretation function) in input.
Remark 46 For a witness-function inside the protection of an external key, since its associated interpretation function calculates the security level of an atom always in a message m having an encryption pattern, i.e. when fk 2 EC, the search of all sources of m in the set fm0 2 MpG j9 0 2 :m0 0 = m g is reduced to a search in the encryption patterns in MpG . Proposition 47 Let Wp;F be a witness-function inside the protection of an external key.
We have:
The selection associated with a witness-function inside the protection of an external key is the union of selections associated with the interpretation function F restricted to derivative messages. It is easy to verify that a witness-function is by construction well-formed. For the full-invariance-by-intruder property, since the derivation just removes variables and since each selection in the union returns a subset among acceptable candidates, then the union itself returns a subset among acceptable candidates (the union of subsets is a subset). Therefore the selection associated with a witness-function remains an instance of the class SGEeKn and so fullinvariant-by-intruder. Since the witness-function is the composition of the homomorphism associated with F and an instance of the class SGEeKn, then it is reliable.
Let MpG = ff :B:Xgkad ; f :Y:Cgkad ; fA:Zgkbc g; m1 = f :B:Cgkad ; V ar(MpG ) = fX; Y; Zg: Wp;FMEKAX ( ; m1) = {Denition 45}
FMEKAX ( ; @[ ]m0 0) = m02uMpG ff :B:Xgkadu;f :Y:Cgkad g 9 02 :m0 0=m1 0=fX7 !C;Y 7 !Bg = fWp;FMEKAX is well-formed from the proposition 47 } FMEKAX ( ; @[ ]f :B:Xgkad [X 7 ! C])uFMEKAX ( ; @[ ]f :Y:Cgkad [Y 7 ! B]) ={Denition 43 and derivation in 41} FMEKAX ( ; f :Bgkad ) u FMEKAX ( ; f :Cgkad ) = {Denition of FMEKAX g fB; A; Dg [ fC; A; Dg = fB; A; D; Cg 4.4
Bounding a Witness-Function Lemma 49 Let m 2 MpG and Wp;F be a witness-function inside the protection of an external key. 8 2 ; 8 2 A(Mp) we have:
The upper bound of a witness-function estimates the security level of an atom from one conrmed source of the closed message, the witness-function it-self estimates it from the exact sources of the closed message (i.e. when the protocol is executed), and the lower bound estimates it from all likely sources of the closed message. The unication in the lower bound "hunts" the candidates from all the likely sources of the closed message in the protocol. 4.5
Sucient condition for protocol correctness with a Witness-Function Now, it is time to state the protocol analysis with a Witness-Function theorem that states a criterion for protocol correctness with respect to the secrecy property which is independent of all substitutions.
Theorem 41 (Protocol analysis with a Witness-Function) Let Wp;F be a witness-function inside the protection of an external key.
A sucient condition of correctness of p with respect to the secrecy property is: 8R:r 2 RG(p); 8 2 A(r+) we have:
m02uMpG 9 0=mgu(m0;r+)
Thanks to the independence of the criterion stated by the theorem 41 of all substitutions, any decision made on the generalized roles can be transmitted to valid traces. 5
NSL protocol analysis with a witness-function
Hereafter, we analyze the N SL protocol given in Table 1 with a witness-function. Let’s have a context of verication such that: pAq = ?; pBq = ?; pNaiq = fA; Bg (secret shared between A and B); pNbiq = fA; Bg (secret shared between A and B); pka 1q = fAg; pkb 1q = fBg; (L; w; t; u; ?; >) = (2I ; ; \; [; I; ;); I = fI; A; B; A1; A2;B1; B2; :::g; The set of messages generated by the protocol is MpG = ffNA1 :A1gkB1 ; fB2:NA2 gkA2 ; fB3:X1gkA3 ; fX2gkB4 ; fY1:A4gkB5 ; fB6:Y2gkA5 ; fB7:NB7 gkA6 ; fNB8 gkB8 g The variables are denoted by X1; X2; Y1 and Y2; The static names are denoted by NA1 , A1, kB1 , B2, NA2 , kA2 , B3, kA3 , kB4 , A4, kB5 , B6, kA5 , B7, NB7 , kA6 , NB8 and kB8 .
After elimination of duplicates, MpG = ffNA1 :A1gkB1 ; fB2:NA2 gkA2 ; fB3:X1gkA3 ; fX2gkB4 ; fY1:A4gkB5 ; fB7:NB7 gkA6 ; fNB8 gkB8 g Let’s select the Witness-Function as follows: p = N SL; F = FMEKAX ; Wp;F ( ; m ) = F ( ; @[ ]m0 0); Please notice that all messages are in their normal form since no equational theory is dened. Principal identities in the context are not analyzed since they are declared public. The protocol is analyzed for the property of secrecy only.
As dened in the generalized roles of p, an agent A can participate in two consequent sessions: Si and Sj such that j > i. In the former session Si, the agent A receives nothing and sends the message fNai:Agkb . In the consequent session Sj, she receives the message fB:Naigka :fB:Xgka and she sends the message A:B:fXgkb . This is described by the following schema:
Si :
2 fNai:Agkb
Sj : fB:Naigka :fB:Xgka
A:B:fXgkb -Analysis of the messages exchanged in the session Si: 1- For any Nai: a- When sending: rS+i = fNai:Agkb (in a sending step, the lower bound is used) 8Nai:fm0 2 MpGj9 0 = mgu(m0; rS+i )g = 8Nai:fm0 2 MpGj9 0 = mgu(m0; fNai:Agkb )g = f(fNA1 :A1gkB1 ; 10); (fX2gkB4 ; 20); (fY1:A4gkB5 ; 30)g such that: 8< 10 = fNA1 7 ! Nai; A1 7 ! A; kB1 7 ! kbg
20 = fX2 7 ! Nai:A; kB4 7 ! kbg : 30 = fY1 7 ! Nai; A4 7 ! A; kB5 7 ! kbg Wp0;F (Nai; fNai:Agkb ) = fDenition of the lower bound of the Witness-Function g F (Nai; @[Nai]fNA1 :A1gkB1 10) u F (Nai; @[Nai]fX2gkB4 20)u F (Nai; @[Nai]fY1:A4gkB5 30) = fSetting the static neighborhood g F (Nai; @[Nai]fNai:Agkb 10) u F (Nai; @[Nai]fX2gkb 20)u F (Nai; @[Nai]fY1:Agkb 30) = fDenition 43g F (Nai; fNai:Agkb ) u F (X2; @[X2]fX2gkb )u F (Y1; @[Y1]fY1:Agkb ) = fDerivation in the denition 41g F (Nai; fNai:Agkb ) u F (X2; fX2gkb ) u F (Y1; fY1:Agkb ) = fSince F = FMEKAX g fA; Bg [ fBg [ fA; Bg = fA; Bg(1.0) F (Nai; @[Nai];) = F (Nai; ;) = > (1.1) b- When receiving: RSi = ; (in a receiving step, the upper bound is used) 2- Compliance with the correctness criterion stated in the theorem 41: From (1.0) and (1.1), we have: Wp0;F (Nai; fNai:Agkb ) = fA; Bg w pNaiq u F (Nai; ;) = fA; Bg (1.2) From (1.2) we have: the messages exchanged in the session Si respect the correctness criterion stated in the theorem 41. (I) -Analysis of the messages exchanged in the session Sj: 1- For any X: a- When sending: rS+j = A:B:fXgkb Wp0;F (X; A:B:fXgkb ) = Wp0;F (X; A)uWp0;F (X; B)uWp0;F (X; fXgkb ) = >u>uWp0;F (X; fXgkb ) = Wp0;F (X; fXgkb ) (2.0) 8X:fm0 2 MpGj9 0 = mgu(m0; fXgkb )g = f(fX2gkB4 ; 10)g such that:
10 = fX2 7 ! X; kB4 7 ! kbg Wp0;F (X; fXgkb ) = fDenition of the lower bound of the Witness-Function g F (X; @[X]fX2gkB4 10) = fSetting the static neighborhood g F (X; @[X]fX2gkb 10) = fDenition 43g F (X2; @[X2]fX2gkb ) = fDerivation in the denition 41g F (X2; fX2gkb ) = fSince F = FMEKAX g fBg (2.1) b- When receiving: RSj = fB:Naigka :fB:Xgka (in a receiving step, the upper bound is used) F (X; @[X]fB:Naigka :fB:Xgka ) =F (X; @[X]fB:Naigka ) u F (X; @[X]fB:Xgka ) = F (X; fB:Naigka ) u F (X; fB:Xgka ) = > u fA; Bg = fA; Bg (2.2) 3-Compliance with the correctness criterion stated in the theorem 41: From (2.0), (2.1) and (2.2), we have: Wp0;F (X; A:B:fXgkb ) = fBg w pXq u F (X; @[X]fB:Naigka :fB:Xgka ) = pXq [ fA; Bg (2.3) From (2.3), we have: the messages exchanged in the session Sj respect the correctness criterion stated in the theorem 41. (II) From (I) and (II), the messages exchanged in the generalized role of A respect the correctness criterion stated in the theorem 41. (III) 5.2
Analysis of the generalized role of B i
As dened in the generalized roles of p, an agent B can participate in a session S0 , in which she receives the message fY:Agkb and she sends the message fB:Y gka :fB:Nbigka . This is described by the following schema:
i S0 :
fY:Agkb fB:Y gka :fB:Nbigka 1- For any N i:
b a- When sending: r+
S0i = fB:Y gka :fB:Nbigka (in a sending step, the lower bound is used) Wp0;F (Nbi; fB:Y gka :fB:Nbigka ) =Wp0;F (Nbi; fB:Y gka ) u Wp0;F (Nbi; fB:Nbigka ) = > u Wp0;F (Nbi; fB:Nbigka ) = Wp0;F (Nbi; fB:Nbigka ) (3.0) 8Nbi:fm0 2 MpGj9 0 = mgu(m0; fB:Nbigka )g = f(fB3:X1gkA3 ; 10); (fX2gkB4 ; 20); (fB7:NB7 gkA6 ; 30)g such that: 8< 10 = fB3 7 ! B; X1 7 ! Nbi; kA3 7 ! kag
20 = fX2 7 ! B:Nbi; kB4 7 ! kag : 30 = fB7 7 ! B; NB7 7 ! Nbi; kA6 7 ! kag Wp0;F (Nbi; fB:Nbigka ) = fDenition of the lower bound of the Witness-Function g F (Nbi; @[Nbi]fB3:X1gkA3 10) u F (Nbi; @[Nbi]fX2gkB4 20)uF (Nbi; @[Nbi]fB7:NB7 gkA6 30) = fSetting the static neighborhood g F (Nbi; @[Nbi]fB:X1gka 10) u F (Nbi; @[Nbi]fX2gka 20)uF (Nbi; @[Nbi]fB:Nbigka 30) = fDenition 43g F (X1; @[X1]fB:X1gka ) u F (X2; @[X2]fX2gka )uF (Nbi; @[Nbi]fB:Nbigka ) = fDerivation in the denition 41g F (X1; fB:X1gka ) u F (X2; fX2gka ) u F (Nbi; fB:Nbigka ) = fSince F = FMEKAX g fA; Bg [ fAg [ fA; Bg = fA; Bg (3.1) b- When receiving: RS0i = fY:Agkb (in a receiving step, the upper bound is used) F (Nbi; @[Nbi]fY:Agkb ) = > (3.2) Wp0;F (Y; fB:Y gka :fB:Nbigka ) = Wp0;F (Y; fB:Y gka ) u Wp0;F (Y; fB:Nbigka ) = Wp0;F (Y; fB:Y gka ) u > = Wp0;F (Y; fB:Y gka ) (3.3) 8Y:fm0 2 MpG j9 0 = mgu(m0; fB:Y gka )g = f(fB3:X1gkA3 ; 1); (fX2gkB4 ; 2)g such that: 10 = fB3 7 ! B; X1 7 ! Y; kA3 7 ! kag 20 = fX2 7 ! B:Y; kB4 7 ! kag Wp0;F (Y; fB:Y gka ) = fDenition of the lower bound of the Witness-Function g F (Y; @[Y ]fB3:X1gkA3 10) uF (Y; @[Y ]fX2gkB4 20) = fSetting the static neighborhood g F (Y; @[Y ]fB:X1gka 10) uF (Y; @[Y ]fX2gka 20) = = fDenition 43g F (X1; @[X1]fB:X1gka ) uF (X2; @[X2]fX2gka ) = fDerivation in the denition 41g F (X1; fB:X1gka ) u F (X2; fX2gka ) = fSince F = FMEKAX g fA; Bg [ fAg = fA; Bg (3.4) b- When receiving: RS0i = fY:Agkb (in a receiving step, the upper bound is used) F (Y; @[Y ]fY:Agkb ) = fA; Bg (3.5) 3- Compliance with the correctness criterion stated in the theorem 41: From (3.0), (3.1) and (3.2) we have: Wp0;F (Nbi; fB:Y gka :fB:Nbigka ) = fA; Bg w pNbiq u F (Nbi; @[Nbi]fY:Agkb ) = fA; Bg (3.6) From (3.3), (3.4) and (3.5) we have: Wp0;F (Y; fB:Y gka :fB:Nbigka ) = fA; Bg w pY q u F (Y; @[Y ]fY:Agkb ) = pY q u fA; Bg (3.7) i From (3.6) and (3.7), the messages exchanged in the session S0 respect the correctness criterion stated in the theorem 41. (IV) From (IV), the messages exchanged in the generalized role of B respect the correctness criterion stated by the theorem 41. (V) From (III) and (V), the protocol N SL respects the correctness criterion stated by the theorem 41, then it is correct with respect to the secrecy property. 6
Comparison with related works
Houmani et al. in [8,9,10,11] have dened universal functions to analyze increasing
protocols. Even if they gave a clear guideline to build safe functions, just two functions have
been dened: DEK and DEKAN. That is due to the diculty to prove that a function is
full-invariant by substitution. Henceforth, with a witness-function, there is no need to
request the property of full-invariance by substitution from an interpretation function. The
witness-function takes it in input, without this property, and solves the problem of
substitutions locally in the protocol, thanks to its construction that depends fully on the static
part of a message and thanks to its two bounds that do not depend on substitutions (bring
two properties and have one for free). This enables us to build more functions, and then, to
analyze more protocols. The bounds of a witness-function having an output free of variables
are expected to prove the correctness of protocols that could not be proven with universal
functions because of variables in output, for instance, Kerberos protocol and SET protocol
with Houmanis’ functions. Our approach does not need a complicated formalism as do the
rank-functions suggested by Schneider in [
Conclusion and future work
In this paper, we introduced the witness-functions as a technique to analyze
cryptographic protocols for secrecy. We gave the way to build them. In a future work, we intend
to dene witness-functions based on the selection of other keys (other than the most
external key) like the most internal key or all encryption keys together. In this respect, we
believe that a witness-function based on the selection of all neighbors and all encryption
keys (i.e. S( ; ffE: gkAB gkCD ) = fE; kAB1; kCD1g) could eciently deal with protocols with
the Die-Hellman property in a non-empty equational theory. In this respect, we believe
that the witness-functions are ready to deal with algebraic properties in convergent
theories. In addition, we intend to take benece of the bounds of a witness-function to
consider exchanged messages in a protocol as keys of encryption. We intend also to experiment
our witness-functions on compose protocols. Indeed, many protocols could be secure when
they are analyzed separately but may show undesirable interactions when analyzed together.
In this regard, similar researches had been led by V. Cortier, S. Ciobaca and S. Delaune
in [
Journal of