Biblio

Conversational Intelligent Tutoring Systems (CITS) in learning environments are capable of providing personalized instruction to students in different domains, to improve the learning process. This interaction between the Intelligent Tutoring System (ITS) and the user is carried out through dialogues in natural language. In this study, we use an open source framework called Rasa to adapt the original button-based user interface of an algebraic/arithmetic word problem-solving ITS to one based primarily on the use of natural language. We conducted an empirical study showing that once properly trained, our conversational agent was able to recognize the intent related to the content of the student’s message with an average accuracy above 0.95.

The fifth-generation (5G) standard is the last telecommunication technology, widely considered to have the most important characteristics in the future network industry. The 5G system infrastructure contains three principle interfaces, each one follows a set of protocols defined by the 3rd Generation Partnership Project group (3GPP). For the next generation network, 3GPP specified two authentication methods systematized in two protocols namely 5G Authentication and Key Agreement (5G-AKA) and Extensible Authentication Protocol (EAP). Such protocols are provided to ensure the authentication between system entities. These two protocols are critical systems, thus their reliability and correctness must be guaranteed. In this paper, we aim to formally re-examine 5G-AKA protocol using micro Common Representation Language 2 (mCRL2) language to verify such a security protocol. The mCRL2 language and its associated toolset are formal tools used for modeling, validation, and verification of concurrent systems and protocols. In this context, the authentication protocol 5G-AKA model is built using Algebra of Communication Processes (ACP), its properties are specified using Modal mu-Calculus and the properties analysis exploits Model-Checker provided with mCRL2. Indeed, we propose a new mCRL2 model of 3GPP specification considering 5G-AKA protocol and we specify some properties that describe necessary requirements to evaluate the correctness of the protocol where the parsed properties of Deadlock Freedom, Reachability, Liveness and Safety are positively assessed.

This article describes a new way to generate and distribute secret encryption keys, in which the processes of generating a public key and formicating a secret encryption key are performed in algebra with a parameter, the secrecy of which provides increased durability of the key.

The world is fundamentally compositional, so it is natural to think of visual recognition as the recognition of basic visually primitives that are composed according to well-defined rules. This strategy allows us to recognize unseen complex concepts from simple visual primitives. However, the current trend in visual recognition follows a data greedy approach where huge amounts of data are required to learn models for any desired visual concept. In this paper, we build on the compositionality principle and develop an "algebra" to compose classifiers for complex visual concepts. To this end, we learn neural network modules to perform boolean algebra operations on simple visual classifiers. Since these modules form a complete functional set, a classifier for any complex visual concept defined as a boolean expression of primitives can be obtained by recursively applying the learned modules, even if we do not have a single training sample. As our experiments show, using such a framework, we can compose classifiers for complex visual concepts outperforming standard baselines on two well-known visual recognition benchmarks. Finally, we present a qualitative analysis of our method and its properties.

This paper presents an algebraic approach for formalizing and detecting vulnerabilities in binary code. It uses behaviour algebra equations for creating patterns of vulnerabilities and algebraic matching methods for vulnerability detection. Algebraic matching is based on symbolic modelling. This paper considers a known vulnerability, buffer overflow, as an example to demonstrate an algebraic approach for pattern creation.

This study introduces formal methods for detection of vulnerabilities in binary code. It considers the transformation of binary code into behavior algebra expressions and formalization of vulnerabilities. The detection method has two levels: behavior matching and symbolic execution with vulnerability pattern matching. This enables more efficient performance.

The evaluation of fault attacks on security-critical hardware implementations of cryptographic primitives is an important concern. In such regards, we have created a framework for automated construction of fault attacks on hardware realization of ciphers. The framework can be used to quickly evaluate any cipher implementations, including any optimisations. It takes the circuit description of the cipher and the fault model as input. The output of the framework is a set of algebraic equations, such as conjunctive normal form (CNF) clauses, which is then fed to a SAT solver. We consider both attacking an actual implementation of a cipher on an field-programmable gate array (FPGA) platform using a fault injector and the evaluation of an early design of the cipher using idealized fault models. We report the successful application of our hardware-oriented framework to a collection of ciphers, including the advanced encryption standard (AES), and the lightweight block ciphers LED and PRESENT. The corresponding results and a discussion of the impact to different fault models on our framework are shown. Moreover, we report significant improvements compared to similar frameworks, such as speedups or more advanced features. Our framework is the first algebraic fault attack (AFA) tool to evaluate the state-of-the art cipher LED-64, PRESENT and full-scale AES using only hardware-oriented structural cipher descriptions.

In this paper, We propose DNA sticker model based algorithm, a computability model, which is a simulation of the parallel computations using the Molecular computing as in Adelman's DNA computing experiment, it demonstrates how to use a sticker-based model to design a simple DNA-based algorithm for attacking a linear and a non-linear feedback shift register (FSR) based stream cipher. The algorithm first construct the TEST TUBE contains all overall solution space of memory complexes for the cipher and initials of registers via the sticker-based model. Then, with biological operations, separate and combine, we remove those which encode illegal plain and key stream from the TEST TUBE of memory complexes, the decision based on verifying a key stream bit this bit represented by output of LFSRs equation. The model anticipates two basic groups of single stranded DNA molecules in its representation one of a genetic bases and second of a bit string, It invests parallel search into the space of solutions through the possibilities of DNA computing and makes use of the method of cryptanalysis of algebraic code as a decision technique to accept the solution or not, and their operations are repeated until one solution or limited group of solutions is reached. The main advantages of the suggested algorithm are limited number of cipher characters, and finding one exact solution The present work concentrates on showing the applicability of DNA computing concepts as a powerful tool in breaking cryptographic systems.

Data provenance tools capture the steps used to produce analyses. However, scientists must choose among workflow provenance systems, which allow arbitrary code but only track provenance at the granularity of files; provenance APIs, which provide tuple-level provenance, but incur overhead in all computations; and database provenance tools, which track tuple-level provenance through relational operators and support optimization, but support a limited subset of data science tasks. None of these solutions are well suited for tracing errors introduced during common ETL, record alignment, and matching tasks - for data types such as strings, images, etc. Scientists need new capabilities to identify the sources of errors, find why different code versions produce different results, and identify which parameter values affect output. We propose PROVision, a provenance-driven troubleshooting tool that supports ETL and matching computations and traces extraction of content within data objects. PROVision extends database-style provenance techniques to capture equivalences, support optimizations, and enable selective evaluation. We formalize our extensions, implement them in the PROVision system, and validate their effectiveness and scalability for common ETL and matching tasks.

We present the IT solution for remote modeling of cryptographic protocols and other cryptographic primitives and a number of education-oriented capabilities based on them. These capabilities are provided at the Department of Mathematical Modeling using the MPEI algebraic processor, and allow remote participants to create automata models of cryptographic protocols, use and manage them in the modeling process. Particular attention is paid to the IT solution for modeling of the private communication and key distribution using the processor combined with the Kerberos protocol. This allows simulation and studying of key distribution protocols functionality on remote computers via the Internet. The importance of studying cryptographic primitives for future IT specialists is emphasized.

There are several works on the formalization of security protocols and proofs of their security in Isabelle/HOL; there have also been tools for automatically generating such proofs. This is attractive since a proof in Isabelle gives a higher assurance of the correctness than a pen-and-paper proof or the positive output of a verification tool. However several of these works have used a typed model, where the intruder is restricted to "well-typed" attacks. There also have been several works that show that this is actually not a restriction for a large class of protocols, but all these results so far are again pen-and-paper proofs. In this work we present a formalization of such a typing result in Isabelle/HOL. We formalize a constraint-based approach that is used in the proof argument of such typing results, and prove its soundness, completeness and termination. We then formalize and prove the typing result itself in Isabelle. Finally, to illustrate the real-world feasibility, we prove that the standard Transport Layer Security (TLS) handshake satisfies the main condition of the typing result.

While computer programs and logical theories begin by declaring the concepts of interest, be it as data types or as predicates, network computation does not allow such global declarations, and requires concept mining and concept analysis to extract shared semantics for different network nodes. Powerful semantic analysis systems have been the drivers of nearly all paradigm shifts on the web. In categorical terms, most of them can be described as bicompletions of enriched matrices, generalizing the Dedekind-MacNeille-style completions from posets to suitably enriched categories. Yet it has been well known for more than 40 years that ordinary categories themselves in general do not permit such completions. Armed with this new semantical view of Dedekind-MacNeille completions, and of matrix bicompletions, we take another look at this ancient mystery. It turns out that simple categorical versions of the limit superior and limit inferior operations characterize a general notion of Dedekind-MacNeille completion, that seems to be appropriate for ordinary categories, and boils down to the more familiar enriched versions when the limits inferior and superior coincide. This explains away the apparent gap among the completions of ordinary categories, and broadens the path towards categorical concept mining and analysis, opened in previous work.