The following LOTOS code describes a 3-way exchange between two principals. Its purpose is to show the intruder's interactions with trusted principals, and thus data types are simplified.
Principal A interacts through gates A_Send_B and
A_Receive_B and principal B uses gates B_Send_A and
B_Receive_A. The intruder is synchronized with each gate. His behaviour
is a loop composed of six possible actions: three actions to receive the
three messages and three actions to send them. Each time a message is received,
it is inserted in the intruder's knowledge. For clarity of this example, the
Insert function hides all the analysis of the message. The choice
operator commands the generation of all the possible distinct actions where the
message sent is in the intruder's knowledge. The structure of the intruder is
quite simple and thus can be guaranteed error free.
behaviour
Principal_A[A_Send_B,A_Receive_B](Initial_Knowledge_of_A)
|[A_Send_B,A_Receive_B]|
Intruder[A_Send_B,A_Receive_B,B_Send_A,B_Receive_A](Initial_Knowledge_of_I)
|[B_Send_A,B_Receive_A]|
Principal_B[B_Send_A,B_Receive_A](Initial_Knowledge_of_B)
where
process Principal_A[A_Send_B,A_Receive_B](Knowledge_of_A :Knowledge) : noexit :=
A_Send_B!Message_1;
A_Receive_B?Message_2 :Type_2;
A_Send_B!Message_3;
stop
endproc
process Principal_B[A_Send_B,A_Receive_B](Knowledge_of_B :Knowledge) : noexit :=
B_Receive_A?Message_1 :Type_1;
B_Send_A!Message_2;
B_Receive_A?Message_3 :Type_3;
stop
endproc
process Intruder[A_Send_B,A_Receive_B,B_Send_A,B_Receive_A]
(Knowledge_of_I :Knowledge) : noexit :=
(A_Send_B?Message_1 : Type_1;
Intruder[A_Send_B,A_Receive_B,B_Send_A,B_Receive_A](Insert(Message_1,Knowledge_of_I))
)
[]
(B_Send_A?Message_2 : Type_2;
Intruder[A_Send_B,A_Receive_B,B_Send_A,B_Receive_A](Insert(Message_2,Knowledge_of_I))
)
[]
(A_Send_B?Message_3 : Type_3;
Intruder[A_Send_B,A_Receive_B,B_Send_A,B_Receive_A](Insert(Message_3,Knowledge_of_I))
)
[]
(choice Message_1 : Type_1 [] [Message_1 is_in Knowledge_of_I] ->
B_Receive_A!Message_1;
Intruder[A_Send_B,A_Receive_B,B_Send_A,B_Receive_A](Knowledge_of_I)
)
[]
(choice Message_2 : Type_2 [] [Message_2 is_in Knowledge_of_I] ->
A_Receive_B!Message_2;
Intruder[A_Send_B,A_Receive_B,B_Send_A,B_Receive_A](Knowledge_of_I)
)
[]
(choice Message_3 : Type_3 [] [Message_3 is_in Knowledge_of_I] ->
B_Receive_A!Message_3;
Intruder[A_Send_B,A_Receive_B,B_Send_A,B_Receive_A](Knowledge_of_I)
)
endproc