EXPLOITING SYMMETRIES FOR TESTING EQUIVALENCE VERIFICATION IN THE SPI CALCULUS

2006 ◽  
Vol 17 (04) ◽  
pp. 815-832
Author(s):  
IVAN CIBRARIO BERTOLOTTI ◽  
LUCA DURANTE ◽  
RICCARDO SISTO ◽  
ADRIANO VALENZANO
Keyword(s):  
Formal Verification ◽  
Cryptographic Protocols ◽  
Transition System ◽  
Experimental Results ◽  
Verification Problem ◽  
Security Properties ◽  
Universal Quantification ◽  
Equivalence Verification ◽  
Testing Equivalence ◽  
Labelled Transition System

Testing equivalence is a quite powerful way of expressing security properties of cryptographic protocols, but its formal verification is a difficult task, because it is based on universal quantification over contexts. A technique based on state exploration to address this verification problem has previously been presented; it relies on an environment-sensitive labelled transition system (ES-LTS) and on symbolic term representation. This paper shows that such a technique can be enhanced by exploiting symmetries found in the ES-LTS structure. Experimental results show that the proposed enhancement can substantially reduce the size of the ES-LTS and that the technique as a whole compares favorably with respect to related work.

scholarly journals Formal verification of neural agents in non-deterministic environments

2021 ◽  
Vol 36 (1) ◽  
Author(s):  
Michael E. Akintunde ◽  
Elena Botoeva ◽  
Panagiotis Kouvaros ◽  
Alessio Lomuscio
Keyword(s):  
Neural Networks ◽  
Parallel Algorithms ◽  
Formal Verification ◽  
Experimental Results ◽  
Use Case ◽  
Feed Forward ◽  
Verification Problem ◽  
Bounded Fragment

AbstractWe introduce a model for agent-environment systems where the agents are implemented via feed-forward ReLU neural networks and the environment is non-deterministic. We study the verification problem of such systems against CTL properties. We show that verifying these systems against reachability properties is undecidable. We introduce a bounded fragment of CTL, show its usefulness in identifying shallow bugs in the system, and prove that the verification problem against specifications in bounded CTL is in coNExpTime and PSpace-hard. We introduce sequential and parallel algorithms for MILP-based verification of agent-environment systems, present an implementation, and report the experimental results obtained against a variant of the VerticalCAS use-case and the frozen lake scenario.

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 Optimization of ProVerif programs for AKE-protocols

2021 ◽  
Vol 33 (5) ◽  
pp. 105-116
Author(s):  
Evgenii Maksimovich Vinarskii ◽  
Alexey Vasilyevich Demakov
Keyword(s):  
Formal Verification ◽  
Formal Methods ◽  
Distinctive Feature ◽  
Formal Specification ◽  
Cryptographic Protocols ◽  
Experimental Results ◽  
Automatic Verification ◽  
Cryptographic Protocol ◽  
Encryption Scheme ◽  
Program Model

Cryptographic protocols are used to establish a secure connection between “honest” agents who communicate strictly in accordance with the rules of the protocol. In order to make sure that the designed cryptographic protocol is cryptographically strong, various software tools are usually used. However, an adequate specification of a cryptographic protocol is usually presented as a set of requirements for the sequences of transmitted messages, including the format of such messages. The fulfillment of all these requirements leads to the fact that the formal specification for a real cryptographic protocol becomes cumbersome, as a result of which it is difficult to analyze it by formal methods. One of such rapidly developing tools for formal verification of cryptographic protocols is ProVerif. A distinctive feature of the ProVerif tool is that with large protocols, it often fails to analyze them, i.e. it can neither prove the security of the protocol nor refute it. In such cases, they resort either to the approximation of the problem, or to equivalent transformations of the program model in the ProVerif language, simplifying the ProVerif model. In this article, we propose a way to simplify the ProVerif specifications for AKE protocols using the El Gamal encryption scheme. Namely, we suggest equivalent transformations that allow us to construct a ProVerif specification that simplifies the analysis of the specification for the ProVerif tool. Experimental results for the Needham-Schroeder and Yahalom cryptoprotocols show that such an approach can be promising for automatic verification of real protocols.

scholarly journals New Statistical Randomness Tests Based on Length of Runs

2015 ◽  
Vol 2015 ◽  
pp. 1-14 ◽  
Author(s):  
Ali Doğanaksoy ◽  
Fatih Sulak ◽  
Muhiddin Uğuz ◽  
Okan Şeker ◽  
Ziya Akcengiz
Keyword(s):  
Statistical Tests ◽  
Random Sequence ◽  
Cryptographic Protocols ◽  
Experimental Results ◽  
Security Evaluation ◽  
Random Numbers ◽  
Statistical Distributions ◽  
Cryptographic Algorithm ◽  
Encryption Algorithms ◽  
Randomness Tests

Random sequences and random numbers constitute a necessary part of cryptography. Many cryptographic protocols depend on random values. Randomness is measured by statistical tests and hence security evaluation of a cryptographic algorithm deeply depends on statistical randomness tests. In this work we focus on statistical distributions of runs of lengths one, two, and three. Using these distributions we state three new statistical randomness tests. New tests useχ2distribution and, therefore, exact values of probabilities are needed. Probabilities associated runs of lengths one, two, and three are stated. Corresponding probabilities are divided into five subintervals of equal probabilities. Accordingly, three new statistical tests are defined and pseudocodes for these new statistical tests are given. New statistical tests are designed to detect the deviations in the number of runs of various lengths from a random sequence. Together with some other statistical tests, we analyse our tests’ results on outputs of well-known encryption algorithms and on binary expansions ofe,π, and2. Experimental results show the performance and sensitivity of our tests.

scholarly journals Study on Formal Modeling and Safety Verification of Train-to-Train Communication

2018 ◽  
Vol 2018 ◽  
pp. 1-9
Author(s):  
Haonan Feng
Keyword(s):  
Transition System ◽  
Research Trend ◽  
Safety Properties ◽  
Safety Verification ◽  
Critical System ◽  
Real Time System ◽  
Vehicle Communication ◽  
Train Control ◽  
Safety Critical System ◽  
Labelled Transition System

VBTC (vehicle-to-vehicle communication based train control) has gradually become an important research trend in the field of rail transit. This has resulted in advantages of decreasing the number of pieces of wayside equipment and improving the efficiency of real-time system communication. Characteristics and mechanism of train-to-train communication, as key implementation technology of safety critical system, are given and discussed. A new method, based on the LTS (labelled transition system) model checking, is proposed for verifying the safety properties in the communication procedure. The LTS method is adapted to model system behaviours; analysis and safety verification are checked by means of LTSA (labelled transition system analyzer) software. The results show that it is an efficient method to verify safety properties, as well as to assist the complex system’s design and development.

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.

Target-oriented Petri Net Synthesis

2020 ◽  
Author(s):  
Eike Best ◽  
Raymond Devillers ◽  
Evgeny Erofeev ◽  
Harro Wimmel
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Transition System ◽  
Efficient Synthesis ◽  
Transition Systems ◽  
Np Complete ◽  
Full Class ◽  
Petri Net Synthesis ◽  
Labelled Transition System ◽  
Additional Constraints

When a Petri net is synthesised from a labelled transition system, it is frequently desirable that certain additional constraints are fulfilled. For example, in circuit design, one is often interested in constructing safe Petri nets. Targeting such subclasses of Petri nets is not necessarily computationally more efficient than targeting the whole class. For example, targeting safe nets is known to be NP-complete while targeting the full class of place/transition nets is polynomial, in the size of the transition system. In this paper, several classes of Petri nets are examined, and their suitability for being targeted through efficient synthesis from labelled transition systems is studied and assessed. The focus is on choice-free Petri nets and some of their subclasses. It is described how they can be synthesised efficiently from persistent transition systems, summarising and streamlining in tutorial style some of the authors’ and their groups’ work over the past few years.

Formal Verification of Secrecy, Coercion Resistance and Verifiability Properties for a Remote Electronic Voting Protocol

2013 ◽  
Vol 7 (2) ◽  
pp. 57-85
Author(s):  
Khaoula Marzouki ◽  
Amira Radhouani ◽  
Narjes Ben Rajeb
Keyword(s):  
Formal Verification ◽  
Electronic Voting ◽  
Automated Verification ◽  
Verification Tool ◽  
Verification Methods ◽  
Pi Calculus ◽  
Security Properties

Electronic voting protocols have many advantages over traditional voting but they are complex and subject to many kinds of attacks. Therefore, the use of formal verification methods is crucial to ensure some security properties. We propose to model a recent protocol of remote electronic voting in the applied Pi-calculus. We focalized on some security properties such as fairness which expresses the impossibility of obtaining partial results, eligibility which requires that only legitimate voters can vote, coercion resistance which ensures that no voter may vote under pressure, and verifiability which supposes that anyone can verify the accuracy of the final result. We proved either manually or using the automated verification tool ProVerif that the protocol satisfies these security properties.

Sign in / Sign up

Export Citation Format

Share Document