A Secure and Lightweight Three-Factor-Based Authentication Scheme for Smart Healthcare Systems by Jihyeon Ryu, Dongwoo Kang, Hakjun Lee, Hyoungshick Kim, Dongho Won

“…We propose a novel three-factor lightweight user authentication scheme that addresses these weaknesses and verifies the security of the proposed scheme using a formal verification tool called ProVerif. In addition, our proposed scheme outperforms other proposed symmetric encryption-based schemes or elliptic curve-based schemes.…”
Get full text

IMSC-EIoTD: Identity Management and Secure Communication for Edge IoT Devices by Kazi Masum Sadique, Rahim Rahmani, Paul Johannesson

“…The proposed security protocols are verified using Scyther formal verification tool, which is a popular tool for automated verification of security protocols. …”
Get full text

TLM.open: a SystemC/TLM Frontend for the CADP Verification Toolbox by Helmstetter, Claude

“…An open-source simulator for SystemC/TLM is provided but there are no tools for formal verification.In order to apply model checking to a SystemC/TLM model, a semantics for standard C++ code and for specific SystemC/TLM features must be provided. …”
Get full text

SMT-Based Consistency Checking of Configuration-Based Components Specifications by Laura Pandolfo, Luca Pulina, Simone Vuotto

“…Nowadays, it is well-established that formal verification has a great potential in reinforcing safety of critical systems, but nevertheless its application in the development of industrial products may still be a challenging activity. …”
Get full text

Comparator automata in quantitative verification by Suguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi

“…The notion of comparison between system runs is fundamental in formal verification. This concept is implicitly present in the verification of qualitative systems, and is more pronounced in the verification of quantitative systems. …”
Get full text

Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games by Xiaomin Wei, Yunwei Dong, Pengpeng Sun, Mingrui Xiao

“…Property formulae are formulated for formal verification of GCPS SMG models, so that occurrence probabilities of failed states and hazards can be obtained for system-level safety analysis. …”
Get full text

Efficient reduction of nondeterministic automata with application to language inclusion testing by Lorenzo Clemente, Richard Mayr

“…This can be used to scale up applications of automata in formal verification tools and decision procedures for logical theories. …”
Get full text

A User-Friendly Verification Approach for IEC 61131-3 PLC Programs by Jiawen Xiong, Gang Zhu, Yanhong Huang, Jianqi Shi

“…To ensure the safety of industrial control systems, it is necessary to verify the correctness of PLCs. Formal verification is considered to be an effective method to verify whether a PLC program conforms to its specifications, but the expertise requirements and the complexity make it hard to be mastered and widely applied. …”
Get full text

A Comprehensive Safety Engineering Approach for Software-Intensive Systems Based on STPA by Abdulkhaleq, Asim, Wagner, Stefan, Leveson, Nancy G

“…Formal verification and testing are complementary approaches which are used in the development process to verify the functional correctness of software. …”
Get full text
Get full text

Performance optimization of the VDFS verified file system by Konradi, Alexander V.

Get full text

Integral Quadratic Constraints and Safety Certificates for Uncertainty Characterization and Control Safety-Aware Filtering of Proximity Operations Between Satellites by Garcia Burgos, Axel

“…Techniques in robust optimization and formal verification methods are used (1) to examine the stability and robust performance of a satellite controller that considers six-dimensional, uncertain state, and often unmodeled dynamics during rendezvous and proximity operations, and (2) to explore the synthesis of control Lyapunov/barrier functions (CLFs/CBFs) using neural networks and stochastic gradient descent to provide safety-aware filtering for the fuel-optimal control policies. …”
Get full text

Simulation of timed input/output automata by Mavrommatis, Panayiotis P

Get full text

Fast, formal, local eXplainable artificial intelligence for neural network by Wong, Laurentius Reynald

“…This suggests that the methodologies used to create V can be implemented in various industries requiring formal verification. Additionally, limitations and potential future work are discussed.…”
Get full text

Identity-based anonymous remote authentication scheme for GLOMONETS by Goh, Yong Rui.

“…Following which, the report will evaluate the enhanced scheme by comparing it against some malicious attacks. Formal verification will also be presented in the form of a simulation using Coloured Petri Nets. …”
Get full text

Unifying B\"uchi Complementation Constructions by Seth J. Fogarty, Orna Kupferman, Thomas Wilke, Moshe Y. Vardi

“…Complementation of B\"uchi automata, required for checking automata containment, is of major theoretical and practical interest in formal verification. We consider two recent approaches to complementation. …”
Get full text

A case study on parametric verification of failure detectors by Thanh-Hai Tran, Igor Konnov, Josef Widder

“…In this paper, we present a case study on formal verification of both safety and liveness of the Chandra and Toueg failure detector that is based on partial synchrony. …”
Get full text

MA-TEECM: Mutual Anonymous Authentication-Based Credential Migration Technology for Mobile Trusted Execution Environments by Ziwang Wang, Liang Wang, Huili Yan

“…First, we propose a peer-to-peer credential migration model between mobile terminals based on TrustZone and SGX, which solves the single point of failure caused by attacks on trusted third parties that act as credential transfer stations and managers in traditional solutions; Second, we propose an identity authentication protocol between TEEs based on mutual anonymous authentication, and a detailed authentication process is designed based on the universal mobile TEE model; Third, we build a formal verification model using High-Level Protocol Specification Language (HLPSL). …”
Get full text

ATWin: An Improved and Detailed Startup Model of TTP/C by Tingting Yang, Xudong Sun, Baoyue Yan, Chao Tong

“…At last, there is lack of the formal verification for the validity of the standard startup model with an arbitrary number of nodes and the formal derivation of its upper bound of startup time. …”
Get full text

Hardware Trojan Detection Using Effective Property-Checking Method by Dejian Li, Qizhi Zhang, Dongyan Zhao, Lei Li, Jiaji He, Yidong Yuan, Yiqiang Zhao

“…Because of the potential security threat of hardware Trojans, they have attracted extensive attention to security issues. As a formal verification method, property checking has been proved to be a powerful solution for hardware Trojan detection. …”
Get full text

Secure-user sign-in authentication for IoT-based eHealth systems by B. D. Deebak, Fadi Al-Turjman

“…Using the formal security analysis, the prominence of the proposed strategies is proven to show the security efficiency of proposed S-USI. From the formal verification, the comparison results demonstrate that the proposed S-USI consumes less computation overhead; and thus it can be more suitable for the telecare medical information systems.…”
Get full text