Download ASLan++ specification and tutorial

D2.3 (update): ASLan++ specification and tutorial
110/190
name:(_) {A1, A2, ...}
where the goal name is augmented with a parameter placeholder (_) to indicate that in
sub-entities the goal name will appear again, in the form of a goal label, with a term as its
argument.
Its interpretation is that the values annotated with the goal labels must be known only
to the agents referred to in the set literal {A1, A2, ...}.
All terms A1, A2, etc. must re-appear as actual arguments in the instantiations of all
sub-entities sharing the secret. In each sub-entity42 , whenever a term labeled with the goal
name is evaluated, the set of the “knowing” agents is computed from the current values of
those parameters that have been matched as just described.
The goal labels should be given in all sub-entities that may know the secret value, as
early as possible, for instance when the value is produced or learned by the respective entity
instance, for example:
entity Session (A , B : agent ) {
entity Alice ( Actor , B : agent ) {
symbols
Nonce : message ;
...
body {
...
secret_Nonce :( Nonce ) := fresh ();
Actor -> B : ... Nonce ...;
% send Nonce to B , somehow confidentiality protected
...
}
}
entity Bob (A , Actor : agent ) {
symbols
N_A : message ;
...
body {
...
A -> Actor : ... secret_Nonce :(? N_A )...;
% receive Nonce from A , somehow confidentiality protected
...
}
}
body {
new Alice (A , B );
42
According to current translator restrictions, only direct sub-entities are supported for secrecy goals.
FP7-ICT-2007-1
Project No. 216471