Security Protocol Verification and Optimization by Epistemic Model Checking

2010 ◽  
Author(s):  
Ron van der Meyden
Keyword(s):  
Model Checking ◽  
Security Protocol ◽  
Protocol Verification ◽  
Epistemic Model

Applying SMV for Security Protocol Verification

2009 ◽  
Vol 8 (7) ◽  
pp. 1065-1070 ◽  
Author(s):  
Jia Mei ◽  
Huaikou Miao ◽  
Pan Liu
Keyword(s):  
Security Protocol ◽  
Protocol Verification

A SAT-Based Planning Approach for Finding Logical Attacks on Cryptographic Protocols

2020 ◽  
Vol 14 (4) ◽  
pp. 1-21
Author(s):  
Noureddine Aribi ◽  
Yahia Lebbah
Keyword(s):  
Model Checking ◽  
State Of The Art ◽  
Cryptographic Protocols ◽  
Protocol Verification ◽  
Planning Problem ◽  
Multiparty Communication ◽  
Planning Approach ◽  
Security Properties ◽  
Sat Solver ◽  
Security Property

Cryptographic protocols form the backbone of digital society. They are concurrent multiparty communication protocols that use cryptography to achieve security goals such as confidentiality, authenticity, integrity, etc., in the presence of adversaries. Unfortunately, protocol verification still represents a critical task and a major cost to engineer attack-free security protocols. Model checking and SAT-based techniques proved quite effective in this context. This article proposes an efficient automatic model checking approach that exemplifies a security property violation. In this approach, a protocol verification is abstracted as a compact planning problem, which is efficiently solved by a state-of-the-art SAT solver. The experiments performed on some real-world cryptographic protocols succeeded in detecting new logical attacks, violating some security properties. Those attacks encompass both “type flaw” and “replay” attacks, which are difficult to tackle with the existing planning-based approaches.

Sign in / Sign up

Export Citation Format

Share Document