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.

Modeling security properties of authentication of cryptographic protocols using spin formal verification

2020 ◽  
pp. 21-25
Author(s):  
E.A. Perevyshina ◽  
L.K. Babenko
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Temporal Logic ◽  
Cryptographic Protocols ◽  
Wide Range ◽  
Security Properties ◽  
Verification Tools ◽  
The Stability ◽  
Security Property ◽  
Ltl Model Checking

To assess the quality and security of cryptographic protocols, we use various formal verification tools, such as Scyther tool, Avispa, ProVerif. these formal verifiers can check the protocol for vulnerability to attacks on secrecy and authentication, as these are the most prevalent attacks on protocols. However, this is not enough to fully analyze the security of the protocol. In this article, we will use linear temporal logic (LTL) model checking with SPIN. This tool, unlike the formal verifiers listed above, is not designed for a specific application in the context of cryptographic protocols; however, it has a very wide range of possibilities. In particular, for each security property, it is possible to describe the behavior of an attacker and test for the stability of the protocol model to its various attacks. The purpose of this work is to describe the developed methodology for verifying the security of authentication properties using the SPIN verifier.

scholarly journals Property Directed Reachability for Automated Planning

2014 ◽  
Vol 50 ◽  
pp. 265-319 ◽  
Author(s):  
M. Suda
Keyword(s):  
Model Checking ◽  
State Of The Art ◽  
Automated Planning ◽  
The State ◽  
Experimental Comparison ◽  
Specific Procedure ◽  
Transition Systems ◽  
Planning Algorithm ◽  
Sat Solver ◽  
Recent Method

Property Directed Reachability (PDR) is a very promising recent method for deciding reachability in symbolically represented transition systems. While originally conceived as a model checking algorithm for hardware circuits, it has already been successfully applied in several other areas. This paper is the first investigation of PDR from the perspective of automated planning. Similarly to the planning as satisfiability paradigm, PDR draws its strength from internally employing an efficient SAT-solver. We show that most standard encoding schemes of planning into SAT can be directly used to turn PDR into a planning algorithm. As a non-obvious alternative, we propose to replace the SAT-solver inside PDR by a planning-specific procedure implementing the same interface. This SAT-solver free variant is not only more efficient, but offers additional insights and opportunities for further improvements. An experimental comparison to the state of the art planners finds it highly competitive, solving most problems on several domains.

Formal Modeling and Verification of Security Property in Handel C Program

2012 ◽  
Vol 3 (3) ◽  
pp. 50-65
Author(s):  
Yujian Fu ◽  
Jeffery Kulick ◽  
Lok K. Yan ◽  
Steven Drager
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
Formal Specification ◽  
Critical Systems ◽  
Formal Approach ◽  
C Programs ◽  
Translation Rule ◽  
Security Properties ◽  
C Program ◽  
Security Property

Multi-million gate system-on-chip (SoC) designs easily fit into today’s Field Programmable Gate Arrays (FPGAs). As FPGAs become more common in safety-critical and mission-critical systems, researchers and designers require information flow guarantees for the FPGAs. Tools for designing a secure system of chips (SOCs) using FPGAs and new techniques to manage and analyze the security properties precisely are desirable. In this work we propose a formal approach to model, analyze and verify a typical set of security properties – noninterference – of Handel C programs using Petri Nets and model checking. This paper presents a method to model Handel C programs using Predicate Transition Nets, a type of Petri Net, and define security properties on the model, plus a verification approach where security properties are checked. Three steps are used. First, a formal specification on the Handel C description using Petri Nets is extracted. Second, the dynamic noninterference properties with respect to the Handel C program statements are defined on the model. To assist in verification, a translation rule from the Petri Nets specification to the Maude programming language is also defined. Thus, the formal specification can be verified against the system properties using model checking. A case study of the pipeline multiplier is discussed to illustrate the concept and validate the approach.

Chapter 19. Planning and SAT

2021 ◽  
Author(s):  
Jussi Rintanen
Keyword(s):  
Artificial Intelligence ◽  
Model Checking ◽  
Bounded Model Checking ◽  
Planning Problem ◽  
Ai Planning ◽  
Transition Systems ◽  
Computer Aided ◽  
Sat Solver ◽  
Main Ideas ◽  
Planning Problems

The planning problem in Artificial Intelligence was the first application of SAT to reasoning about transition systems and a direct precursor to the use of SAT in a number of other applications, including bounded model-checking in computer-aided verification. This chapter presents the main ideas about encoding goal reachability problems as a SAT problem, including parallel plans and different forms of constraints for speeding up SAT solving, as well as algorithms for solving the AI planning problem with a SAT solver. Finally, more general planning problems that require the use of QBF or other generalizations of SAT are discussed.

scholarly journals Security assurance cases—state of the art of an emerging approach

2021 ◽  
Vol 26 (4) ◽  
Author(s):  
Mazen Mohamad ◽  
Jan-Philipp Steghöfer ◽  
Riccardo Scandariato
Keyword(s):  
State Of The Art ◽  
Tool Support ◽  
Security Assurance ◽  
The Past ◽  
Depth Analysis ◽  
Structured Argumentation ◽  
Security Properties ◽  
Standards And Regulations ◽  
Assurance Cases ◽  
Security Standards

AbstractSecurity Assurance Cases (SAC) are a form of structured argumentation used to reason about the security properties of a system. After the successful adoption of assurance cases for safety, SAC are getting significant traction in recent years, especially in safety-critical industries (e.g., automotive), where there is an increasing pressure to be compliant with several security standards and regulations. Accordingly, research in the field of SAC has flourished in the past decade, with different approaches being investigated. In an effort to systematize this active field of research, we conducted a systematic literature review (SLR) of the existing academic studies on SAC. Our review resulted in an in-depth analysis and comparison of 51 papers. Our results indicate that, while there are numerous papers discussing the importance of SAC and their usage scenarios, the literature is still immature with respect to concrete support for practitioners on how to build and maintain a SAC. More importantly, even though some methodologies are available, their validation and tool support is still lacking.

scholarly journals Even Simple Processes of π-calculus are Hard for Analysis

2018 ◽  
Vol 25 (6) ◽  
pp. 589-606
Author(s):  
Marat M. Abbas ◽  
Vladimir A. Zakharov
Keyword(s):  
Information Security ◽  
Mathematical Models ◽  
Cryptographic Protocols ◽  
Bounded Number ◽  
Distributed Computations ◽  
Security Properties ◽  
Mobile Processes ◽  
Π Calculus ◽  
Np Complete ◽  
Turing Complete

Mathematical models of distributed computations, based on the calculus of mobile processes (π-calculus) are widely used for checking the information security properties of cryptographic protocols. Since π-calculus is Turing-complete, this problem is undecidable in general case. Therefore, the study is carried out only for some special classes of π-calculus processes with restricted computational capabilities, for example, for non-recursive processes, in which all runs have a bounded length, for processes with a bounded number of parallel components, etc. However, even in these cases, the proposed checking procedures are time consuming. We assume that this is due to the very nature of the π -calculus processes. The goal of this paper is to show that even for the weakest model of passive adversary and for relatively simple protocols that use only the basic π-calculus operations, the task of checking the information security properties of these protocols is co-NP-complete.

scholarly journals Dolius: A Distributed Parallel SAT Solving Framework

10.29007/hvqt ◽  
2018 ◽  
Author(s):  
Gilles Audemard ◽  
Benoît Hoessen ◽  
Saïd Jabbour ◽  
Cédric Piette
Keyword(s):  
Shared Memory ◽  
State Of The Art ◽  
Divide And Conquer ◽  
Sat Solving ◽  
Sat Solvers ◽  
Sat Solver

Over the years, parallel SAT solving becomes more and more important. However, most of state-of-the-art parallel SAT solvers are portfolio-based ones. They aim at running several times the same solver with different parameters. In this paper, we propose a tool called Dolius, mainly based on the divide and conquer paradigm. In contrast to most current parallel efficient engines, Dolius does not need shared memory, can be distributed, and scales well when a large number of computing units is available. Furthermore, our tool contains an API allowing to plug any SAT solver in a simple way.

Analysis of secret sharing schemes based on Nielsen transformations

2018 ◽  
Vol 0 (0) ◽  
Author(s):  
Matvei Kotov ◽  
Dmitry Panteleev ◽  
Alexander Ushakov
Keyword(s):  
Computer Algebra ◽  
Secret Sharing ◽  
Computer Algebra System ◽  
Cryptographic Protocols ◽  
Secret Sharing Schemes ◽  
Polynomial Equations ◽  
Polynomial Size ◽  
Security Properties ◽  
System Of Polynomial Equations

Abstract We investigate security properties of two secret-sharing protocols proposed by Fine, Moldenhauer, and Rosenberger in Sections 4 and 5 of [B. Fine, A. Moldenhauer and G. Rosenberger, Cryptographic protocols based on Nielsen transformations, J. Comput. Comm. 4 2016, 63–107] (Protocols I and II resp.). For both protocols, we consider a one missing share challenge. We show that Protocol I can be reduced to a system of polynomial equations and (for most randomly generated instances) solved by the computer algebra system Singular. Protocol II is approached using the technique of Stallings’ graphs. We show that knowledge of {m-1} shares reduces the space of possible values of a secret to a set of polynomial size.

Sign in / Sign up

Export Citation Format

Share Document