=Paper=
{{Paper
|id=Vol-1158/paper3
|storemode=property
|title=Secrecy by Witness Functions
|pdfUrl=https://ceur-ws.org/Vol-1158/paper3.pdf
|volume=Vol-1158
|dblpUrl=https://dblp.org/rec/conf/apn/FattahiMH14
}}
==Secrecy by Witness Functions==
https://ceur-ws.org/Vol-1158/paper3.pdf
Secrecy by Witness-Functions
Jaouhar Fattahi1 , Mohamed Mejri1 and Hanane Houmani2
1
LSI Group, Laval University, Quebec, Canada
2
University Hassan II, Morocco
Abstract. In this paper, we introduce a new type of functions to analyze crypto-
graphic protocols statically for the property of secrecy: the Witness-Functions. A
Witness-Function is a reliable protocol-dependent function intended to prove the cor-
rectness of a protocol through its growth. It bases its calculation on the static part of a
message in a role-based speci cation 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.
Keywords: Protocol, role-based speci cation, secrecy, su cient condition.
1 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 pre-
serves 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 de ne "good" metrics to evaluate the security of any atomic message. This way of
thinking has been considered in some previous works. In [1], Steve Schneider proposed the
concept of rank-functions as metrics to analyze protocols in CSP algebra. These functions
were successful in analyzing Needham-Schroeder protocol. However, a such analysis requires
the protocol implementation in CSP [2,3]. Besides, building rank-functions is not a trivial
job and their existence is not sure [4]. In [5] Abadi, using Spi-Calculus [6,7], guarantees that:
"If a protocol typechecks, then it does not leak its secret inputs". To do so, he requests from
the exchanged messages to be composed of four parts having strictly the following types: {se-
cret, public, any, confounder} in order to recognize the security level of every part. However,
this approach cannot analyze protocols that had been implemented with no respect to this
restriction. In the same vein, Houmani and al. [8,9,10,11] de ned universal functions called
interpretation functions able to analyze a protocol statically and operate on an abstraction
of the protocol called generalized roles, that generate a space of messages with variables. An
interpretation function must meet some su cient conditions to be reliable for the analysis.
Obviously, less we have conditions on functions, more we have functions and more we have
chance to get protocols proven correct since one function may fail to prove the growth of a
protocol but another may manage to do. However, we notice that the conditions on functions
were so restrictive that only two concrete functions had been proposed. We believe that the
condition related to the full-invariance by substitution, which is the property-bridge between
an analysis run on messages of the generalized roles and the conclusion made on valid traces,
is the most restrictive one. Since the aim of our approach is to build as more reliable functions
as we are able to do, we think that if we free a function from this restrictive condition, we can
build more functions. Nevertheless, freeing a function from a condition may impel us to take
additional precautions. In this work, we introduce the witness-functions to analyze crypto-
graphic protocols. We show how to build them. We show that a witness-function oers two
bounds that allow us to get rid of the restrictive condition of full-invariance by substitution
in Houmani's work by using derivation techniques. We state nally the theorem of proto-
col analysis with the Witness-Functions that sets an interesting criterion for the protocol
correctness.
Notations
Hereafter, we give some de nitions and conventions that will be used throughout the
paper.
+ We denote by C = hM, ξ, |=, 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.
• |= : is the inference system of the intruder under the equational theory. Let M be a
set of messages and m a message. M |= m means that the intruder is able to infer
m from M using her capacity. We extend this notation to traces as following: ρ |= 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 mes-
sages. 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 ∃m0 ∈
M.pm0 q 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 veri cation 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 speci cation are in [12,13,14]. Hereafter, an example of a variation of N SL
protocol written in a role-based speci cation:
m1 : A −→ B : {Na .A}kb
m2 : B −→ A : {B.Na }ka .{B.Nb }ka
m3 : A −→ B : A.B.{Nb }kb
Table 1. A variation of NSL protocol
The generalized roles of this protocol in a role-based speci cation are RG (pNSL )=
{A1G , A2G , BG1 , BG2 } where:
A1G = i.1 A −→ I(B) : {Nai .A}kb
2
AG = i.1 A −→ I(B) : {Nai .A}kb
i.2 I(B) −→ A : {B.Nai }ka .{B.X}ka
i.3 A −→ I(B) : A.B.{X}kb
BG1 = i.1 I(A) −→ B : {Y.A}kb
i.2 B −→ I(A) : {B.Y }ka .{B.Nbi }ka
BG2 = i.1 I(A) −→ B : {Y.A}kb
i.2 B −→ I(A) : {B.Y }ka .{B.Nbi }ka
i.3 I(A) −→ B : A.B.{Nbi }kb
We denote by MGp the set of messages with variables generated by RG (p), by Mp
the set of closed messages generated by substituting terms in MGp . We denote by R+
(respectively R− ) the set of sent messages (respectively received messages) by a honest
agent in the role R. Commonly , we reserve the uppercase letters for sets or sequences
of elements and the lowercase for single elements. For instance M denotes a set of
messages, m a single message, R a role composed of a sequence of steps, r a step and
R.r the role ending by the step r.
+ A valid trace is an interleaving of instantiated generalized roles where each message
sent by the intruder can be produced by her using her capacity and the previous received
messages. We denote by [[p]] the set of valid traces of p.
+ We assume that the intruder has the full-control of the net, as described in the Dolev-
Yao model [15] with no restriction neither on the size of messages nor on the number
of sessions.
2 Increasing protocols are correct with respect to the secrecy
property
To analyze a protocol, we need reliable functions to estimate the security level of every
atomic message. In this section, we state su cient 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 C -reliable interpretation functions
De nition 21 (Well-formed interpretation function)
Let F be an interpretation function.
F is well-formed in C if:
∀M, M1 , M2 ⊆ M, ∀α ∈ A(M):
F (α, {α}) =⊥
F (α, M1 ∪ M2 ) = F (α, M1 ) u F (α, M2 )
F (α, M ) = >, if α ∈
/ 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 = {α}, m2 = {β.A}k , M = {m1 , m2 } and F a well-formed interpre-
ab
tation function.
• F (α, M ) = F (α, {m1 } ∪ {m2 }) = F (α, {α}) u F (α, {β.A}kab )= ⊥ u > = ⊥
• F (β, M )= F (α, {m1 } ∪ {m2 })= F (β, {α}) u F (β, {β.A}kab )= > u F (β, {β.A}kab )
= F (β, {β.A}kab )
De nition 23 (Full-invariant-by-intruder interpretation function)
Let F be an interpretation function.
F is full-invariant-by-intruder in C if:
∀M ⊆ M, m ∈ M.M |=C m ⇒ ∀α ∈ 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 veri cation, unless α is initially intended to be known by the intruder (i.e. pK(I)q w pαq).
De nition 24 (Reliable interpretation function)
Let F be an interpretation function and C be a context.
F is C -reliable if F is well-formed and F is full-invariant-by-intruder in C.
De nition 25 [F -increasing protocol]
Let F be an interpretation function and p a protocol.
p is F -increasing in C if:
∀R.r ∈ RG (p), ∀σ ∈ Γ : X → Mp we have:
∀α ∈ 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.
De nition 26 (Secret disclosure)
Let p be a protocol and C a context.
We say that p discloses a secret α ∈ A(M) in C if:
∃ρ ∈ [[p]].(ρ |=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 veri cation C , to infer a secret α
that she is not allowed to know (expressed by: pK(I)q 6w pαq in the de nition 26).
Lemma 27
Let F be a C -reliable interpretation function and p a F -increasing protocol.
We have:
∀m ∈ M.[[p]] |=C m ⇒ ∀α ∈ A(m).(F (α, m) w pαq) ∨ (pK(I)q w pαq).
Proof. See the proof 819 in [16]
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.
Theorem 21 (Correctness of increasing protocols)
Let F be a C -reliable interpretation function and p a F -increasing protocol.
p is C -correct with respect to the secrecy property.
Proof. See the proof 820 in [16]
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 su cient
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 de nition 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 interpre-
tation 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 ex-
ternal 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 [17] to verify correspondences for security in protocols.
But rst, we introduce the notion of well-protected messages that have interesting properties
that we will use in the de nition of reliable selections.
3.1 Well-protected messages
We denote by EC the set of encryption functions and by E C the complementary set Σ\EC
in a context of veri cation C . In the de nition 31, we de ne the application keys that returns
the encryption keys of any atom α in a message m.
De nition 31 (Keys)
Let M ⊆ M, f ∈ Σ and m ∈ M .
We de ne the application Keys as follows:
Keys : A × M −→ P(P(A))
∀t1 , t2 ...tn subterms of m:
Keys(α, α) = {∅}
Keys(α, β) = ∅, if α 6= β and β ∈ A
n
Keys(α, fk (t1 , ..., tn )) = {k} ⊗ ∪ Keys(α, ti ), if fk ∈ EC
i=1
n
Keys(α, f (t1 , ..., tn )) = ∪ Keys(α, ti ), if f ∈ E C
i=1
We extend the application Keys to sets as follows:
∀M ⊆ M.Keys(α, M ) = ∪ Keys(α, m) and Keys(α, ∅) = ∅.
m∈M
De nition 32 (Equational theory, rewriting system and normal form)
We assume that we can transform the equational theory ξ given in the context of veri cation
to a convergent rewriting system →ξ such that:
∀m ∈ M, ∀α ∈ A(m), ∀l → r ∈→ξ , Keys(α, r) ⊆ Keys(α, l) (3.1.1)
We denote by m⇓ the normal form of m in →ξ .
The normal form of a message in the de nition 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 theo-
ries [18,19,20].
In the de nition 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 de ned in 32.
De nition 33 (Access)
Let M ⊆ M, f ∈ Σ and m ∈ M .
We de ne the application Accessor as follows:
Access : A × M −→ P(P(A))
∀t1 , t2 ...tn subterms of m:
Access(α, α) = {∅}
Access(α, β) = ∅, if α 6= β and β ∈ A
n
Access(α, fk (t1 , ..., tn )) = {k −1 } ⊗ ∪ Access(α, ti ), if fk ∈ EC and fk (t1 , ..., tn ) = fk (t1 , ..., tn )⇓
i=1
n
Access(α, f (t1 , ..., tn )) = ∪ Access(α, ti ), if f ∈ E C and fk (t1 , ..., tn ) = fk (t1 , ..., tn )⇓
i=1
Access(α, f (t1 , ..., tn )) = Access(α, f (t1 , ..., tn )⇓ ), if not.
We extend the application Access to sets as follows:
∀M ⊆ M.Access(α, M ) = ∪ Access(α, m) and Access(α, ∅) = ∅.
m∈M
Example 34 Let m be a message such that: m = {{A.D.α}k .α.{A.E.{C.α}k }k }k ;
ab ef ab ac
−1 −1
Access(α, m) = {{kac −1
, kab }, {kac }, {kac , kab , kef }}.
−1 −1 −1
In the de nition 35, we de ne 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 −1 q w pαq after elimination of unnecessary keys by the normal form de ned in 32.
De nition 35 (Well-protected message)
Let C be context of veri cation, m ∈ M, M ⊆ M and α ∈ A(m) such that pαq A ⊥.
We say that α is well-protected in m if:
∀K ∈ Access(α, m).pKq w pαq
We say that α is well-protected in M if:
∀m ∈ M.α is well-protected in m
We say that m is well-protected in C if:
∀α ∈ A(m).α is well-protected in m
We say that M is well-protected in C if:
∀m ∈ M.m is well-protected in C.
In the de nition 36, we de ne 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 de ned in 32.
De nition 36 (Clear)
Let m ∈ M and M ⊂ M.
Clear(m) = {α ∈ A(m)| ∅ ∈ Access(α, m)}
We extend this de nition to sets as follows:
Clear(M ) = ∪ Clear(m)
m∈M
Lemma 37
Let M be a set of well-protected messages in M. We have:
M |=C m ⇒ ∀α ∈ A(m).(α is well-protected in m) ∨ (pK(I)q w pαq)
Proof. See the proof 912 in [16]
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 −1 q 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 k 0 such
that pk 0−1 q w pk −1 q 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 |=C α ⇒ pK(I)q w pαq.
Proof. See the proof 914 in [16]
3.2 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 suit-
able homomorphisms, provide reliable interpretation functions. The de nition 39 introduces
the notion of a well-formed selection and the de nition 310 introduces the notion of a full-
invariant-by-intruder selection.
De nition 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:
S(α, {α}) = A,
S(α, M1 ∪ M2 ) = S(α, M1 ) ∪ S(α, M2 ),
S(α, M ) = ∅, if α ∈
/ A(M )
For an atom α in a set of messages M , a well-formed selection returns all the atoms in
M if M = {α}. 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 .
De nition 310 (Full-invariant-by-intruder selection)
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:
∀M ⊆ M, m ∈ M, we have:
M |=C m ⇒ ∀α ∈ A(m).(S(α, m) ⊆ S(α, M )) ∨ (pK(I)q w pαq)
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 de nition 310.
De nition 311 (Reliable selection)
Let S : A × M 7−→ 2A be a selection and C be a context of veri cation.
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 de ne a generic class of selections that we call SGen EK
and we prove that any in-
stance of this class is C -reliable. Then we instantiate concrete selections from this class.
De nition 312 (SGen
EK
: selection inside the protection of an external key)
We denote by SGen
EK
the class of all selections S that meet the following conditions:
• S(α, α) = A;
(3.3.1)
• S(α, m) = ∅, if α 6∈ A(m);
(3.3.2)
• ∀α ∈ A(m), where m = fk (m1 , ..., mn ) :
S(α, m) ⊆ ( ∪ A(mi )∪{k −1 }\{α}) if fk ∈ EC and pk −1 q w pαq and m = m⇓ (3.3.3)
1≤i≤n
• ∀α ∈ A(m), where m = f (m1 , ..., mn ) :
if fk ∈ EC and pk−1 q 6w pαq and m = m⇓ (a)
∪ S(α, mi )
1≤i≤n
S(α, m) = ∪ S(α, mi ) if f ∈ E C and m = m⇓ (b) (3.3.4)
1≤i≤n
if m 6= m⇓ (c)
S(α, m⇓ )
• S(α, {m} ∪ M ) = S(α, m) ∪ S(α, M )
(3.3.5)
For an atom α in an encrypted message m = fk (m1 , ..., mn ), a selection S as de ned 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 ∪ A(mi )∪{k −1 }\{α}
1≤i≤n
in the equation 3.3.3. The most external protective key (or simply the external key) is the
most external one that satis es pk −1 q 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 sepa-
rately 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).
EK
SGen de nes a generic class of selections since it does not identify what atoms to select pre-
cisely inside the protection of the external key. It identi es only the atoms that are candidates
for selection and among them we are allowed to return any subset.
Proposition 313
Let S ∈ SGen
EK
and C be a context of veri cation.
Let's have a rewriting system →ξ such that ∀m ∈ M, ∀α ∈ A(m) ∧ α 6∈ Clear(m), we have:
∀l → r ∈→ξ , S(α, r) ⊆ S(α, l) (3.3.6)
We have:
S is full-invariant-by-intruder in C .
Proof. See the proof 107 in [16]
Remark 314 (Scope)
The condition on the rewriting system →ξ given by the equation 3.3.6 in the de nition 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 mes-
sage. For example, let m = {α.C}kab be a message in a homomorphic cryptography (i.e.
{α.C}kab = {α}kab .{C}kab ). In the form {α.C}kab , the selection S(α, {α.C}kab ) may select
C , but in the form {α}kab .{C}kab , the selection S(α, {α}kab .{C}kab ) may not. Then, we must
make sure that the rewriting system →ξ we are using is oriented in such way that it chooses
the form {α}kab .{C}kab rather than the form {α.C}kab 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
veri cation 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 SGen
EK
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 = {A, B} and
m = {A.C.α.D}kab . Let S1 , S2 and S3 be three selections such that: S1 (α, m) = {kab −1
},
S2 (α, m) = {A, C, kab } and S3 (α, m) = {A, C, D, kab }. These three selections are C -reliable.
−1 −1
3.4 Instantiation of reliable selections from the class SGen
EK
Now that we de ned a generic class of reliable selections SGen EK
, we will instantiate some
concrete selections from it, that are naturally reliable. Instantiating SGen
EK
consists in de ning
selections that return precise sets of atoms among the candidates allowed by SGen EK
.
3.4.1 The selection SM
EK
AX : is the instance of the class SGen that returns for an atom
EK
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 SEK
EK
: is the instance of the class SGen
EK
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 SN
EK
: is the instance of the class SGen
EK
that returns only its neigh-
bors, that are principal identities, inside the protection of the external protective key. (N
means: Neighbors)
Several other selections could be de ned such that the selections inside the most internal
key or inside all the keys together since they are all subselections inside the external key.
Example 316
Let α be an atom and m a message such that: pαq = {A, C} and m ={{{α.C}kab .B}kac .D}kad
EK −1 EK −1 EK
SM AX (α, m) = {C, B, kac }; SEK (α, m) = {kac }; SN (α, m) = {C, B}
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.
Proposition 317
Let ψ be a homomorphism de ned as follows:
ψ : (2A )⊆ 7→ (
Lw
> if M = ∅
M 7→ u ψ(α) if not.
α∈M
{α} if α ∈ I (Principal Identities)
such that: ψ(α) =
pαq if not.
We have: FM
EK
AX = ψ ◦ SM AX , FEK = ψ ◦ SEK and FN
EK EK EK EK EK
= ψ ◦ SN are C -reliable.
Proof. See the proof 1110 in [16]
The homomorphism ψ de ned 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 veri cation. ψ 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 well-
formed. Generally, any function ψ ◦ S remains reliable for any selection S that is an instance
of SGen
EK
.
Example 318
Let α be an atom, m a message and kab a key such that: pαq = {A, B}; m = {A.C.α.D}kab ;
−1
kab = kab ; pkab q = {A, B};
EK
SEK (α, m) = {kab −1
}; SN
EK
(α, m) = {A, C, D}; SM
EK
AX (α, m) = {A, C, D, kab };
−1
FEK (α, m) = ψ ◦ SEK (α, m) = pkab q = {A, B}; FN (α, m) = ψ ◦ SN (α, m) = {A, C, D};
EK EK −1 EK EK
AX (α, m) = ψ ◦ SM AX (α, m) = {A, C, D}upkab q = {A, C, D} u {A, B} = {A, C, D, B}.
EK EK −1
FM
4 The Witness-Functions
In the previous section, we presented a constructive way of a class of selection-based func-
tions 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 in nite. The nite set of the generalized roles contains variables. The func-
tions we de ned are not "enough prepared" to analyze messages with variables because they
are not supposed to be full-invariant by substitution (or stable by substitution) [21,22,23].
The full-invariance by substitution is the property-bridge that allows us to perform an anal-
ysis over messages with variables and propagate the conclusion made-on to closed messages.
In the following section, we deal with the substitution question. We introduce the notion of
derivation to reduce the impact of variables and we build the witness-functions that operate
on derivative messages rather than messages themselves. As we will see, the witness-functions
provide two interesting bounds that are independent of all substitutions and hence we solve
the problem of substitution. We last de ne a criterion of protocol correctness based on these
two bounds. The fact that the criterion is independent of all substitutions enables an analysis
to be run on generalized roles and the decision made-on to be exported to valid traces.
4.1 Derivative message
Let m, m1 , m2 ∈ M; X m = V ar(m); S1 , S2 ⊆ 2Xm ; α ∈ A(m); X, Y ∈ Xm and be the
empty message.
De nition 41 (Derivation)
We de ne the derivative message as follows:
∂X =
∂X α =α
∂X X =
∂X Y =Y
∂X f (m) = f (∂X m), f ∈ EC ∪ E C
∂{X} m = ∂X m
∂[X]m = ∂{Xm \X} m
∂S1 ∪S2 m = ∂S2 ∪S1 m= ∂S1 ∂S2 m= ∂S2 ∂S1 m
For the sake of simpli cation, we denote by ∂m the expression ∂Xm m. The operation of
derivation in the de nition 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 = {A.X.Y }k where A and kab are static and X and Y are two vari-
ab
ables. We have: ∂m = {A}kab ; ∂X m = {A.Y }kab ; ∂[X]m = {A.X}kab
De nition 43
Let m ∈ MGp , X ∈ Xm and mσ be a closed message.
For all α ∈ A(mσ), σ ∈ Γ , we denote by:
if α 6∈ A(mσ),
>
F (α, ∂[α]mσ) = F (α, ∂m) if α ∈ A(∂m),
F (X, ∂[X]m) if α ∈ A(Xσ) ∧ α ∈
/ A(∂m).
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 SGenEK
, 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 "side-
eects" 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 =
{α.B.X}kad and m2 = {α.Y.C}kad and pαq = {A, D}. Let m = {α.B.C}kad be in a valid
trace generated by p.
(
EK {B, A, D} if m comes by the substitution of X by C in m1
FM AX (α, ∂[α]m) =
{A, D, C} if m comes by the substitution of Y by B in m2
Hence FM AX (α, ∂[α]m) is not even a function on the closed message m since it may return
EK
more than one image for the same preimage. This leads us straightly to the witness-functions.
4.2 The Witness-Functions
De nition 45 (Witness-Function)
Let m ∈ MGp , X ∈ Xm and mσ be a closed message.
Let p be a protocol and F be a C -reliable interpretation function.
We de ne a witness-function Wp,F for all α ∈ A(mσ), σ ∈ Γ , as follows:
Wp,F (α, mσ) = u F (α, ∂[α]m0 σ 0 )
m0 ∈MGp
∃σ 0 ∈Γ.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 SGen
EK
.
As seen in the example 44, the application de ned in 43 is not necessary a function in the
set MGp of messages generated by the generalized roles of p since a valid trace could have more
than one source in MGp 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 MGp . 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 asso-
ciated interpretation function calculates the security level of an atom always in a message m
having an encryption pattern, i.e. when fk ∈ EC , the search of all sources of m in the set
{m0 ∈ MGp |∃σ 0 ∈ Γ.m0 σ 0 = mσ} is reduced to a search in the encryption patterns in MGp .
4.3 Inheritance of reliability properties from F
Proposition 47
Let Wp,F be a witness-function inside the protection of an external key.
We have:
Wp,F inherits reliability from F
Proof. See the proof 122 in [16]
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 SGen
EK
and so full-
invariant-by-intruder. Since the witness-function is the composition of the homomorphism
associated with F and an instance of the class SGenEK
, then it is reliable.
Example 48
Let MGp = {{α.B.X}kad , {α.Y.C}kad , {A.Z}kbc }; m1 = {α.B.C}kad ; V ar(MGp ) = {X, Y, Z}.
Wp,FM
EK (α, m1 )
AX
= {De nition 45}
EK 0 0 EK 0 0
u FM AX (α, ∂[α]m σ ) = u FM AX (α, ∂[α]m σ )
m0 ∈MGp
{{α.B.X}k
ad
,{α.Y.C}k
ad
}
∃σ 0 ∈Γ.m0 σ 0 =m 1 σ 0 ={X7−→C,Y 7−→B}
= {Wp,FMEK
AX
is well-formed from the proposition 47 }
EK EK
FM AX (α, ∂[α]{α.B.X}kad [X 7−→ C])uFM AX (α, ∂[α]{α.Y.C}kad [Y 7−→ B])
={De nition 43 and derivation in 41}
EK EK
FM AX (α, {α.B}kad ) u FM AX (α, {α.C}kad )
= {De nition of FM AX }
EK
{B, A, D} ∪ {C, A, D} = {B, A, D, C}
4.4 Bounding a Witness-Function
Lemma 49
Let m ∈ MGp and Wp,F be a witness-function inside the protection of an external key.
∀σ ∈ Γ, ∀α ∈ A(Mp ) we have:
F (α, ∂[α]m) w Wp,F (α, mσ) w u F (α, ∂[α]m0 σ 0 )
m0 ∈MG
p
∃σ 0 =mgu(m0 ,m)
Proof. See the proof 124 in [16]
The upper bound of a witness-function estimates the security level of an atom from one
con rmed 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 uni cation in the lower bound
"hunts" the candidates from all the likely sources of the closed message in the protocol.
4.5 Su cient 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 su cient condition of correctness of p with respect to the secrecy property is:
∀R.r ∈ RG (p), ∀α ∈ A(r+ ) we have:
u F (α, ∂[α]m0 σ 0 ) w pαq u F (α, ∂[α]R− )
m0 ∈MG
p
∃σ 0 =mgu(m0 ,r + )
Proof. See the proof 125 in [16]
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 veri cation such that: pAq = ⊥; pBq = ⊥; pNai q = {A, B} (secret
shared between A and B ); pNbi q = {A, B} (secret shared between A and B ); pka−1 q = {A};
pkb−1 q = {B}; (L, w, t, u, ⊥, >) = (2I , ⊆, ∩, ∪, I, ∅); I = {I, A, B, A1 , A2 ,B1 , B2 , ...};
The set of messages generated by the protocol is MGp = {{NA1 .A1 }kB1 , {B2 .NA2 }kA2 ,
{B3 .X1 }kA3 , {X2 }kB4 , {Y1 .A4 }kB5 , {B6 .Y2 }kA5 , {B7 .NB7 }kA6 , {NB8 }kB8 }
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, MGp = {{NA1 .A1 }kB1 , {B2 .NA2 }kA2 , {B3 .X1 }kA3 , {X2 }kB4 ,
{Y1 .A4 }kB5 , {B7 .NB7 }kA6 , {NB8 }kB8 }
Let's select the Witness-Function as follows:
p = N SL; F = FM AX ; Wp,F (α, mσ) =
EK
u F (α, ∂[α]m0 σ 0 );
m0 ∈MG
p
∃σ 0 .m0 σ 0 =mσ
Let's denote the lower bound of the Witness-Function in the theorem 41 by:
0
Wp,F (α, r+ ) = u F (α, ∂[α]m0 σ 0 )
m0 ∈MG
p
∃σ 0 =mgu(m0 ,r + )
Please notice that all messages are in their normal form since no equational theory is de-
ned. Principal identities in the context are not analyzed since they are declared public. The
protocol is analyzed for the property of secrecy only.
5.1 Analysis of the generalized role of A
As de ned in the generalized roles of p, an agent A can participate in two consequent
sessions: S i and S j such that j > i. In the former session S i , the agent A receives nothing
and sends the message {Nai .A}kb . In the consequent session S j , she receives the message
{B.Nai }ka .{B.X}ka and she sends the message A.B.{X}kb . This is described by the following
schema:
2 {B.Nai }ka .{B.X}ka
Si : i
Sj :
{Na .A}kb A.B.{X}kb
-Analysis of the messages exchanged in the session S i :
1- For any Nai :
a- When sending: rS+i = {Nai .A}kb (in a sending step, the lower bound is used)
∀Nai .{m0 ∈ MGp |∃σ 0 = mgu(m0 , rS+i )}
= ∀Nai .{m0 ∈ MGp |∃σ 0 = mgu(m0 , {Nai .A}kb )}
= {({NA1 .A1 }kB1 , σ10 ), ({X2 }kB4 , σ20 ), ({Y1 .A4 }kB5 , σ30 )} such that:
0
σ1 = {NA1 7−→ Nai , A1 7−→ A, kB1 7−→ kb }
σ 0 = {X2 7−→ Nai .A, kB4 7−→ kb }
20
σ3 = {Y1 7−→ Nai , A4 7−→ A, kB5 7−→ kb }
0
Wp,F (Nai , {Nai .A}kb )
= {De nition of the lower bound of the Witness-Function}
F (Nai , ∂[Nai ]{NA1 .A1 }kB1 σ10 ) u F (Nai , ∂[Nai ]{X2 }kB4 σ20 )u F (Nai , ∂[Nai ]{Y1 .A4 }kB5 σ30 )
= {Setting the static neighborhood}
F (Nai , ∂[Nai ]{Nai .A}kb σ10 ) u F (Nai , ∂[Nai ]{X2 }kb σ20 )u F (Nai , ∂[Nai ]{Y1 .A}kb σ30 )
= {De nition 43}
F (Nai , {Nai .A}kb ) u F (X2 , ∂[X2 ]{X2 }kb )u F (Y1 , ∂[Y1 ]{Y1 .A}kb )
= {Derivation in the de nition 41}
F (Nai , {Nai .A}kb ) u F (X2 , {X2 }kb ) u F (Y1 , {Y1 .A}kb )
= {Since F = FM EK
AX }
{A, B} ∪ {B} ∪ {A, B} = {A, B}(1.0)
b- When receiving: RS−i = ∅ (in a receiving step, the upper bound is used)
F (Nai , ∂[Nai ]∅) = F (Nai , ∅) = > (1.1)
2- Compliance with the correctness criterion stated in the theorem 41:
From (1.0) and (1.1), we have: Wp,F
0
(Nai , {Nai .A}kb ) = {A, B} w pNai q u F (Nai , ∅) = {A, B}
(1.2)
From (1.2) we have: the messages exchanged in the session S i respect the correctness criterion
stated in the theorem 41. (I)
-Analysis of the messages exchanged in the session S j :
1- For any X :
a- When sending: rS+j = A.B.{X}kb
0 0 0 0 0
Wp,F (X, A.B.{X}kb ) = Wp,F (X, A)uWp,F (X, B)uWp,F (X, {X}kb ) = >u>uWp,F (X, {X}kb ) =
Wp,F (X, {X}kb ) (2.0)
0
∀X.{m0 ∈ MGp |∃σ 0 = mgu(m0 , {X}kb )} = {({X2 }kB4 , σ10 )} such that:
σ10 = {X2 7−→ X, kB4 7−→ kb }
0
Wp,F (X, {X}kb )
= {De nition of the lower bound of the Witness-Function}
F (X, ∂[X]{X2 }kB4 σ10 )
= {Setting the static neighborhood}
F (X, ∂[X]{X2 }kb σ10 )
= {De nition 43}
F (X2 , ∂[X2 ]{X2 }kb )
= {Derivation in the de nition 41}
F (X2 , {X2 }kb )
= {Since F = FM EK
AX }
{B} (2.1)
b- When receiving: RS−j = {B.Nai }ka .{B.X}ka (in a receiving step, the upper bound is used)
F (X, ∂[X]{B.Nai }ka .{B.X}ka ) =F (X, ∂[X]{B.Nai }ka ) u F (X, ∂[X]{B.X}ka ) =
F (X, {B.Nai }ka ) u F (X, {B.X}ka ) = > u {A, B} = {A, B} (2.2)
3-Compliance with the correctness criterion stated in the theorem 41:
From (2.0), (2.1) and (2.2), we have:
0
Wp,F (X, A.B.{X}kb ) = {B} w pXq u F (X, ∂[X]{B.Nai }ka .{B.X}ka ) = pXq ∪ {A, B} (2.3)
From (2.3), we have: the messages exchanged in the session S j respect the correctness crite-
rion 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 de ned in the generalized roles of p, an agent B can participate in a session S 0 , in
which she receives the message {Y.A}kb and she sends the message {B.Y }ka .{B.Nbi }ka . This
is described by the following schema:
i {Y.A}kb
S0 :
{B.Y }ka .{B.Nbi }ka
1- For any Nbi :
a- When sending: r+0 i = {B.Y }ka .{B.Nbi }ka (in a sending step, the lower bound is used)
S
0 0 0
Wp,F (Nbi , {B.Y }ka .{B.Nbi }ka ) =Wp,F (Nbi , {B.Y }ka ) u Wp,F (Nbi , {B.Nbi }ka ) =
> u Wp,F0 0
(Nbi , {B.Nbi }ka ) = Wp,F (Nbi , {B.Nbi }ka ) (3.0)
0 G 0 0
∀Nb .{m ∈ Mp |∃σ = mgu(m , {B.Nbi }ka )}
i
= {({B3 .X1 }kA3 , σ10 ), ({X2 }kB4 , σ20 ), ({B7 .NB7 }kA6 , σ30 )} such that:
0
σ1 = {B3 7−→ B, X1 7−→ Nbi , kA3 7−→ ka }
σ 0 = {X2 7−→ B.Nbi , kB4 7−→ ka }
20
σ3 = {B7 7−→ B, NB7 7−→ Nbi , kA6 7−→ ka }
0
Wp,F (Nbi , {B.Nbi }ka )
= {De nition of the lower bound of the Witness-Function}
F (Nbi , ∂[Nbi ]{B3 .X1 }kA3 σ10 ) u F (Nbi , ∂[Nbi ]{X2 }kB4 σ20 )uF (Nbi , ∂[Nbi ]{B7 .NB7 }kA6 σ30 )
= {Setting the static neighborhood}
F (Nbi , ∂[Nbi ]{B.X1 }ka σ10 ) u F (Nbi , ∂[Nbi ]{X2 }ka σ20 )uF (Nbi , ∂[Nbi ]{B.Nbi }ka σ30 )
= {De nition 43}
F (X1 , ∂[X1 ]{B.X1 }ka ) u F (X2 , ∂[X2 ]{X2 }ka )uF (Nbi , ∂[Nbi ]{B.Nbi }ka )
= {Derivation in the de nition 41}
F (X1 , {B.X1 }ka ) u F (X2 , {X2 }ka ) u F (Nbi , {B.Nbi }ka )
= {Since F = FM EK
AX }
{A, B} ∪ {A} ∪ {A, B} = {A, B} (3.1)
b- When receiving: R−0 i = {Y.A}kb (in a receiving step, the upper bound is used)
S
F (Nbi , ∂[Nbi ]{Y.A}kb ) = > (3.2)
2- For any Y :
a- When sending: r+0 i = {B.Y }ka .{B.Nbi }ka (in a receiving step, the upper bound is used)
S
0 0 0
Wp,F (Y, {B.Y }ka .{B.Nbi }ka ) = Wp,F (Y, {B.Y }ka ) u Wp,F (Y, {B.Nbi }ka ) =
Wp,F (Y, {B.Y }ka ) u > = Wp,F (Y, {B.Y }ka ) (3.3)
0 0
∀Y.{m0 ∈ MGp |∃σ 0 = mgu(m0 , {B.Y }ka )} = {({B3 .X1 }kA3 , σ1 ), ({X2 }kB4 , σ2 )} such that:
0
σ1 = {B3 7−→ B, X1 7−→ Y, kA3 7−→ ka }
σ20 = {X2 7−→ B.Y, kB4 7−→ ka }
0
Wp,F (Y, {B.Y }ka )
= {De nition of the lower bound of the Witness-Function}
F (Y, ∂[Y ]{B3 .X1 }kA3 σ10 ) uF (Y, ∂[Y ]{X2 }kB4 σ20 )
= {Setting the static neighborhood}
F (Y, ∂[Y ]{B.X1 }ka σ10 ) uF (Y, ∂[Y ]{X2 }ka σ20 ) =
= {De nition 43}
F (X1 , ∂[X1 ]{B.X1 }ka ) uF (X2 , ∂[X2 ]{X2 }ka )
= {Derivation in the de nition 41}
F (X1 , {B.X1 }ka ) u F (X2 , {X2 }ka )
= {Since F = FM EK
AX }
{A, B} ∪ {A} = {A, B} (3.4)
b- When receiving: R−0 i = {Y.A}kb (in a receiving step, the upper bound is used)
S
F (Y, ∂[Y ]{Y.A}kb ) = {A, B} (3.5)
3- Compliance with the correctness criterion stated in the theorem 41:
From (3.0), (3.1) and (3.2) we have:
0
Wp,F (Nbi , {B.Y }ka .{B.Nbi }ka ) = {A, B} w pNbi q u F (Nbi , ∂[Nbi ]{Y.A}kb ) = {A, B} (3.6)
From (3.3), (3.4) and (3.5) we have:
0
Wp,F (Y, {B.Y }ka .{B.Nbi }ka ) = {A, B} w pY q u F (Y, ∂[Y ]{Y.A}kb ) = pY q u {A, B} (3.7)
i
From (3.6) and (3.7), the messages exchanged in the session S 0 respect the correctness cri-
terion stated in the theorem 41. (IV)
From (IV), the messages exchanged in the generalized role of B respect the correctness cri-
terion 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 de ned universal functions to analyze increasing pro-
tocols. Even if they gave a clear guideline to build safe functions, just two functions have
been de ned: DEK and DEKAN. That is due to the di culty to prove that a function is
full-invariant by substitution. Henceforth, with a witness-function, there is no need to re-
quest 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 substi-
tutions 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 [1] that require the CSP formalism [24]. It does
not need, neither, a strongly message-typing as suggested by Abadi in [5]. Our approach
intersects Schneider's work and Houmani's work in the way of seeing the protocol correctness
through its growth and through the need to have reliable metrics to evaluate security. Besides,
all of these methods handle an unbounded number of sessions and provide a semi-decidable
procedure since they decide only when the protocol is increasing.
7 Conclusion and future work
In this paper, we introduced the witness-functions as a technique to analyze crypto-
graphic protocols for secrecy. We gave the way to build them. In a future work, we intend
to de ne witness-functions based on the selection of other keys (other than the most ex-
ternal 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
−1 −1
keys (i.e. S(α, {{E.α}kAB }kCD ) = {E, kAB , kCD }) could e ciently deal with protocols with
the Di e-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 theo-
ries. In addition, we intend to take bene ce of the bounds of a witness-function to con-
sider 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 [25,26,27] where they suggest protocol-tags to secure compose protocols. We think that
our witness-functions are prepared to deal with this question.
References
1. Steve Schneider. Verifying authentication protocols in csp. IEEE Trans. Software Eng.,
24(9):741758, 1998.
2. Steve Schneider. Security properties and csp. In IEEE Symposium on Security and Privacy,
pages 174187, 1996.
3. Steve A. Schneider and Rob Delicata. Verifying security protocols: An application of csp. In 25
Years Communicating Sequential Processes, pages 243263, 2004.
4. James Heather and Steve Schneider. A decision procedure for the existence of a rank function.
J. Comput. Secur., 13(2):317344, March 2005.
5. Martín Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46:611638, 1998.
6. Martín Abadi and Andrew D. Gordon. Reasoning about cryptographic protocols in the spi
calculus. In CONCUR, pages 5973, 1997.
7. Martín Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus.
In ACM Conference on Computer and Communications Security, pages 3647, 1997.
8. Hanane Houmani and Mohamed Mejri. Practical and universal interpretation functions for
secrecy. In SECRYPT, pages 157164, 2007.
9. Hanane Houmani and Mohamed Mejri. Ensuring the correctness of cryptographic protocols with
respect to secrecy. In SECRYPT, pages 184189, 2008.
10. Hanane Houmani and Mohamed Mejri. Formal analysis of set and nsl protocols using the
interpretation functions-based method. Journal Comp. Netw. and Communic., 2012, 2012.
11. Hanane Houmani, Mohamed Mejri, and Hamido Fujita. Secrecy of cryptographic protocols under
equational theory. Knowl.-Based Syst., 22(3):160173, 2009.
12. Mourad Debbabi, Y. Legaré, and Mohamed Mejri. An environment for the speci cation and
analysis of cryptoprotocols. In ACSAC, pages 321332, 1998.
13. Mourad Debbabi, Mohamed Mejri, Nadia Tawbi, and I. Yahmadi. Formal automatic veri cation
of authentication crytographic protocols. In ICFEM, pages 5059, 1997.
14. Mourad Debbabi, Mohamed Mejri, Nadia Tawbi, and I. Yahmadi. From protocol speci cations
to aws and attack scenarios: An automatic and formal algorithm. In WETICE, pages 256262,
1997.
15. Danny Dolev and Andrew Chi-Chih Yao. On the security of public key protocols. IEEE Trans-
actions on Information Theory, 29(2):198207, 1983.
16. Jaouhar Fattahi, Mohamed Mejri, and Hanane Houmani. The witness-functions: Proofs
and intermediate results http://web_security.fsg.ulaval.ca/lab/sites/default/files/
WF/WFFMS/WFAppend.pdf. pages 128, 2014.
17. Bruno Blanchet. Automatic veri cation of correspondences for security protocols. Journal of
Computer Security, 17(4):363434, 2009.
18. Hubert Comon-Lundh, Véronique Cortier, and Eugen Zalinescu. Deciding security properties
for cryptographic protocols. application to key cycles. ACM Trans. Comput. Log., 11(2), 2010.
19. Véronique Cortier and Stéphanie Delaune. Decidability and combination results for two notions
of knowledge in security protocols. J. Autom. Reasoning, 48(4):441487, 2012.
20. Véronique Cortier, Steve Kremer, and Bogdan Warinschi. A survey of symbolic methods in
computational analysis of cryptographic systems. J. Autom. Reasoning, 46(3-4):225259, 2011.
21. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press,
1998.
22. Nachum Dershowitz and David A. Plaisted. Rewriting. In Handbook of Automated Reasoning,
pages 535610. 2001.
23. Hubert Comon-Lundh, Claude Kirchner, and Hélène Kirchner, editors. Rewriting, Computation
and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday,
volume 4600 of Lecture Notes in Computer Science. Springer, 2007.
24. Steve A. Schneider, Helen Treharne, and Neil Evans. Chunks: Component veri cation in csp||b.
In IFM, pages 89108, 2005.
25. Stefan Ciobaca and Veronique Cortier. Protocol composition for arbitrary primitives. 2012 IEEE
25th Computer Security Foundations Symposium, 0:322336, 2010.
26. Véronique Cortier. Secure composition of protocols. In TOSCA, pages 2932, 2011.
27. Véronique Cortier and Stéphanie Delaune. Safely composing security protocols. Formal Methods
in System Design, 34(1):136, 2009.