Download ASLan++ specification and tutorial

D2.3 (update): ASLan++ specification and tutorial
135/190
the optimization that an insecure network and the intruder can be identified, i.e. we
have a compressed transition where the intruder sends a message that is received and
answered to by the receiver, and the intruder immediately intercepts this answer.
• The ICM is more helpful in a different class of tools where the number of transitions
is less problematic, but the complexity of terms is an issue. Also, it is the abstract
reference model for our compositionality results between channels as assumptions and
channels as goals.
• The ACM, finally, allows for arbitrary LTL constraints on the sending and receiving,
e.g. resilient channels (i.e. every message is eventually received). Thus, the assumed
security properties of the channels are expressed abstractly, and — differently from
CCM — they do not need to be defined via concrete implementations.
Translation of channel goals is discussed in § 4.12.2. Here, we focus on the translation
of channels when used as an assumption, which depends on the choice of the channel model
as we discussed in detail in D3.3 [2]. In this case, we take into account the send and
receive predicates generated after the preprocessing phase described in § 4.1. In order to
make explicit that both the translation and the interpretation of such predicates can be
different according to the channel model chosen, let us illustrate the translation(s) at hand
of a concrete example (we proceed analogously for the other cases).
Each model introduces a number of symbols, facts, and rules necessary to express the
different channels as defined in D3.3. Note that freshness is not supported for CCM/ICM
channels as assumptions, while for ACM it is implied by confidentiality and weak confidentiality.
Assume that the translation process has proceeded up to the point of producing a transition rule that includes an agent receiving a message M1 on a confidential channel from A and
sending a message M2 to B on an authentic channel. For CCM/ICM let us further assume
that the agent sends M2 under pseudonym P:
A
- >* Actor : M1 ;
[ Actor ] _ [ P ] * - > B
: M2 ;
while for ACM let us further assume that the reception is on channel ch1 and transmission
is on channel ch2:
ch1 - > confidential_to ( Actor );
ch2 - >
authentic_on ( Actor );
...
A
-ch1 - > Actor : M1 ;
Actor -ch2 - > B
: M2 ;
The final translation into ASLan in the three models is as follows.
CCM:
FP7-ICT-2007-1
Project No. 216471