Deep auto-encoders (AEs) are widely employed deep learning methods in the field of anomaly detection across diverse domains (e.g., cybersecurity analysts managing large volumes of alerts, or medical practitioners monitoring irregular patient signals). In such contexts, practitioners often face challenges of scale and limited processing resources. To cope, strategies such as false positive reduction, human-in-the-loop review, and alert prioritization are commonly adopted. This paper explores the integration of uncertainty quantification (UQ) methods into alert prioritization for anomaly detection using ensembles of AEs. UQ models highlight doubtful classification decisions, enabling analysts to address the most certain alerts first, since higher certainty typically correlates with greater accuracy. Our study reveals a nuanced issue where applying UQ to ensembles of AEs can produce skewed distributions of large reconstruction errors (errors exceeding a pre-defined threshold), which may falsely suggest high uncertainty when standard deviation is used as the metric. Conventionally, a high standard deviation indicates high uncertainty. However, contrary to intuition, large reconstruction errors often reflect AE is strongly confident that an input is anomalous—not uncertainty about it. Moreover, ensembles of AEs generate reconstruction errors with varying ranges, complicating interpretation. To address this, we propose an extension that calibrates the standard deviation distribution of uncertainties, mitigating erroneous prioritization. Evaluation on 10 benchmark datasets demonstrates that our calibration approach improves the effectiveness of UQ methods in prioritizing alerts, while maintaining favorable trade-offs across other key performance metrics.

Secure authentication remains a critical challenge in healthcare IoT (H-IoT) systems, where constrained devices must ensure data integrity, privacy, and resilience despite limited resources. This paper proposes EHKEA, a lightweight mutual authentication and key establishment protocol designed specifically for H-IoT environments. EHKEA relies solely on symmetric cryptographic primitives and ephemeral randomness to provide mutual authentication, forward secrecy and resistance to common attacks such as replay, impersonation, and man-in-the-middle intrusions. We formally verify EHKEA in the Tamarin prover under the Dolev-Yao adversary model, proving key security properties including injective agreement and session key secrecy. A detailed informal analysis further confirms its robustness against desynchronization, insider threats, and key compromise impersonation. Comparative analysis with recent H-IoT protocols demonstrates that EHKEA achieves superior efficiency while offering stronger security guarantees, making it well-suited for deployment in real-time healthcare monitoring applications.

International audience

Abstract This paper presents SGAC (Solution de Gestion Automatisée du Consentement / automated consent management solution), a new healthcare access control model and its support tool, which manages patient wishes regarding access to their electronic health records (EHR). This paper also presents the verification of access control policies for SGAC using two first-order-logic model checkers based on distinct technologies, Alloy and ProB. The development of SGAC has been achieved within the scope of a project with the University of Sherbrooke Hospital (CHUS), and thus has been adapted to take into account regional laws and regulations applicable in Québec and Canada, as they set bounds to patient wishes: for safety reasons, under strictly defined contexts, patient consent can be overriden to protect his/her life (break-the-glass rules). Since patient wishes and those regulations can be in conflict, SGAC provides a mechanism to address this problem based on priority, specificity and modality. In order to protect patient privacy while ensuring effective caregiving in safety-critical situations, we check four types of properties: accessibility, availability, contextuality and rule effectivity. We conducted performance tests comparison: implementation of SGAC versus an implementation of another access control model, XACML, and property verification with Alloy versus ProB. The performance results show that SGAC performs better than XACML and that ProB outperforms Alloy by two order of magnitude thanks to its programmable approach to constraint solving.

Nowadays, the usefulness of the formal verification and validation of system specifications is well established, at least for critical systems. However, one of the main obstacles to their adoption lies in obtaining the formal specification of the system, and, in the case of refinement-based formal methods such as B System or Event-B, in obtaining the most abstract specification that heads the development of the system. The SysML/KAOS requirements engineering method is proposed to overcome this difficulty. It includes a goal modeling language to model requirements from stakeholders needs. Translation rules from a goal model to a B System specification have already been defined. They allow to obtain a skeleton of the system specification. To complete it, a language has been defined to express the domain model associated to the goal model. Its translation gives the structural part of the B System specification. However, it very often appears that new elements must be added in the B System specification obtained from SysML/KAOS models, discovered for instance when specifying the body of events and/or by using formal validation and/or verification tools. We have therefore defined a set of rules allowing the back propagation, within domain models, of every newly added element. This paper describes these rules and how they are specified in Event-B. Their consistency is proved using the Rodin tool. We show that they are structure preserving: two related elements within the B System specification remain related within the domain model. This is done by proving various isomorphisms between the B System specification and the domain models.

Algebraic State-Transition Diagrams (ASTDs) are extensions of common automata and statecharts that can be combined with process algebra operators like sequence, choice, guard and quantified synchronization. They were previously introduced for the graphical representation, specification and proof of information systems. In an attempt to use ASTDs to specify cyber-attack detection, we have identified a number of missing features in ASTDs. This paper extends the ASTD notation with state variables (attributes), actions on transitions, and a new operator called flow which corresponds to AND states in statecharts and is a compromise between interleaving and synchronization in process algebras. We provide a formal structured operational semantics of these extensions and illustrate its implementation in an OCaml-based interpreter called iASTD and the model checker ProB. Extended ASTDs are illustrated in a case study in cyber attack detection.

Abstract In this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic State-Transition Diagrams (ASTD) notation. Then, we use the Well Structured Transition Systems (WSTS) theory to solve the coverability problem for an unbounded ASTD state space. Moreover, we define a new framework to prove the effective pred-basis condition of WSTSs, i.e. the computability of a base of predecessors for every states.

This paper presents SGAC(Solution de Gestion Automatisée du Consentement, automatised consent management solution), a new healthcare access control model and its support tool, that manages patient wishes regarding access to their electronic health record (EHR). The development of this model has been achieved in the scope of a project with the Sherbrooke University Hospital, and thus has been adapted to take into account laws and regulations applicable in Québec and Canada, as they set bounds to patient wishes: under strictly defined contexts, patient consent can be overridden to protect his/her life. Moreover, since patient wishes and laws can be in conflict, SGAC provides a mechanism to address this problem. Besides, laws do not cover all cases where consent should be overridden to ensure patient safety. To this end, we define a formal model of SGAC which allows for property verification, making it possible to detect these cases. A performance comparison with XACML (WSO2/Balana) is presented and demonstrates the superior performances of SGAC.

Abstract This paper proposes a formal approach for generating necessary and sufficient proof obligations to demonstrate a set of dynamic properties using the B method. In particular, we consider reachability, non-interference and absence properties. Also, we show that these properties permit a wide range of property patterns introduced by Dwyer to be expressed. An overview of a tool supporting these approaches is also provided.

Abstract This paper introduces three refinement patterns for algebraic state-transition diagrams ( astds ): state refinement, transition refinement and loop-transition refinement. These refinement patterns are derived from practice in using astds for specifying information systems and security policies in two industrial research projects. Two refinement relations used in these patterns are formally defined. For each pattern, proof obligations are proposed to ensure preservation of behaviour through refinement. The proposed refinement relations essentially consist in preserving scenarios by replacing abstract events with concrete events, or by introducing new events. Deadlocks cannot be introduced; divergence over new events is allowed in one of the refinement relation. We prove congruence-like properties for these three patterns, in order to show that they can be applied to a subpart of a specification while preserving global properties. These three refinement patterns are illustrated with a simple case study of a complaint management system.

Temporal properties are very common in various classes of systems, including information systems and security policies. This paper investigates two verification methods, proof and model checking, for one of the most frequent patterns of temporal property, the absence pattern. We explore two model-based specification techniques, B and Alloy, because of their adequacy for easily specifying systems with complex data structures, like information systems. We propose a first-order, assertion-based, sound and complete strategy to verify the absence pattern. This enables the proof of the absence pattern using conventional first-order provers. We show that the use of assertions significantly increases the size of the models that can be checked, when compared to traditional LTL model checking techniques. The approach is illustrated throughout a case study.

This paper proposes an approach to prove interference freedom for a reach ability property of the form AG (ψ =>; EF Φ) in a B specification. Such properties frequently occur in security policies and information systems. Reach ability is proved by constructing using stepwise algorithmic refinement an abstract program that refines AG (ψ =>; EF Φ). We propose proof obligations to show non-interference, ie, to prove that other operations can be executed in interleaving with this program while preserving the reach ability property, to cater for the multi-user aspect of information systems. Proof obligations are discharged using conventional B provers (eg, Atelier B). Since refinement preserves these reach ability properties and non-interference, proofs can be conducted on abstract machines rather than implementation code.

EB3is a trace-based formal language created for the specification of information systems (IS). Attributes, linked to entities and associations of an IS, are computed in EB3by recursive functions on the valid traces of the system. We aim at synthesizing relational database transactions that correspond to EB3attribute definitions. Each EB3action is translated into a transaction. EB3attribute definitions are analysed to determine the key values affected by each action. Some key values are retrieved from SELECT statements that correspond to first-order predicates in EB3attribute definitions. To avoid problems with the sequencing of SQL statements in the transactions, temporary variables and/or tables are introduced for these key values. Generation of DELETE statements is straightforward, but distinguishing updates from insertions of tuples requires more analysis

We propose a formalization of the COSMIC Full Function Point (COSMIC-FFP) measure for the Real-time Object Oriented Modeling (ROOM) language. COSMIC-FFP is a measure of the functional size of software. It has been proposed by the COSMIC group as an adaptation of the function point measure for real-time systems. The definition of COSMIC-FFP is general and can be applied to any specification language. The benefits of our formalization are twofold. First it eliminates measurement variance, because the COSMIC informal definition is subject to interpretation by COSMIC-FFP raters, which may lead to different counts for the same specification, depending on the interpretation made by each rater. Second it allows the automation of COSMIC-FFP measurement for ROOM specifications, which reduces measurement costs. Finally, the formal definition of COSMIC-FFP can provide a clear and unambiguous characterization of COSMIC-FFP concepts which is helpful for measuring COSMIC-FFP for other object-oriented notations like UML.

We give a formal relation-based definition of scenarios and we show how different scenarios can be integrated to obtain a more global view of user-system interactions. We restrict ourselves to the sequential case, meaning that we suppose that there is only one user (thus, the scenarios we wish to integrate cannot occur concurrently). Our view of scenarios is state-based, rather than event-based, like most of the other approaches, and can be grafted to the well-established specification language Z. Also, the end product of scenario integration, the specification of the functional aspects of the system, is given as a relation; this specification can be refined using independently developed methods. Our formal description is coupled with a diagram-based, transition-system like, presentation of scenarios, which is better suited to communication between clients and specifiers.

Given a software library whose entries are represented by formal specifications, we distinguish between two retrieval procedures: exact retrieval, whereby, given a query K, we identify all the library components that are correct with respect to K; approximate retrieval, which is invoked when exact retrieval fails, and identifies the library components that minimize adaptation effort. To this effect, we define four measures of functional distance between specifications, and discuss algorithms that minimize these measures over a set of components; then we discuss whether these measures can be used to predict adaptation effort.