SAT and SMT-Based Verification of Security Protocols Including Time Aspects

Area of Science:

• Computer Science
• Cybersecurity
• Formal Methods

Background:

• Secure communication is crucial for sensor-equipped devices and complex systems.
• Security protocols (SP) ensure system security but are complex to design and verify.
• Time primitives are increasingly used in SP due to time-dependent security requirements.

Purpose of the Study:

• To propose and investigate formal verification methods for SP in sensor networks.
• To address the verification challenges of time-dependent security properties.
• To ensure the correctness and reliability of SP in device communication.

Main Methods:

• Utilizing SAT-and SMT-based formal verification techniques.
• Employing a formal model based on networks of communicating timed automata.
• Investigating timed properties such as network delays and message lifetimes.

Main Results:

• Demonstrated a method for verifying security properties of SP in the sensor world.
• Successfully applied formal verification to time-dependent security aspects.
• Quantified the impact of network delays and message lifetimes on SP security.

Conclusions:

• Formal verification methods, particularly SAT/SMT-based approaches, are effective for validating SP in sensor networks.
• The proposed model accurately captures and verifies time-dependent security properties.
• This work enhances the security and reliability of communication in sensor-based systems.