Information Technology Reference
In-Depth Information
• c
!
m
allows the message
m
to be sent on channel
c
.
• c
?
x
allows messages
m
to be received on channel
c
. The message received
substitutes the variable
x
.
-
[
m
1
...m
n
r
x
]
A
1
is the inference construct. If, applying a case of inference
schema
r
with the premises
m
1
...m
n
, a message
m
can be inferred, then
the process behaves as
A
1
(where
m
substitutes
x
). This is the message-
manipulating construct of the language for modeling cryptographic opera-
tions.
-
A compound system
S \ L
allows only external actions whose channel is not
in
L
. The internal action
τ
, which denotes an internal communication among
agents, is never prevented.
-
A compound system
S | S
1
performs an action
a
if one of its sub-components
performs
a
. A synchronization or internal action, denoted by the symbol
τ
,
may take place whenever
S
and
S
1
are able to perform two complementary,
i.e. send-receive, actions.
-
Finally, the term
A
φ
represents a system which consists of a single sequential
agent whose knowledge, i.e. the set of messages which occur in its term
A
,
is described by
φ
. The agent's knowledge increases as it receives messages
(see rule (?)), infers new messages from the messages it knows (see rule
D
1
).
Sometimes we omit to represent agent's knowledge when this can be easily
inferred from the context.
We assume on the process terms some well-formedness conditions that can be
statically checked. In particular the inference construct [
m
1
...m
n
r
x
]
A
1
binds
the variable
x
in
A
1
. The prefix construct
c
?
x.A
binds the variable
x
in
A
.We
assume that each variable may be bound at most once. For every sequential
agent
A
φ
, we require that all the closed messages and free variables (i.e., not
bound) that appear in the term
A
belong to its knowledge
φ
. A sequential agent
is said to be closed if
φ
consists only of closed messages.
2.3 Symbolic Semantics
In the symbolic semantics, we may have some CryptoCCS terms that present
in their knowledge
φ
some variables. The actual values that can be substituted
to the variables in order to have a common CryptoCCS process will be denoted
through a symbolic language. This language will encode the possible substi-
tutions from variables to closed messages. For instance, we can denote that a
variable
x
may be the application of the message constructor
F
to every message
by simply requiring
x ∈ F
(
y
). Indeed, variable
y
is not constrained and so its
value can range over all possible messages. We can also join two constraints:
e.g.,
x ∈ F
(
y
)
,y ∈ m
(where
m
is closed) simply represents that
x
must be
equal to
F
(
m
) and
y
to
m
. During the analysis of a security protocol is also
useful to be able to express that a variable may store whatever message one
can deduce from a certain set of messages. This enable us to model what an in-
truder may send to the system under attack by using the set of messages it has
already acquired during the computation, i.e. its knowledge
φ
. Indeed, we use
