# Cryptographic Protocol with Keyless Sensors Authentication for WBAN in Healthcare Applications
## 4 Test and Results
### Security Results Obtained from Protocol Verification Tools  
The results of the security tests carried out on the protocols using the protocol verification tools are presented in the same order in which they were reviewed in the previous sections. Hence, the results thrown by Scyther are presented first, followed by those thrown by AVISPA. Both tools were configured with the environment in which the protocol was tested. Each of them had different configurations. Scyther was configured with a minimum of five runs, which is the default for the tool. In the same way, the tool was chosen to search for all possible attacks on the protocol with a maximum number of ten patterns per claim. On its part, in AVISPA, the user only needs to choose the model on which the protocol will be tested. These models, as seen in Figure 12, are On-the-fly Model-checker (OFMC), CL-based Attack Searcher (AtSe), SAT-based Model-Checker (SATMC), and Tree Automata-based Protocol Analyzer (TA4 SP), the specific description of them can be found in [16]. In this case, the protocol was run for each of these modes.  
Some of the results obtained with Scyther are shown in Figure 13. The results are displayed in columns; the first column specifies the name given to the protocol. In such case, is an acronym for \"Cryptographic Protocol for Medical Information in Heterogeneous Devices\"; the second column shows the entity; the third column shows the communication within the protocol, that is, the side of the communication between the entities being reviewed. The next column shows the claim that is being sought; in the case of secrecy, the data that is sought is also shown, whether it is secret; in our case, it will be the symmetric key that is being obtained with a \(KDF\) function and the value \(ct_{b}\) and the message. The last two columns show the result of the claim and the comments on the claims. The results produced by the tool show only \(Ok\), indicating that the property that was demonstrated has been verified. In the comments, the legend _No attacks within bounds_ is shown, meaning that there are no attacks within the limits specified in the tool.  
These results show that the protocol covers the security services of authentication, confidentiality, and integrity. This is achieved using encrypted primitives, digital signature, KEM, and hash functions.  
Figure 14 shows the results of the AVISPA tool. Summarizing, these results indicate that the protocol is \"SAFE\". Details specify that it is safe in a limited number of sessions. In the same way, it is shown the number of nodes that were visited during the evaluation with the tool. In this case, there are five nodes, and the search time taken by the tool was 0.01s. As mentioned above, no claims are specified in this tool for the tool to be checked. However, the model in which the protocol is to be verified must be specified. The results indicate that the protocol is secure in the specified mode. Similarly, it is observed that the protocol me  
Figure 13: Results obtained by SCYTHER for the verified protocol.  
In this case, only the results of the OFMC model are shown, but it should be noted that in the remaining models that the tool can verify, the protocol also has \"SAFE\" results.  
The protocol covers the security services of authentication, confidentiality, and integrity. The protocol uses encryption primitives, digital signature, KEM, and hash functions. Hence, the protocol designed in this work has proven to be completely secure and well-constructed regarding cryptographic primitives.