2.2.2 Sequence of events
Each role in the protocol corresponds to the event list. In other words, a structure is imposed on the protocol event set belonging to the role R, and the total sequence is expressed as $ \prec $, so any role R∈Role and $\varepsilon 1$ ,$\varepsilon 2$ ∈ RoleEvent, so Role($\varepsilon 1$)=R and role($\varepsilon 2$)=R we have Such expression: $ \varepsilon 1 \prec \varepsilon 2\vee \varepsilon 1=\varepsilon 2\vee \varepsilon 1\succ R\varepsilon 2$ We consider an abstract security protocol P as a collection of communication sequential processes. Each sequence component is carried by a specific role. The communication is managed by the label of the decoration event, because the label directly determines the relationship of the communication.
Define 2.10 (Communication relationship): All $\imath $∈Label, m1, m2 ∈ Role × Role × RoleTerm, the communication relationship? Expressed as:
$\varepsilon 1 $? $\varepsilon 2\Leftrightarrow \exists \imath $ m1,m2:$\varepsilon 1=send \imath (m1) \Lambda \varepsilon 2=read \imath (m2)$. This relationship stipulates the sending agreement event and How to correspond to the agreement acceptance event,
Example: 2.1.1 (Event role and communication relationship): For example, the NS protocol, the order of roles $\prec$ i and $\prec$ r are roles i and r, They are expressed as follows:
Communication Relationship? Give the following expressions:
< p>2.2.3 Static requirements
In the previous chapter, we explained the abstract protocol specification syntax. Appropriate protocol specifications must meet many good formal requirements. It is not a secure protocol for sending, declaring, and reading event sequences. For example, we require the agent to be able to construct the terminology clauses he sends, if he does not know the secret. The key cannot check the content of the encrypted term.
Good role: For each role, we require him to meet certain basic standards, these scopes are quite obvious, for example: each event in the role definition has the same role to perform it ( Are called participants in the event), a more subtle request for the message. For messages, we require that the sent message can actually have a sender structure. If the message is in the sending role, this requirement is met. For variables, we require that they first appear in a read event, be actualized in this event, and then they can appear in a sending event.
For reading events, the situation is much more complicated. As can be seen from the examples above, we describe the initial role of the protocol Needham-Schroeder. The reading event imposes a structure on the incoming message. In the form of the pattern, if the recipient’s knowledge meets certain requirements, then he can only match the message with this expected pattern.
We introduce a form of prediction WF (Well-Formed) means that the role definition meets these consistency requirements, using auxiliary prediction RD (Readable) and an inferential knowledge relationship $ \vdash $: RoleKnow × RoleTerm
The role can form and decompose term pairs. If the agent knows the encryption key, the term can be encrypted, and if the agent knows the decryption key, the encrypted term can also be decrypted.
Definition 2.12 (Knowledge Reasoning Operation)
Using M as the role knowledge set, the knowledge reasoning relationship $ \vdash $: RoleKnow × RoleTerm The definition is summarized as follows: For the desired role term rt , Rt1, rt2, k
Liezi 2.13 (Inference and Encryption)
From a term set containing {/m/}k terms, excluding $k^{-1}$ cannot infer m or k ,i ,e
given term expression {/m/}k and $k^{-1}$, we can infer m, if k is an asymmetric key (this means that k is not equal to $k^{-1}$)