RFID-based authentication plays a crucial role in various fields, such as e-commerce, e-learning, e-business, healthcare, cloud, IoT, etc.At the same time, there is growing interest in using physically unclonable functions (PUFs) in RFID tags to protect against key corruption of pseudo-random functions (PRFs).In this paper, we discuss the privacy properties of PRF+PUF-based RFID authentication protocols in Vaudenay's and the Hermans-Pashalidis-Vercauteren-Preneel (HPVP) models, considering two fundamental aspects: using temporary variables that might compromise privacy and using simulatable PUFs, a more realistic approach to ideal PUFs.Finally, we prove that a variant of a recently proposed RFID-based authentication protocol achieves strong privacy in the HPVP model.• Extending the scheme to ensure mutual authentication

RFID technology has proven very useful in many healthcare applications, starting with medical asset tracking, continuing with staff tracking, and reaching medical event and procedure tracking. Security and privacy properties play a fundamental role in this range of applications. The protocols proposed so far highlights many techniques for analyzing these properties, making it difficult to compare the protocols with each other most of the time. In the case of lightweight protocols, the comparisons are even more challenging to achieve because these resort to idealizations that usually have no practical support, such as protocols based on physically unclonable functions (PUFs), or because no security and privacy model is known so far. This paper draws attention to the HPVP model as a possibility for uniformly studying healthcare RFID protocols’ security and privacy properties. We highlight two general patterns that, once encountered in RFID protocols, show that they do not satisfy privacy or mutual authentication requirements. We then illustrate these templates through several proposed RFID protocols for use in healthcare. Then, we propose a Classification of healthcare services based on an extended hierarchy of HPVP privacy classes, and we highlight RFID protocols that reach the respective levels of privacy.

Healthcare offers a rich palette of potential applications of RFID technology. Healthcare provides a rich palette of possible applications of RFID technology. Besides traditional uses such as tracking medical equipment and devices or access control, healthcare can benefit even more significantly from RFID technology. However, using the RFID technology in healthcare raises various problems of scalability, timely identification of tags, security, privacy, and efficient implementation in practice. That is because such systems contain many tags, operate with private personal data, and must respond promptly in concrete, practical situations to avoid malfunctions (errors in the decision process, traffic congestion, and so on). This paper discusses the fundamental requirements of RFID systems raised by healthcare and the limitations of existing schemes. Then, we propose a new RFID scheme that achieves mutual authentication, strong privacy, and constant-time identification in the HPVP model. The scheme employs a secure symmetric-key encryption scheme, making it very efficient in implementation and physically unclonable functions (PUFs) to protect the secret key against adversaries with corruption capabilities.

The concept of Generalized Inverse Decoding (GID) is introduced, as an algebraic framework for the syndrome decoding (SD) and low-weight codeword (LWC) problems. The framework has ground on two characterizations by generalized inverses, one for the null space of a matrix and the other for the solution space of a system of linear equations over a finite field. Generic GID solvers are proposed for the SD and LWC problems. It is shown that information set decoding (ISD) algorithms, such as Prange, Lee-Brickell, Leon, and Stern’s algorithms, are particular cases of GID solvers. All of them search generalized inverses or elements of the null space under various specific strategies. However, as the paper shows in the case of Prange’s algorithm, they do not search through the entire space, while our solvers do even when they use just one Gaussian elimination. Apart from these, our GID framework clearly shows how each ISD algorithm except for Prange’s can be used as an SD or LWC solver. Experimental results show a very good behavior of the GID solvers. The domain of easy weights can be reached by a very few iterations and even enlarged.

RFID technology is increasingly used in various areas of society, where privacy plays a critical role. Due to this aspect, a sustained effort has been devoted in recent years to develop privacy models for RFID systems. Two widely accepted such models are Vaudenay’s model and the HPVP model. An incursion into the broad diversity of the RFID schemes developed so far shows that many of them do not assure privacy in any of the two models. That is either due to design errors or because their authors did not run any privacy analysis or have used weaker ad hoc privacy models. This article presents five design scenarios underlying constructions of RFID schemes that cannot provide certain levels of privacy in any of the two models. Each scenario is richly exemplified by RFID schemes proposed in the literature, and it is concluded by a lesson to guide us to a better design of such schemes.

Abstract Multilevel and compartmented access structures are two important classes of access structures where participants are grouped into levels/compartments with different degrees of trust and privileges. The construction of secret sharing schemes for such access structures has been the attention of researchers for a long time. Two main approaches have been taken so far, one of them is based on polynomial interpolation and the other one is based on the Chinese Remainder Theorem (CRT). In this article the first asymptotically ideal CRT‐based secret sharing schemes for (disjunctive, conjunctive) multilevel and compartmented access structures are proposed. Our approach is compositional and it is based on a variant of the Asmuth‐Bloom secret sharing scheme where some participants may have public shares. Based on this, the proposed secret sharing schemes for multilevel and compartmented access structures are asymptotically ideal if and only if they are based on 1‐compact sequences of co‐primes. Possible applications for secret image and multi‐secret sharing are pointed‐out.

RFID tag corruption is a powerful attack on RFID systems, especially when it reveals the tag's temporary state. Under such an attack, no RFID scheme can achieve both security and privacy if the tags are not endowed with some hardware primitives, such as physically unclonable functions (PUFs), to prevent adversarial access to secret information. However, the use of such primitives does not constitute a guarantee for security and privacy because they do not substitute a good RFID system design. In this paper a general technique is proposed, to translate any (PUF-based) RFID scheme that is secure and private under corruption without temporary state disclosure into a PUF-based RFID scheme that is secure and private under corruption with temporary state disclosure. Our technique is optimal with respect to the tag overhead induced by PUFs. The technique is richly exemplified on both RFID and PUF-based RFID schemes. As a notable result, the first PUF-based RFID scheme is obtained, that is secure and forward private, but not destructive private, under corruption with temporary state disclosure. By using our technique, some flawed PUF-based RFID schemes that have been proposed so far in the literature can be fixed.

We show that a history-based variant of alternating bisimulation with imperfect information allows it to be related to a variant of Alternating-time Temporal Logic (ATL) with imperfect information by a full Hennessy-Milner theorem. The variant of ATL we consider has a common knowledge semantics, which requires that the uniform strategy available for a coalition to accomplish some goal must be common knowledge inside the coalition, while other semantic variants of ATL with imperfect information do not accomodate a Hennessy-Milner theorem. We also show that the existence of a history-based alternating bisimulation between two finite Concurrent Game Structures with imperfect information (iCGS) is undecidable.

There is a major interest in designing RFID schemes based on symmetric-key cryptography and ensuring efficient tag identification. These requirements taken together often lead to a decrease in the degree of privacy provided by the scheme. This issue, as we know, has been treated in an ad-hoc manner so far. In this paper, we introduce the class of stateful RFID schemes with constant tag identifiers, that ensure tag identification in no more than logarithmic time. In order to study their privacy, we propose an appropriate general model obtained by constraining Vaudenay's model. We then propose two symmetric-key cryptography based RFID schemes in this class that achieve weak and destructive privacy, respectively, in addition to mutual authentication. We also discuss on the degree of privacy provided by other schemes proposed in the literature, that fall in this class.

Group anonymity, as an instance of information hiding, means that an agent is not identifiable within a group of agents with respect to an observer.In this paper we define group anonymity in security protocols by taking into account two types of observers: honest agents, as local observers of the protocol execution, and intruders (active or passive), as global observers of the protocol execution.It is shown that an action may be group anonymous in a protocol under a passive intruder but not in the same protocol under an active intruder, and vice versa.In case of basic-term actions, group anonymity in a protocol under an active intruder implies group anonymity in the same protocol under a passive intruder.A broad spectrum of relationships between group anonymity for various types of actions is developed, as well as relationships between group anonymity, minimal anonymity, and role interchangeability.Finally, the decidability and complexity status of the decision problems induced by these concepts is completely discussed.Thus, it is shown that group anonymity and role interchangeability are undecidable in unrestricted protocols.Group anonymity is complete for NEXPTIME when it is restricted to basic-term actions and bounded security protocols, and it is complete for NP when it is restricted to basic-term actions and 1-session bounded security protocols.

The reversible released form (RRF) of Petri nets is introduced as an extension of the released form. This new form introduces undo transitions in order to reverse the effect of some of the transitions of the original Petri net. It is shown that the RRF preserves the soundness property of workflow (WF) nets: a WF net is sound if and only if its RRF is sound too. Then, various properties of the RRF of circuit-based Petri nets are investigated, and complexity results of the soundness property of circuit-based WF nets are derived.

This paper focuses on the complexity of the (weak) soundness problem of acyclic workflow (WF) nets, and two main results are established: (1) soundness of 1-bounded acyclic WF nets is co-NP-complete and (2) weak soundness of 3-bounded acyclic asymmetric-choice WF nets is co-NP-complete.

In this paper, a robust and as simple as possible concept of a Petri net (PN) computer is proposed. It has a similar structure and behavior to weak sound priority workflow nets. It is shown that all recursive functions are PN computable and, vice-versa, PN computable functions are recursive. This shows that the PN computers we have proposed have exactly the power of Turing machines. Complexity classes of PN computable functions are defined, and the relationship between them and similar complexity classes defined by counter machines is investigated. Finally, the close relationship between PN computers and weak sound (priority) workflow nets is investigated.

Complex workflows arising from practical applications usually combine time, resource, and task priority constraints. The goal of this paper is to formulate a suitable WF net model with all these three types of constraints, and to investigate the soundness property of the resulting model. Thus, the concept of a multilevel resource constrained workflow net (mlRCWF net) as being a place composition of resource constrained workflow (RCWF) nets is introduced, and its soundness property is investigated. This model is then enriched with time and task priority constraints. It is shown that the soundness property of timed priority mlRCWF nets can be reduced in linear time to the soundness property of (untimed) priority RCWF nets. A resource relocation policy is a policy by which resources already allocated to some task are then relocated to urgent tasks, the current task being thus delayed. When the current tasks support an indefinite delay, the soundness of timed priority mlRCWF nets with resource relocation can be reduced in quadratic time to the soundness property of (untimed) priority RCWF nets.

This paper proposes priority (resource-constrained) workflow nets (WF nets) as Petri-net-based models of (resource-constrained) workflows with priorities between tasks. It is shown that the soundness problem (behavioral correctness criterion) is undecidable for priority (resource-constrained) WF nets. If supplementary conditions are imposed, soundness for priority (resource-constrained) WF nets can be reduced to soundness for their underlying (resource-constrained) WF nets. Two such conditions are proposed in this paper. One of them generalizes the well-known EQUAL-conflict condition for priority Petri nets, and the other one generalizes the conflict-freeness condition for Petri nets. Using the Petri net path logic, it is shown that both conditions are decidable. Finally, a generalization of the priority relation is proposed, which allows for a broader spectrum of workflow modeling. The results aforementioned also hold in this case.

This paper focuses on the decidability status of various forms of behavioral correctness criteria for resource-constrained workflow (RCWF) nets (Petri net models of RCWF systems). These behavioral correctness criteria, usually called soundness criteria, are natural extensions of similar correctness criteria for workflow nets (Petri net models of workflow systems). While all forms of soundness are known to be decidable for workflow nets, only soundness for RCWF nets with just one resource type is known to be decidable. In this paper, we show that if we limit the number of cases, then soundness for RCWF nets with arbitrarily many resource types is decidable. Moreover, we show that some “intermediate” forms of soundness, as well as a restrictive form of structural soundness for RCWF nets, are decidable too. The proof technique is based on instantiation nets as a general tool for dealing with arbitrarily many cases and arbitrarily large resources in workflow nets and RCWF nets. It is also shown why this technique cannot be extended to the most general form of soundness.

The main purpose of workflow management systems is to support the definition, execution, and control of workflow processes. With or without time constraints, workflow management systems should satisfy certain correctness properties. The most important and widely used is the soundness property . In this paper, we focus on the soundness property for two classes of Petri-net-based workflow management systems with time constraints,S- andA-timedworkflownets(WNs), and we show that this property is undecidable for them. The proof technique, based on the undecidability of the halting problem for deterministic counter machines, shows first that the reachability, coverability, boundedness, and quasi-liveness problems are undecidable for these two classes of timed WNs, and then, as a consequence, the undecidability of the soundness problem is derived.

The secrecy problem for security protocols is the problem to decide whether or not a given security protocol has leaky runs. In this paper, the (initial) secrecy problem for bounded protocols with freshness check is shown to be NEXPTIME-complete. Relating the formalism in this paper to the multiset rewriting (MSR) formalism we obtain that the initial secrecy problem for protocols in restricted form, with bounded length messages, bounded existentials, with or without disequality tests, and an intruder with no existentials, is NEXPTIME-complete. If existentials for the intruder are allowed but disequality tests are not allowed, the initial secrecy problem still is NEXPTIME-complete. However, if both existentials for the intruder and disequality tests are allowed and the protocols are not well-founded (and, therefore, not in restricted form), then the problem is undecidable. These results also correct some wrong statements in Durgin et al., JCS 12 (2004), 247–311.

We consider here some special forms of ambiguity for pure context-free grammars, namely pattern avoiding ambiguity, pattern preserving ambiguity, pattern ambiguity, and grammar avoiding ambiguity. The first two properties are undecidable for arbitrary pure context-free grammars, and in a particular but general enough case we can effectively decide whether or not a pure context-free grammar is pattern preserving ambiguous.

A Jumping Petri Net ([18], [12]), JPTN for short, is defined as a classical net which can spontaneously jump from a marking to another one. In [18] it has been shown that the reachability problem for JPTN's is undecidable, but it is decidable for finite JPTN's (FJPTN). In this paper we establish some specific properties and investigate the computational power of such nets, via the interleaving semantics. Thus, we show that the non-labelled JPTN's have the same computational power as the labelled or λ-labelled JPTN's. When final markings are considered, the power of JPTN's equals the power of Turing machines. The family of regular languages and the family of languages generated by JPTN's with finite state space are shown to be equal. Languages generated by FJPTN's can be represented in terms of regular languages and substitutions with classical Petri net languages. This characterization result leads to many important consequences, e.g. the recursiveness (context-sensitiveness, resp.) of languages generated by arbitrarily labelled (labelled, resp.) FJPTN's. A pumping lemma for nonterminal jumping net languages is also established. Finally, some comparisons between families of languages are given, and a connection between FJPTN's and a subclass of inhibitor nets is presented.