Download ASLan++ specification and tutorial

D2.3 (update): ASLan++ specification and tutorial
“OO-style” notation
ActorP->send(B,M)
ActorP->receive(B,M)
ActorP->send(B,M)
ActorP->receive(B,M)
ActorP->send(B,M)
ActorP->receive(B,M)
ActorP->send(B,M)
ActorP->receive(B,M)
ActorP->send(B,M)
ActorP->receive(B,M)
ActorP->send(B,M)
ActorP->receive(B,M)
over
over
over
over
over
over
over
over
over
over
authCh
authCh
confCh
confCh
secCh
secCh
fresh_authCh
fresh_authCh
fresh_secCh
fresh_secCh
101/190
Annotated channels notation
ActorP -> B: M
B -> ActorP: M
ActorP *-> B: M
B *-> ActorP: M
ActorP ->* B: M
B ->* ActorP: M
ActorP *->* B: M
B *->* ActorP: M
ActorP *->> B: M
B *->> ActorP: M
ActorP *->>* B: M
B *->>* ActorP: M
Table 1: Channel notations in ASLan++ for CCM and ICM
“OO-style” notation
Actor->send(B,M)
over ch
Actor->receive(B,M) over ch
Annotated channels notation
Actor -ch-> B: M
B -ch-> Actor: M
Table 2: Channel notations in ASLan++ for ACM
Client to the Server, where either one of the end-points is replaced by Actor. This does
not give all protections of TLS, but is usually sufficient. If the additional properties of
replay protection, order preservation, and session distinction are needed, then they can be
constructed as described in § 2.9.6.
In Table 1, ActorP stands for Actor or any pseudonym of P it, which is either the default
pseudonym [Actor] or [Actor]_[P]. Similarly, B stands for the (intended) communication
partner of Actor or any pseudonym P of this partner, which is denoted by [B’]_[P] where
B’ is a term different from Actor with irrelevant value.
ACM. In ACM, channels are referred to by terms of type channel. Their properties are
usually declared by introducing certain pre-defined facts, introduced below, which trigger
pre-defined LTL constraints. One must of course be careful not to require non-fulfillable
(e.g., contradictory) channel properties, which would lead to a non-executable model.
As mentioned before, Table 2 shows the general syntax that ASLan++ supports for
ACM. Differently from the CCM and ICM, in ACM the arrow is labeled with the name of
the channel. The name may be used for identifying the channel to relate several send/receive
statements, as well as for stating the assumed properties of the channel.
The named channel syntax can be used only for ACM channels as assumptions, while –
even when ACM is chosen – channel goals are always expressed and interpreted in the same
way as in CCM/ICM.
Like in CCM and ICM, by default a channel does not guarantee any protection (insecure
channel), and is controlled by a Dolev-Yao intruder. The other properties of the channels
FP7-ICT-2007-1
Project No. 216471