# A Secure and Lightweight Group Mobility Authentication Scheme for 6 LoWPAN Networks
## 4 System Models
### Analysis of SVO Logic
#### 5.2.1 Symbols  
Listed below are the relevant notations and descriptions for the purpose of facilitating the following security proof. The SVO logic has the following rules:  
**Modus ponens (MP):** From \(\varphi\) and \(\varphi\supset\psi\) infer \(\psi\). It means that if you know that \(\varphi\) is true and that \(\varphi\) implies \(\psi\) (denoted as \(\varphi\supset\psi\)), then you can infer that \(\psi\) is also true. **Necessitation (Nec):** From \(\vdash\varphi\) infer \(\vdash P\) believes \(\varphi\). This rule means that if \(\varphi\) can be proven (i.e., \(\vdash\varphi\)) without assuming anything specific, it can infer that any principal \(P\) can believe \(\varphi\). This is a method of moving from logical truths to logical beliefs. **Believe axioms: BA1**: \(P\) believes \(\varphi\wedge P\) believes (\(\varphi\supset\psi\)) \(\supset P\) believes \(\psi\). If \(P\) believes both \(\varphi\) and that \(\varphi\) implies \(\psi\), then \(P\) must also believe \(\psi\). This is an example of basic logical reasoning applied to beliefs. **BA2:**\(P\) believes \(\varphi\supset P\) believes (\(P\) believes \(\varphi\)). This axiom aims to ensure that beliefs are \"closed under belief\". In other words, if \(P\) believes something, then \(P\) also believes that they believe it. **Source-association axioms: SA1:**\(P\stackrel{{ K}}{{\leftrightarrow}}Q\wedge R\) received \(\{X\,Q\}\)\(K\supset(Q\longmapsto X\wedge Q\
i K)\). Suppose \(P\) believes that \(Q\) shares a key \(K\) with \(R\), and \(R\) receives a message encrypted with \(K\); then, \(Q\) sends message X. **SA2:**\(P\stackrel{{ K}}{{\leftrightarrow}}Q\wedge R\) received \(\{X\,Q\}\)\(K\supset(Q\longmapsto X\wedge Q\
i K)\). It is a similar concept to the previous one, but it only works if there is a bidirectional or mutual key association \((P+(K)\,Q)\), meaning both parties, \(P\) and \(Q\), use the key \(K\), and the message \(X\) originates from \(Q\). **Receiving axioms: R1:**\(P\) received (\(X1\),..., \(Xn\)) \(\supset P\) received \(Xi\). According to this axiom, if \(P\) receives a list of items (X1,..., Xn), \(P\) also receives each of the individual items Xi within the list. **Seeing: S1:**\(P\) received \(X\supset P\) sees X. If \(P\) receives \(X\), then \(P\) has access to or can observe \(X\). **S2:**\(P\) sees (\(X1\),..., \(Xn\)) \(\supset P\) sees \(Xi\). If \(P\) can observe a list of items, then \(P\) can observe any individual item on that list. It is similar to **R1** in terms of \"seeing\" rather than receiving. **Saying: S3:**\(P\) said (\(X1\),..., \(Xn\)) \(\supset P\) said \(X1\)\(\wedge P\) sees X1. If \(P\) said the list (\(X1\),..., \(Xn\)), then \(P\) must have said \(X1\) and seen \(X1\). **S4:**\(P\) says (\(X1\),..., \(Xn\)) \(\supset P\) says \(X1\)\(\wedge P\) said (\(X1\),..., \(Xn\)). It follows that if \(P\) says the entire list (\(X1\),..., \(Xn\)), \(P\) says \(X1\) and the entire list (\(X1\),..., \(Xn\)). Message trustworthiness is established through this chain of \"sayings\". **Jurisdiction J1:**\(P\) controls \(\varphi\)\(\wedge P\) says \(\varphi\supset\varphi\). If \(P\) controls \(\varphi\) and \(P\) says \(\varphi\), then \(\varphi\) must be true. It is essential in information security, where an authority over certain information makes a declaration, and it is deemed true if that statement is made. **Freshness F1:** fresh (_Xi_) \(\supset\) fresh (_X1_,..., _Xn_). In the case of a fresh Xi (e.g., a new, unused nonce), the entire list (X1,..., Xn) will also be considered fresh. A scheme can benefit from this feature whenever freshness needs to be preserved across multiple elements. **Nonce-verification NV1:** fresh(X) \(\wedge\)\(P\) said X \(\supset\)\(P\) says X. When X is fresh, and P says X, then P says X now. This ensures that fresh data can be accepted as a part of current communications. **Symmetric goodness of shared keys SK1:** Shared key (\(K\), \(P\), \(Q\)) \(\equiv\) shared key (\(K\), \(Q\), \(P\)). It simply illustrates the symmetry in the relationship between two shared keys.