Keeping Secrets in Resource Aware Components

We present a powerful and flexible method for automatically checking the secrecy of values inside components. In our framework an attacker may monitor the external communication of a component, interact with it and monitor the components resource usage. We use an automata model of components in which each transition is tagged with resource usage information. We extend these automata to pass values and say that a value is kept secret if the observable behaviour of the automata is the same for all possible instantiations of that value. If a component leaks some, but not all of the information about its secret we use a notion of secrecy degree to quantify the worst-case leakage. We show how this secrecy degree can be automatically calculated, for values from a finite domain, using the μCRL process algebraic verification toolset.     

Linearity and bisimulation

Exploiting linear type structure, we introduce a new theory of weak bisimilarity for the π-calculus in which we abstract away not only τ-actions but also non-τ actions which do not affect well-typed observers. This gives a congruence far larger than the standard bisimilarity while retaining semantic soundness. The framework is smoothly extendible to other settings involving nondeterminism and state. As an application we develop a behavioural theory of secrecy in the π-calculus which ensures secure information flow for a strictly greater set of processes than the type-based approach, while still offering compositional verification techniques.     

On the Symbolic Reduction of Processes with Cryptographic Functions

We study the reachability problem for cryptographic protocols represented as processes relying on perfect cryptographic functions. We introduce a symbolic reduction system that can handle hashing functions, symmetric keys, and public keys. Desirable properties such as secrecy or authenticity are specified by inserting logical assertions in the processes.We show that the symbolic reduction system provides a flexible decision procedure for finite processes and a reference for sound implementations. The symbolic reduction system can be regarded as a variant of syntactic unification which is compatible with certain set-membership constraints. For a significant fragment of our formalism, we argue that a dag implementation of the symbolic reduction system leads to an algorithm running in nptime thus matching the lower bound of the problem.In the case of iterated or finite control processes, we show that the problem is undecidable in general and in ptime for a subclass of iterated processes that do not rely on pairing. Our technique is based on rational transductions of regular languages and it applies to a class of processes containing the ping-pong protocols studied in 1982 by Dolev, Even and Karp.     

Revisiting the notion of function

Functions play a central role in type theory, logic and computation. We describe how the notions of functionalisation (the way in which functions can be constructed) and instantiation (the process of applying a function to an argument) have been developed in the last century. We explain how both processes were implemented in Frege’s Begriffschrift, Russell’s Ramified Type Theory, and the λ-calculus (originally introduced by Church) showing that the λ-calculus misses a crucial aspect of functionalisation. We then pay attention to some special forms of function abstraction that do not exist in the λ-calculus and we show that various logical constructs (e.g., let expressions and definitions and the use of parameters in mathematics), can be seen as forms of the missing part of functionalisation. Our study of the function concept leads to: (a) an extension of the Barendregt cube [4] with all of definitions, Π-reduction and explicit substitutions giving all their advantages in one system; and (b) a natural refinement of the cube with parameters. We show that in the refined Barendregt cube, systems like A , LF, and ML, can be described more naturally and accurately than in the original cube.     

Fractional transformation group induced byQR factorization and linear prediction problem

A new fractional transformation group is found which acts transitively on the space of linear predictors for nonstationary processes by using the QR factorization of nonsingular matrices.     

Static Equivalence is Harder than Knowledge

There are two main ways of defining secrecy of cryptographic protocols. The first version checks if the adversary can learn the value of a secret parameter. In the second version, one checks if the adversary can notice any difference between protocol runs with different values of the secret parameter.We give a new proof that when considering more complex equational theories than partially invertible functions, these two kinds of secrecy are not equally difficult to verify. More precisely, we identify a message language equipped with a convergent rewrite system such that after a completed protocol run, the first problem mentioned above (adversary knowledge) is decidable but the second problem (static equivalence) is not. The proof is by reduction of the ambiguity problem for context-free grammars.     

Structured coalgebras and minimal HD-automata for the -calculus

The coalgebraic framework developed for the classical process algebras, and in particular its advantages concerning minimal realizations, does not fully apply to the π-calculus, due to the constraints on the freshly generated names that appear in the bisimulation.In this paper we propose to model the transition system of the π-calculus as a coalgebra on a category of name permutation algebras and to define its abstract semantics as the final coalgebra of such a category. We show that permutations are sufficient to represent in an explicit way fresh name generation, thus allowing for the definition of minimal realizations.We also link the coalgebraic semantics with a slightly improved version of history dependent (HD) automata, a model developed for verification purposes, where states have local names and transitions are decorated with names and name relations. HD-automata associated with agents with a bounded number of threads in their derivatives are finite and can be actually minimized. We show that the bisimulation relation in the coalgebraic context corresponds to the minimal HD-automaton.     

A fuzzy vector valued KNN-algorithm for automatic outlier detection

The K nearest neighbors approach is a viable technique in time series analysis when dealing with ill-conditioned and possibly chaotic processes. Such problems are frequently encountered in, e.g., finance and production economics. More often than not, the observed processes are distorted by nonnormal disturbances, incomplete measurements, etc. that undermine the identification, estimation and performance of multivariate techniques. If outliers can be duly recognized, many crisp statistical techniques may perform adequately as such. Geno-mathematical programming provides a connection between statistical time series theory and fuzzy regression models that may be utilized e.g., in the detection of outliers. In this paper we propose a fuzzy distance measure for detecting outliers via geno-mathematical parametrization. Fuzzy KNN is connected as a linkable library to the genetic hybrid algorithm (GHA) of the author, in order to facilitate the determination of the LR-type fuzzy number for automatic outlier detection in time series data. We demonstrate that GHA[Fuzzy KNN] provides a platform for automatically detecting outliers in both simulated and real world data.     

Maximum <Emphasis Type="Italic">k</Emphasis>-Splittable <Emphasis Type="Italic">s</Emphasis>,<Emphasis Type="Italic">t</Emphasis>-Flows

Given a graph with a source and a sink node, the NP-hard maximum k-splittable s,t-flow (M k SF) problem is to find a flow of maximum value from s to t with a flow decomposition using at most k paths. The multicommodity variant of this problem is a natural generalization of disjoint paths and unsplittable flow problems. Constructing a k-splittable flow requires two interdepending decisions. One has to decide on k paths (routing) and on the flow values for the paths (packing). We give efficient algorithms for computing exact and approximate solutions by decoupling the two decisions into a first packing step and a second routing step. Usually the routing is considered before the packing. Our main contributions are as follows: (i) We show that for constant k a polynomial number of packing alternatives containing at least one packing used by an optimal M k SF solution can be constructed in polynomial time. If k is part of the input, we obtain a slightly weaker result. In this case we can guarantee that, for any fixed ε>0, the computed set of alternatives contains a packing used by a (1−ε)-approximate solution. The latter result is based on the observation that (1−ε)-approximate flows only require constantly many different flow values. We believe that this observation is of interest in its own right. (ii) Based on (i), we prove that, for constant k, the M k SF problem can be solved in polynomial time on graphs of bounded treewidth. If k is part of the input, this problem is still NP-hard and we present a polynomial time approximation scheme for it.     

Attacking Fair-Exchange Protocols: Parallel Models vs. Trace Models

Most approaches to formal protocol verification rely on an operational model based on traces of atomic actions. Modulo CSP, CCS, state-exploration, Higher Order Logic or strand spaces frills, authentication or secrecy are analyzed by looking at the existence or the absence of traces with a suitable property.We introduced an alternative operational approach based on parallel actions and an explicit representation of time. Our approach consists in specifying protocols within a logic language ( AL _SP), and associating the existence of an attack to the protocol with the existence of a model for the specifications of both the protocol and the attack.In this paper we show that, for a large class of protocols such as authentication and key exchange protocols, modeling in AL _SP is equivalent - as far as authentication and secrecy attacks are considered - to modeling in trace based models.We then consider fair exchange protocols introduced by N. Asokan et al. showing that parallel attacks may lead the trusted third party of the protocol into an inconsistent state. We show that the trace based model does not allow for the representation of this kind of attacks, whereas our approach can represent them.     

A batch arrival queue with a vacation time under single vacation policy

We consider an M^x/G/1 queueing system with a vacation time under single vacation policy, where the server takes exactly one vacation between two successive busy periods. We derive the steady state queue size distribution at different points in times, as well as the steady state distributions of busy period and unfinished work (backlog) of this model.Scope and purposeThis paper addresses issues of model building of manufacturing systems of job-shop type, where the server takes exactly one vacation after the end of each busy period. This vacation can be utilized as a post processing time after clearing the jobs in the system. To be more realistic, we further assume that the arrivals occur in batches of random size instead of single units and it covers many practical situations. For example in manufacturing systems of job-shop type, each job requires to manufacture more than one unit; in digital communication systems, messages which are transmitted could consist of a random number of packets. These manufacturing systems can be modeled by M^x/G/1 queue with a single vacation policy and this extends the results of Levy and Yechiali, Manage Sci 22 (1975) 202, and Doshi, Queueing Syst 1 (1986) 29.     

A spatial logic for concurrency (part I)

We present a logic that can express properties of freshness, secrecy, structure, and behavior of concurrent systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to composition, local name restriction, and a primitive fresh name quantifier. Properties can also be defined by recursion; a central aim of this paper is then the combination of a logical notion of freshness with inductive and coinductive definitions of properties.     

On quorum systems for group resources allocation

We present a problem, called (n, m, k, d)-resource allocation, to model allocation of group resources with bounded capacity. Specifically, the problem concerns the scheduling of k identical resources among n processes which belong to m groups. Each resource can be used by at most d processes of the same group at a time, but no two processes of different groups can use a resource simultaneously. The problem captures two fundamental types of conflicts in mutual exclusion: k-exclusion’s amount constraint on the number of processes that can share a resource, and group mutual exclusion’s type constraint on the class of processes that can share a resource. We then study the problem in the message passing paradigm, and investigate quorum systems for the problem. We begin by establishing some basic and general results for quorum systems for the case of k = 1, based on which quorum systems for the general case can be understood and constructed. We found that the study of quorum systems for (n, m, 1, d)-resource allocation is related to some classical problems in combinatorics and in finite projective geometries. By applying the results there, we are able to obtain some optimal/near-optimal quorum systems.     

同源密码中Montgomery模型的w-坐标研究

椭圆曲线群律计算是传统椭圆曲线密码(ECC)的核心运算,同时也是基于同源的后量子密码计算中的重要组成部分。Montgomery曲线上的Montgomery ladder算法是一种高效(伪)群律计算方法,且经常用于预防侧信道攻击。Farashahi和Hosseini在ACISP 2017提出了Edwards曲线模型上的w-坐标可得到类似Montgomery ladder算法以进行群律计算,Kim等人在ASIACRYPT 2019将其用于优化奇数次同源计算。随后,不同曲线模型上的w-坐标陆续被提出用于优化同源计算。本质上,w-坐标是关于传统椭圆曲线有理点(x,y)-坐标的有理函数。与标准(x,y)-坐标相比,w-坐标不仅可以节约椭圆曲线群律和同源计算的计算量,还可以减少带宽。Hisil和Renes在ACM TOMS 2019提出可利用加2阶点得到更多的w-坐标。受此启发,本文提出利用Montgomery曲线上的2-同源构造出3类新的w-坐标,与x-坐标相同的是,均可应用于Montgomery ladder算法和奇数次同源计算的优化。同时,w-坐标在计算奇数次同源中,同源映射像曲线系数计算公式与像点公式类似,可利用SIMD指令集将两者并行化处理,从而得到相关计算的进一步加速。最后,由于Edwards,Huff,Jacobi等曲线模型在某些条件下可与Montgomery模型建立双有理等价,因此可由Montgomery曲线上新的w-坐标开发出其他曲线模型上更多的w-坐标,它们将有可能支持同源密码实现中更有效的算法。     

The <Emphasis Type="Italic">k</Emphasis>-Homotopic Thinning and a Torus-Like Digital Image in <Emphasis Type="Bold">Z</Emphasis><Superscript><Emphasis Type="Italic">n</Emphasis></Superscript>

In order to discuss digital topological properties of a digital image (X,k), many recent papers have used the digital fundamental group and several digital topological invariants such as the k-linking number, the k-topological number, and so forth. Owing to some difficulties of an establishment of the multiplicative property of the digital fundamental group, a k-homotopic thinning method can be essentially used in calculating the digital fundamental group of a digital product with k-adjacency. More precisely, let be a simple closed k _i -curve with l _i elements in . For some k-adjacency of the digital product which is a torus-like set, proceeding with the k-homotopic thinning of , we obtain its k-homotopic thinning set denoted by DT _k . Writing an algorithm for calculating the digital fundamental group of , we investigate the k-fundamental group of by the use of various properties of a digital covering (Z×Z,p ₁×p ₂,DT _k ), a strong k-deformation retract, and algebraic topological tools. Finally, we find the pseudo-multiplicative property (contrary to the multiplicative property) of the digital fundamental group. This property can be used in classifying digital images from the view points of both digital k-homotopy theory and mathematical morphology.

A Behavioural Pseudometric based on λ–Bisimilarity

In order to describe approximate equivalence among processes, the notions of λ–bisimilarity and behavioural pseudometric have been introduced by Ying and van Breugel respectively. Van Breugel provides a distance function induced by λ–bisimilarity, and conjectures that his behavioural pseudometric coincides with this function. This paper is inspired by this conjecture. We give a negative answer for van Breugel's conjecture first. Moreover, we show that the distance function induced by λ–bisimilarity is a pseudometric on states, and provide a fixed point characterization of this pseudometric.     

Simultaneous Lp-stabilization and internal stabilization of linear systems subject to input saturation — state feedback case

We consider the problem of simultaneous finite gain L_p-stabilization and internal stabilization of linear systems subject to input saturation via linear static state feedback. We show that bounded input finite-gain L_p-stabilization and local asymptotic stabilization can always be achieved simultaneously no matter where the poles of the open-loop system are, and the locations of these poles play a role only when bounded input finite gain L_p-stabilization and global or semi-global stabilization are required simultaneously.     

Geno-mathematical identification of the multi-layer perceptron

In this paper, we will focus on the use of the three-layer backpropagation network in vector-valued time series estimation problems. The neural network provides a framework for noncomplex calculations to solve the estimation problem, yet the search for optimal or even feasible neural networks for stochastic processes is both time consuming and uncertain. The backpropagation algorithm—written in strict ANSI C—has been implemented as a standalone support library for the genetic hybrid algorithm (GHA) running on any sequential or parallel main frame computer. In order to cope with ill-conditioned time series problems, we extended the original backpropagation algorithm to a K nearest neighbors algorithm (K-NARX), where the number K is determined genetically along with a set of key parameters. In the K-NARX algorithm, the terminal solution at instant t can be used as a starting point for the next t, which tends to stabilize the optimization process when dealing with autocorrelated time series vectors. This possibility has proved to be especially useful in difficult time series problems. Following the prevailing research directions, we use a genetic algorithm to determine optimal parameterizations for the network, including the lag structure for the nonlinear vector time series system, the net structure with one or two hidden layers and the corresponding number of nodes, type of activation function (currently the standard logistic sigmoid, a bipolar transformation, the hyperbolic tangent, an exponential function and the sine function), the type of minimization algorithm, the number K of nearest neighbors in the K-NARX procedure, the initial value of the Levenberg–Marquardt damping parameter and the value of the neural learning (stabilization) coefficient α. We have focused on a flexible structure allowing addition of, e.g., new minimization algorithms and activation functions in the future. We demonstrate the power of the genetically trimmed K-NARX algorithm on a representative data set.     

Pattern-based abstraction for verifying secrecy in protocols

We present a method based on abstract interpretation for verifying secrecy properties of cryptographic protocols. Our method allows one to verify secrecy properties in a general model allowing an unbounded number of sessions, an unbounded number of principals, and an unbounded size of messages. As abstract domain we use sets of so-called super terms. Super terms are obtained by allowing an interpreted constructor, which we denote by Sup , where the meaning of a term Sup (t) is the set of terms that contain t as subterm. For these terms, we solve a generalized form of the unification problem and introduce a widening operator. We implemented a prototype and were able to verify well-known protocols such as, for instance, Needham–Schroeder–Lowe (0.03 s), Yahalom (12.67 s), Otway–Rees (0.01 s), and Kao–Chow (0.78 s).     

Micro-hotplates for high-throughput thin film processing and in situ phase transformation characterization

This paper presents the use of micro-hotplates (MHPs) as thermal processing and in situ characterization platforms for phase transformations in thin films. MHPs are fabricated by microsystem technology processes and consist of a SiO₂/Si₃N₄ membrane (app. 1 μm) supported by a bulk Si frame. Several embedded Pt thin films serve as heater and electrical measurement electrodes. It is shown that the MHPs have unique properties for the controlled annealing of thin film materials (up to 1270 K), as the annealing temperature and heating/cooling rates can be precisely controlled by in situ measurements. These rates can be extremely high (up to 10⁴ K/s), due to the low thermal mass of MHPs. The high cooling rates are especially useful for the fabrication of metastable phases (e.g. Fe₇₀Pd₃₀) by quenching. By measuring the resistivity of a thin film under test in situ as a function of the MHP temperature, microstructural changes (e.g. phase transformations) can be detected during heating and cooling cycles. In this paper, examples are presented for the determination of phase transitions in thin films using MHPs: the solid–liquid–gas phase transition (Al), the ferromagnetic–paramagnetic phase transition (Fe–Pt) and martensitic transformations (Ni–Ti–Cu, Fe–Pd). Furthermore, it is demonstrated that crystallization processes from amorphous to crystalline (Ni–Ti–Cu) can be detected with this method. Finally the application of MHPs in thin film combinatorial materials science and high-throughput experimentation is described.