Recently, knowledge graphs have been utilised in recommendation systems to improve accuracy by integrating item-side auxiliary information. However, structural user-side knowledge is difficult to construct and integrate due to inherent scarcity and improper granularity. This paper introduces a graph contrastive learning with Semantic transitions-Enhanced DIffusion architecture based on Large Language Models (LLMs) for user-side knowledge-aware Recommendation (SEDIRec). Specifically, our SEDIRec first leverages LLMs to infer user interests from historical behaviors, integrating this user-side information with item-side and collaborative data to construct main views. Then, two contrastive views are generated using diffusion models with semantic transitions: one at the user-side level and the other at the item-side level. For both contrastive views, we integrate user-side or item-side information with collaborative data to generate a user-item graph. Subsequently, each user-item graph is transformed into collaborative data spaces via diffusion models for generating contrastive views. This procedure not only enhances the alignment between user/item-side information and the semantic spaces of collaborative data but also effectively eliminates noise. Extensive experiments on three datasets reveal the superiority of SEDIRec, especially for users with sparse interactions.

In distributed networks, calculating the maximum element is a fundamental task in data analysis, known as the distributed maximum consensus problem. However, the sensitive nature of the data involved makes privacy protection essential. Despite its importance, privacy in distributed maximum consensus has received limited attention in the literature. Traditional privacy-preserving methods typically add noise to updates, degrading the accuracy of the final result. To overcome these limitations, we propose a novel distributed optimization-based approach that preserves privacy without sacrificing accuracy. Our method introduces virtual nodes to form an augmented graph and leverages a carefully designed initialization process to ensure the privacy of honest participants, even when all their neighboring nodes are dishonest. Through a comprehensive information-theoretical analysis, we derive a sufficient condition to protect private data against both passive and eavesdropping adversaries. Extensive experiments validate the effectiveness of our approach, demonstrating that it not only preserves perfect privacy but also maintains accuracy, outperforming existing noise-based methods that typically suffer from accuracy loss.

Existing methods for inferring latent relational structures struggle to integrate partial prior knowledge, such as known edges, node-degree constraints, and global sparsity, without destabilizing training or conflicting with probabilistic assumptions. We propose Soft-Gated Structural Inference (SGSI), a VAE framework that seamlessly incorporates domain constraints via (1) soft gating with learnable edge masks to preserve gradients, (2) cloning-clamping of deterministic edges to avoid distributional conflicts, and (3) adaptive regularization to balance data-driven learning with domain constraints. By excluding known edges from stochastic inference, SGSI reallocates capacity to uncertain interactions, optimizing the information bottleneck trade-off. Experiments on 16 datasets show SGSI improves edge recovery by up to $9$% AUROC over baselines, scales to larger graphs ($94.2$% AUROC), and maintains stable training. SGSI bridges domain expertise with data-driven learning, enabling interpretable and robust structural discovery in dynamical systems.

Deep neural networks are widely deployed with quantization techniques to reduce memory and computational costs by lowering the numerical precision of their parameters. While quantization alters model parameters and their outputs, existing privacy analyses primarily focus on full-precision models, leaving a gap in understanding how bit-width reduction can affect privacy leakage. We present the first systematic study of the privacy–utility relationship in post-training quantization (PTQ), a versatile family of methods that can be applied to pretrained models without further training. Using membership inference attacks as our evaluation framework, we analyze three popular PTQ algorithms—AdaRound, BRECQ, and OBC—across multiple precision levels (4-bit, 2-bit, and 1.58-bit) on CIFAR-10, CIFAR-100, and TinyImageNet datasets. Our findings consistently show that low-precision PTQs can reduce privacy leakage. In particular, lower-precision models demonstrate up to an order of magnitude reduction in membership inference vulnerability compared to their full-precision counterparts, albeit at the cost of decreased utility. Additional ablation studies on the 1.58-bit quantization level show that quantizing only the last layer at higher precision enables fine-grained control over the privacy-utility trade-off. These results offer actionable insights for practitioners to balance efficiency, utility, and privacy protection in real-world deployments.

Abstract Gene regulatory networks (GRNs) are essential in studying cell differentiation and development. However, existing GRN inference models often disregard the network nature of GRNs, undermining the potential for GRN inference from scRNA-seq data. Popular GRN models such as PIDC and GENIE3 only consider at most triplet interactions among genes, significantly underestimating the regulation complexity in real biological systems. To showcase the importance of the network structure in GRNs, we proposed a novel GRN aggregation method, MuxGRN, which leverages multiplex link prediction to aggregate GRNs inferred from various state-of-the-art models and extracts the information propagated within different layers of GRNs. We tested MuxGRN on 14 real scRNA-seq datasets aggregated from 9 GRN models and compared it with 2 baseline edge-level aggregation methods. Our evaluation shows that MuxGRN achieves a top-tier averaged AUPRC among individual GRN models and discovers up to 26.55% new true positive edges, significantly outperforming baselines. This highlights the potential of link prediction in GRN aggregation for mining weak signals from inferred GRNs, and suggests that future development of GRN models should emphasize the network nature of GRNs. Introduction Gene regulatory networks (GRNs) are a core component in Systems Biology, capturing the complex interactions among genes that govern cell development and differentiation. Connected network modules are essential in gene regulatory analysis. Previous research shows that network motifs, such as feedforward loops and single-input modules, are meaningful functional units in GRN. From the perspective of information diffusion, regulations among genes are not isolated but propagated through the cascade in the network. However, existing GRN inference methods often overlook the intrinsic network nature of GRNs and focus only on pairwise or triplet interactions among genes. Popular methods such as PIDC decompose the interaction up to three genes, and GENIE3 only quantifies the contribution of one gene to reconstruct the expression of the target gene. To capture the cascade of gene regulations, a dynamic model that propagates information is required to capture the temporal evolution of gene expression. Ordinary differential equation (ODE) methods such as SCODE use ODE to model such dynamics, but their performances are not competitive compared to state-of-the-art (SOTA) methods [1] since existing ODE models cannot tackle thousands of genes. However, the ODE methods’ weakness should not rule out the importance of GRN network structures. To demonstrate the importance of GRN as a network, we proposed a novel GRN aggregation method, MuxGRN, which leverages variational graph autoencoder [2] (VGAE) to aggregate noisy GRNs inferred by various SOTA methods and discover new edges from information propagation within different layers of GRN. Different GRNs from GRN models can be viewed as a multiplex network, where each layer represents a GRN inferred by a specific method. We use CompGCN [3] to extract weak signals from different layers of GRNs and use the VGAE [2] framework to predict missing edges in a self-supervised manner. Our evaluation of 14 experimental data sets on the BEELINE benchmark [1] shows that MuxGRN can reach a level of performance similar to the best individual GRN model, of which up to 26.55% edges are new true positive edges. Our method outperforms two baseline edge-level aggregation methods, showcasing the potential of GRN aggregation via link prediction and a call for network-aware GRN inference. Related work COFFEE [4] proposed using the Borda count for GRN aggregation, but the Borda count is an edge-level aggregation and does not capture the characteristics of the GRN network. GENECI [5] and Fujii et al. [6] aim at finding the optimal weight of GRN that maximizes some topological measures of the network. However, weighted-averaging GRNs have a low degree of freedom, and reweighting the GRN to improve network topology does not modify the relative edge strengths. Finally, methods such as EnsInfer [7] and EnGRaiN [8] train a meta-model using GRNs as input and part of the ground truth edges as labels to predict the rest of the ground truth, which is biased towards the ground truth and exposed to the risk of incorrect edges in the ground truth. Thus, a network-aware GRN aggregation method that can discover new edges without relying on the ground truth is still missing. Methodology Our method, MuxGRN, aggregates GRNs inferred from various SOTA methods by multiplex link prediction. We deploy VGAE [2] to learn the node embeddings during the reconstruction of the multiplex network in a self-supervised manner. A multi-relational graph neural network model, CompGCN [3], is used as an encoder to extract weak signals from different layers of GRNs and compute node embeddings. The standard inner product decoder is used to reconstruct the multiplex network from the node embeddings, and new edges in the reconstructed network are considered as potential new regulations among genes. Detailed implementation is provided in our code repository https://github.com/1250326/MuxGRN. Evaluation We evaluated MuxGRN on the BEELINE benchmark [1], which contains 7 sets of experimental scRNA-seq datasets for human and mouse biological systems. The top 500 (1000) high-variance genes and their transcription factors are selected from each dataset, resulting in 14 datasets in total with 501–1783 genes on 2000 cells. We used the STRING database as ground-truth GRNs, with 3220–85,424 edges and 0.92%–4.19% density. AUPRC is used as an evaluation metric to measure the model’s precision and discrimination ability. We also computed the proportion of newly discovered true positive edges apart from edges in the union of all individual GRN models, normalized by the best individual GRN models for aggregation baselines to show the ability of finding new edges. We selected 9 SOTA GRN inference methods. GRNs are inferred using the default parameters in BEELINE, then aggregated by MuxGRN and two edge-level aggregation baselines, COFFEE [4] and Mean. COFFEE uses Borda count to compute the rank of each edge in each GRN and averages the ranks across different GRNs. In addition, we also designed a mean aggregation to compute the z-score of the edge weights in each GRN to denoise each GRN following the idea of CLR, and then average the z-scores across different GRNs. Limitation Despite promising results, our method has several limitations. First, the STRING ground truth is incomplete and biased towards well-studied genes, which may affect the evaluation of GRN models. Besides, the STRING database also lacks directionality and signs of regulations, which are essential in GRNs. Second, our method cannot predict the directionality of regulations, which can be addressed using a biaffine decoder. Future work focuses on solving these limitations. Acknowledgments Authors Tsz Pan Tong and Jun Pang acknowledge financial support from the Institute for Advanced Studies of the University of Luxembourg through an Audacity Grant (AUDACITY-2021). This work was also supported by the Luxembourg National Research Fund under the grant agreement INTER/NCN/24/18732364/EdgeCR. References 1. Pratapa A., Jalihal A.P., Law J.N., Bharadwaj A., and Murali T.M.. ‘Benchmarking algorithms for gene regulatory network inference from single-cell transcriptomic data.’ Nature Methods 2020;17(2):147–154. 2. Kipf T.N. and Welling M.. ‘Variational graph auto-encoders.’ arXiv preprint arXiv:1611.07308, 2016. 3. Vashishth S., Sanyal S., Nitin V., and Talukdar P.. ‘Composition-based multi-relational graph convolutional networks.’ In 8th International Conference on Learning Representations, 2020. 4. Lodi M.K., Chernikov A., and Ghosh P.. ‘COFFEE: consensus single cell-type specific inference for gene regulatory networks.’ Briefings in Bioinformatics 2024;25(6):bbae457. 5. Segura-Ortiz A., García-Nieto J., Aldana-Montes J.F., and Navas-Delgado I.. ‘GENECI: a novel evolutionary machine learning consensus-based approach for the inference of gene regulatory networks.’ Computers in Biology and Medicine 2023;155:106653. 6. Fujii C., Kuwahara H., Yu G., Guo L., and Gao X.. ‘Learning gene regulatory networks from gene expression data using weighted consensus.’ Neurocomputing 2017;220:23–33. 7. Shen B., Coruzzi G., and Shasha D.. ‘EnsInfer: a simple ensemble approach to network inference outperforms any single method.’ BMC Bioinformatics 2023;24(1):114. 8. Aluru M., Shrivastava H., Chockalingam S.P., Shivakumar

Multi-relational graph learning aims to embed entities and relations in knowledge graphs into low-dimensional representations, which has been successfully applied to various multi-relationship prediction tasks, such as information retrieval, question answering, and etc. Recently, contrastive learning has shown remarkable performance in multi-relational graph learning by data augmentation mechanisms to deal with highly sparse data. In this paper, we present a Multi-Relational Graph Contrastive Learning architecture (MRGCL) for multi-relational graph learning. More specifically, our MRGCL first proposes a Multi-relational Graph Hierarchical Attention Networks (MGHAN) to identify the importance between entities, which can learn the importance at different levels between entities for extracting the local graph dependency. Then, two graph augmented views with adaptive topology are automatically learned by the variant MGHAN, which can automatically adapt for different multi-relational graph datasets from diverse domains. Moreover, a subgraph contrastive loss is designed, which generates positives per anchor by calculating strongly connected subgraph embeddings of the anchor as the supervised signals. Comprehensive experiments on multi-relational datasets from three application domains indicate the superiority of our MRGCL over various state-of-the-art methods. Our datasets and source code are published at https://github.com/Legendary-L/MRGCL.

Real-world datasets often exhibit long-tailed distributions, raising important questions about how privacy risks evolve when machine learning (ML) models are applied to such data. In this work, we present a comprehensive analysis of membership inference attacks in long-tailed scenarios, revealing significant privacy vulnerabilities in tail data. We begin by examining standard ML models trained on long-tailed datasets and identify three key privacy risk effects: amplification, convergence, and polarization. Building on these insights, we extend our analysis to state-of-the-art long-tailed learning methods, such as foundation model-based approaches, offering new perspectives on how these models respond to membership inference attacks across head to tail classes. Finally, we investigate the privacy risks of ML models trained with differential privacy in long-tailed scenarios. Our findings corroborate that, even when ML models are designed to improve tail class performance to match head classes and are protected by differential privacy, tail class data remain particularly vulnerable to membership inference attacks.

The sudden onset of the recently concluded COVID-19 pandemic has driven substantial progress in various scientific fields. One notable example is the comprehension of public vaccination attitudes and the timely monitoring of their fluctuations through social media platforms. This approach can serve as a cost-effective means to supplement surveys in gathering public vaccine hesitancy levels. In this article, we propose a deep learning framework leveraging textual posts on social media to extract and track users’ vaccination stances in near real time. Compared to previous works, we integrate into the framework the recent posts of a user’s social network friends to collaboratively detect the user’s genuine attitude towards vaccination. Based on our annotated dataset from X (formerly known as Twitter), the models instantiated from our framework can increase the performance of attitude extraction by up to 23% compared to the state-of-the-art text-only models. Using this framework, we successfully confirm the feasibility of using social media to track the evolution of vaccination attitudes in real life. In addition, we illustrate the generality of our framework in extracting other public opinions such as political ideology. We further show one practical use of our framework by validating the possibility of forecasting a user’s vaccine hesitancy changes with information perceived from social media.

Estonia has been deploying electronic voting for its government elections since 2005. The underlying e-voting system and protocol have been continuously improved, aiming to fix the vulnerabilities found over the years and to provide election verifiability, which is now the standard way to ensure election integrity despite corrupt infrastructure or parties. Another goal is receipt-freeness, to ensure privacy even if voters are coerced. However, several recent attacks against its verifiability and privacy show the need of rigorous, realistic formal specifications for the protocol and its security, of new solutions to mitigate attacks, and of automated security proofs to ensure all attacks have been covered. In this paper we propose:

Graph Neural Networks (GNNs) are powerful techniques in representation learning for graphs and have been increasingly deployed in a multitude of different applications that involve node- and graph-wise tasks. Most existing studies solve either the node-wise task or the graph-wise task independently while they are inherently correlated. This work proposes a unified model, AdamGNN, to interactively learn node and graph representations in a mutual-optimisation manner. Compared with existing GNN models and graph pooling methods, AdamGNN enhances the node representation with the learned multi-grained semantics and avoids losing node features and graph structure information during pooling. Experiments on 14 real-world graph datasets show that AdamGNN can significantly outperform 17 competing models on both node- and graph-wise tasks. The ablation studies confirm the effectiveness of AdamGNN's components, and the last empirical analysis further reveals the ingenious ability of AdamGNN in capturing long-range interactions. This work was published at IEEE TKDE11Full paper is available at https://ieeexplore.ieee.org/document/9844866/.

This paper introduces a novel approach to structural inference, combining a variational dynamics encoder with partial correlation coefficients. In contrast to prior methods, our approach leverages variational inference to encode node dynamics within latent variables, and structural reconstruction relies on the calculation of partial correlation coefficients derived from these latent variables. This unique design endows our method with scalability and extends its applicability to both one-dimensional and multi-dimensional feature spaces. Furthermore, by reorganizing latent variables according to temporal steps, our approach can effectively reconstruct directed graph structures. We validate our method through extensive experimentation on twenty datasets from a benchmark dataset and biological networks. Our results showcase the superior scalability, accuracy, and versatility of our proposed approach compared to existing methods. Moreover, experiments conducted on noisy data affirm the robustness of our method.

This paper introduces SICSM, a novel structural inference framework that integrates Selective State Space Models (selective SSMs) with Generative Flow Networks (GFNs) to handle the challenges posed by dynamical systems with irregularly sampled trajectories and partial observations. By utilizing the robust temporal modeling capabilities of selective SSMs, our approach learns input-dependent transition functions that adapt to non-uniform time intervals, thereby enhancing the accuracy of structural inference. By aggregating dynamics across diverse temporal dependencies and channeling them into the GFN, the SICSM adeptly approximates the posterior distribution of the system's structure. This process not only enables precise inference of complex interactions within partially observed systems but also ensures the seamless integration of prior knowledge, enhancing the model’s accuracy and robustness. Extensive evaluations on sixteen diverse datasets demonstrate that SICSM outperforms existing methods, particularly in scenarios characterized by irregular sampling and incomplete observations, which highlight its potential as a reliable tool for scientific discovery and system diagnostics in disciplines that demand precise modeling of complex interactions.

Understanding complex dynamical systems begins with identifying their topological structures, which expose the organization of the systems. This requires robust structural inference methods that can deduce structure from observed behavior. However, existing methods are often domain-specific and lack a standardized, objective comparison framework. We address this gap by benchmarking 13 structural inference methods from various disciplines on simulations representing two types of dynamics and 11 interaction graph models, supplemented by a biological experimental dataset to mirror real-world application. We evaluated the methods for accuracy, scalability, robustness, and sensitivity to graph properties. Our findings indicate that deep learning methods excel with multi-dimensional data, while classical statistics and information theory based approaches are notably accurate and robust. Additionally, performance correlates positively with the graph's average shortest path length. This benchmark should aid researchers in selecting suitable methods for their specific needs and stimulate further methodological innovation.

The advancement of clustering heuristics has demonstrated that the addresses of Bitcoin, which are protected by their anonymous mechanisms, can be de-anonymized. While the state-of-the-art (SOTA) clustering heuristics focus on confirmed transactions stored in the blockchain, they ignore unconfirmed transactions in the mempool. These unconfirmed transactions contain information about transactions before being stored in the blockchain, covering additional address associations that can improve Bitcoin address clustering.

Abstract We propose a new deep learning cascade prediction model CasSIM that can simultaneously achieve two most demanded objectives: popularity prediction and final adopter prediction. Compared to existing methods based on cascade representation, CasSIM simulates information diffusion processes by exploring users’ dual roles in information propagation with three basic factors: users’ susceptibilities, influences and message contents. With effective user profiling, we are the first to capture the topic-specific property of susceptibilities and influences. In addition, the use of graph neural networks allows CasSIM to capture the dynamics of susceptibilities and influences during information diffusion. We evaluate the effectiveness of CasSIM on three real-life datasets and the results show that CasSIM outperforms the state-of-the-art methods in popularity and final adopter prediction.

Parameterized verification is a challenging problem that is known to be undecidable in the general case. ‍is a widely-used method for parameterized verification, originally proposed by Chou, Mannava and Park in 2004. It involves abstracting the protocol to a small fixed number of nodes, and strengthening by auxiliary invariants to refine the abstraction. In most of the existing applications of CMP, the abstraction and strengthening procedures are carried out manually, which can be tedious and error-prone. Existing theoretical justification of the ‍method is also done at a high level, without detailed descriptions of abstraction and strengthening rules. In this paper, we present a formally verified theory of ‍in Isabelle/HOL, with detailed, syntax-directed procedure for abstraction and strengthening that is proven correct. The formalization also includes correctness of symmetry reduction and assume-guarantee reasoning. We also describe a tool AutoCMP for automatically carrying out abstraction and strengthening in , as well as generating Isabelle proof scripts showing their correctness. We applied the tool to a number of parameterized protocols, and discovered some inaccuracies in previous manual applications of ‍to the FLASH cache coherence protocol.

The outbreak of the COVID-19 pandemic triggered the perils of misinformation over social media. By amplifying the spreading speed and popularity of trustworthy information, influential social media users have been helping overcome the negative impacts of such flooding misinformation. In this article, we use the COVID-19 pandemic as a representative global health crisisand examine the impact of the COVID-19 pandemic on these influential users’ subjective well-being (SWB), one of the most important indicators of mental health. We leverage X (formerly known as Twitter) as a representative social media platform and conduct the analysis with our collection of 37,281,824 tweets spanning almost two years. To identify influential X users, we propose a new measurement called user bridging performance (UBM) to evaluate the speed and wideness gain of information transmission due to their sharing. With our tweet collection, we manage to reveal the more significant mental sufferings of influential users during the COVID-19 pandemic. According to this observation, through comprehensive hierarchical multiple regression analysis , we are the first to discover the strong relationship between individual social users’ subjective well-being and their bridging performance. We proceed to extend bridging performance from individuals to user subgroups. The new measurement allows us to conduct a subgroup analysis according to users’ multilingualism and confirm the bridging role of multilingual users in the COVID-19 information propagation. We also find that multilingual users not only suffer from a much lower SWB in the pandemic, but also experienced a more significant SWB drop.

Recently, there is a surge in ransomware activities that encrypt users’ sensitive data and demand bitcoins for ransom payments to conceal the criminal’s identity. It is crucial for regulatory agencies to identify as many ransomware addresses as possible to accurately estimate the impact of these ransomware activities. However, existing methods for detecting ransomware addresses rely primarily on time-consuming data collection and clustering heuristics, and they face two major issues: (1) The features of an address itself are insufficient to accurately represent its activity characteristics, and (2) the number of disclosed ransomware addresses is extremely less than the number of unlabeled addresses. These issues lead to a significant number of ransomware addresses being undetected, resulting in a substantial underestimation of the impact of ransomware activities. To solve the above two issues, we propose an optimized ransomware address detection method based on Bitcoin transaction relationships, named XRAD , to detect more ransomware addresses with high performance. To address the first one, we present a cascade feature extraction method for Bitcoin transactions to aggregate features of related addresses after exploring transaction relationships. To address the second one, we build a classification model based on Positive-unlabeled learning to detect ransomware addresses with high performance. Extensive experiments demonstrate that XRAD significantly improves average accuracy, recall, and F1 score by 15.07%, 19.71%, and 34.83%, respectively, compared to state-of-the-art methods. In total, XRAD detects 120,335 ransomware activities from 2009 to 2023, revealing a development trend and average ransom payment per year that aligns with three reports by FinCEN, Chainalysis, and Coveware.

Electronic voting is a prominent example of conflicting requirements in security protocols, as the triad of privacy, verifiability and usability is essential for their deployment in practice. Receipt-freeness is a particularly strong notion of privacy, stating that it should be preserved even if voters cooperate with the adversary. While there are impossibility results showing we cannot have receipt-freeness and verifiability at the same time, there are several protocols that aim to achieve both, based on carefully devised trust assumptions. To evaluate their security, we propose a general symbolic definition of election verifiability, extending the state of the art to capture the more complex structure of receipt-free protocols. We apply this definition to analyse, using ProVerif, recent protocols with promising practical features: BeleniosRF and several variants of Selene. Against BeleniosRF, we find several attacks showing that verifiability in Belenios does indeed suffer from the attempt to introduce receipt-freeness. On the other hand, Selene satisfies a weaker notion of receipt-freeness, but we show that it satisfies verifiability in stronger corruption scenarios. We introduce a general frame-work to compare the verifiability of these protocols in various corruption scenarios and conclude with an analysis of SeleneRF, an attempt to get the best of both that we formalise in this paper. In addition to extending the symbolic model, our results point to foundational gaps in current cryptographic models for election verifiability, as they fail to uncover attacks that we do.

In multiagent systems (MASs), agents’ observation upon system behaviours may improve the overall team performance, but may also leak sensitive information to an observer. A quantified observability analysis can thus be useful to assist decision-making in MASs by operators seeking to optimise the relationship between performance effectiveness and information exposure through observations in practice. This paper presents a novel approach to quantitatively analysing the observability properties in MASs. The concept of opacity is applied to formally express the characterisation of observability in MASs modelled as partially observable multiagent systems. We propose a temporal logic oPATL to reason about agents’ observability with quantitative goals, which capture the probability of information transparency of system behaviours to an observer, and develop verification techniques for quantitatively analysing such properties. We implement the approach as an extension of the PRISM model checker, and illustrate its applicability via several examples.

peer reviewed

In this paper, we propose a novel framework, Active Learning based Structural Inference (ALaSI), to infer the existence of directed connections from observed agents' states over a time period in a dynamical system. With the help of deep active learning, ALaSI is competent in learning the representation of connections with a relatively small pool of prior knowledge. Moreover, based on information theory, the proposed inter- and out-of-scope message learning pipelines are remarkably beneficial to structural inference for large dynamical systems. We evaluate ALaSI on various large datasets including simulated systems and real-world networks, to demonstrate that ALaSI is able to outperform previous methods in precisely inferring the existence of connections in large systems under either supervised learning or unsupervised learning.

In this paper, we present an effective and efficient structural inference approach by integrating a Reservoir Computing (RC) network into a Variational Auto-encoder-based (VAE-based) structural inference framework. With the help of Bi-level Optimization, the backbone VAE-based method follows the Information Bottleneck principle and infers a general adjacency matrix in its latent space; the RC net substitutes the partial role of the decoder and encourages the whole approach to perform further steps of gradient descent based on limited available data. The experimental results on various datasets including biological networks, simulated fMRI data, and physical simulations show the effectiveness and efficiency of our proposed method for structural inference, either with much fewer trajectories or with much shorter trajectories compared with previous works.

Neural code intelligence models are cutting-edge automated code understanding technologies that have achieved remarkable performance in various software engineering tasks. However, the lack of deep learning models’ interpretability hinders the application of deep learning based code intelligence models in real-world scenarios, particularly in security-critical domains. Previous studies use program simplification to understand neural code intelligence models, but they have overlooked the fact that the most significant difference between source code and natural language is the code’s structural semantics.

Abstract Graph Neural Networks (GNNs) have become a prominent approach to machine learning with graphs and have been increasingly applied in a multitude of domains. Nevertheless, since most existing GNN models are based on flat message-passing mechanisms, two limitations need to be tackled: (i) they are costly in encoding long-range information spanning the graph structure; (ii) they are failing to encode features in the high-order neighbourhood in the graphs as they only perform information aggregation across the observed edges in the original graph. To deal with these two issues, we propose a novel Hierarchical Message-passing Graph Neural Networks framework. The key idea is generating a hierarchical structure that re-organises all nodes in a flat graph into multi-level super graphs, along with innovative intra- and inter-level propagation manners. The derived hierarchy creates shortcuts connecting far-away nodes so that informative long-range interactions can be efficiently accessed via message passing and incorporates meso- and macro-level semantics into the learned node representations. We present the first model to implement this framework, termed Hierarchical Community-aware Graph Neural Network (HC-GNN), with the assistance of a hierarchical community detection algorithm. The theoretical analysis illustrates HC-GNN’s remarkable capacity in capturing long-range information without introducing heavy additional computation complexity. Empirical experiments conducted on 9 datasets under transductive, inductive, and few-shot settings exhibit that HC-GNN can outperform state-of-the-art GNN models in network analysis tasks, including node classification, link prediction, and community detection. Moreover, the model analysis further demonstrates HC-GNN’s robustness facing graph sparsity and the flexibility in incorporating different GNN encoders.

We study the target control of asynchronous Boolean networks, to identify interventions that can drive the dynamics of a given Boolean network from any initial state to the desired target attractor. Based on the application time, the control can be realised with three types of perturbations, including instantaneous, temporary and permanent perturbations. We develop efficient methods to compute the target control for a given target attractor with these three types of perturbations. We compare our methods with the stable motif-based control method on a variety of real-life biological networks to evaluate their performance. We show that our methods scale well for large Boolean networks and they are able to identify a rich set of solutions with a small number of perturbations.

Graph Neural Networks (GNNs) are powerful techniques in representation learning for graphs and have been increasingly deployed in a multitude of different applications that involve node- and graph-wise tasks. Most existing studies solve either the node-wise task or the graph-wise task independently while they are inherently correlated. This work proposes a unified model, AdamGNN, to interactively learn node and graph representations in a mutual-optimisation manner. Compared with existing GNN models and graph pooling methods, AdamGNN enhances the node representation with the learned multi-grained semantics and avoids losing node features and graph structure information during pooling. Specifically, a differentiable pooling operator is proposed to adaptively generate a multi-grained structure that involves meso- and macro-level semantic information in the graph. We also devise the unpooling operator and theflybackaggregator in AdamGNN to better leverage the multi-grained semantics to enhance node representations. The updated node representations can further adjust the graph representation in the next iteration. Experiments on 14 real-world graph datasets show that AdamGNN can significantly outperform 17 competing models on both node- and graph-wise tasks. The ablation studies confirm the effectiveness of AdamGNN's components, and the last empirical analysis further reveals the ingenious ability of AdamGNN in capturing long-range interactions.

With their rapid development, the scale and complexity of software systems are rapidly growing. Identifying and organizing files of similar functionality into the same module, called architecture recovery, contributes to the maintainability of a software system. However, manual architecture recovery on large-sized software requires unbearable costs. Hence a lot of automatic algorithms have been proposed in recent years. However, current algorithms’ accuracy is still insufficient to support practical applications. To improve the accuracy of architecture recovery, this work proposes a novel algorithm, NEGAR, which leverages random walks to extract latent graphic information from the dependency graph of files in the software system and learn the node representation for clustering. The proposed algorithm NEGAR has been comprehensively evaluated on three medium-sized and two large-sized software systems, as well as a super large-sized software system, in terms of four widely-used metrics. The experimental results demonstrate the outstanding accuracy and excellent scalability of NEGAR.

Functional scenario comprehension of screens in Android applications paves the way for Android app development and Android UI testing, especially in automated UI testing and test reuse. On the one hand, the screens of diverse Android applications contain widgets with many combinations. On the other hand, the screens of different scenarios may leverage similar widgets to fulfill the functionalities. Due to the above reasons, scenario comprehension is still hard to be solved by current approaches. In this paper, to fully understand the functionality of each screen, we propose a novel approach that employs Graph Neural Networks (GNN) to classify scenarios leveraging the transitions between screens and other available information of screens altogether. According to the result evaluated on 30 popular applications in the file management category, our approach improves the classification accuracy by at least 6% compared to previous work, demonstrating that GNN can fully utilize the potential relations and dependencies between the transitioned screens.

In this paper, we propose a variational model, iterative Structural Inference of Directed Graphs (iSIDG), to infer the existence of directed interactions from observational agents’ features over a time period in a dynamical system. First, the iterative process in our model feeds the learned interactions back to encourage our model to eliminate indirect interactions and to emphasize directional representation during learning. Second, we show that extra regularization terms in the objective function for smoothness, connectiveness, and sparsity prompt our model to infer a more realistic structure and to further eliminate indirect interactions. We evaluate iSIDG on various datasets including biological networks, simulated fMRI data, and physical simulations to demonstrate that our model is able to precisely infer the existence of interactions, and is significantly superior to baseline models.

Abstract Recently, increasing attention has been paid to heterogeneous graph representation learning (HGRL), which aims to embed rich structural and semantic information in heterogeneous information networks (HINs) into low-dimensional node representations. To date, most HGRL models rely on hand-crafted meta-paths. However, the dependency on manually-defined meta-paths requires domain knowledge, which is difficult to obtain for complex HINs. More importantly, the pre-defined or generated meta-paths of all existing HGRL methods attached to each node type or node pair cannot be personalised to each individual node. To fully unleash the power of HGRL, we present a novel framework, Personalised Meta-path based Heterogeneous Graph Neural Networks (PM-HGNN), to jointly generate meta-paths that are personalised for each individual node in a HIN and learn node representations for the target downstream task like node classification. Precisely, PM-HGNN treats the meta-path generation as a Markov Decision Process and utilises a policy network to adaptively generate a meta-path for each individual node and simultaneously learn effective node representations. The policy network is trained with deep reinforcement learning by exploiting the performance improvement on a downstream task. We further propose an extension, PM-HGNN++, to better encode relational structure and accelerate the training during the meta-path generation. Experimental results reveal that both PM-HGNN and PM-HGNN++ can significantly and consistently outperform 16 competing baselines and state-of-the-art methods in various settings of node classification. Qualitative analysis also shows that PM-HGNN++ can identify meaningful meta-paths overlooked by human knowledge.

Exploiting the anonymous mechanism of Bitcoin, ransomware activities demanding ransom in bitcoins have become rampant in recent years. Several existing studies quantify the impact of ransomware activities, mostly focusing on the amount of ransom. However, victims’ reactions in Bitcoin that can well reflect the impact of ransomware activities are somehow largely neglected. Besides, existing studies track ransom transfers at the Bitcoin address level, making it difficult for them to uncover the patterns of ransom transfers from a macro perspective beyond Bitcoin addresses. In this article, we conduct a large-scale analysis of ransom payments, ransom transfers, and victim migrations in Bitcoin from 2012 to 2021. First, we develop a fine-grained address clustering method to cluster Bitcoin addresses into users, which enables us to identify more addresses controlled by ransomware criminals. Second, motivated by the fact that Bitcoin activities and their participants already formed stable industries, such as Darknet and Miner , we train a multi-label classification model to identify the industry identifiers of users. Third, we identify ransom payment transactions and then quantify the amount of ransom and the number of victims in 63 ransomware activities. Finally, after we analyze the trajectories of ransom transferred across different industries and track victims’ migrations across industries, we find out that to obscure the purposes of their transfer trajectories, most ransomware criminals (e.g., operators of Locky and Wannacry) prefer to spread ransom into multiple industries instead of utilizing the services of Bitcoin mixers. Compared with other industries, Investment is highly resilient to ransomware activities in the sense that the number of users in Investment remains relatively stable. Moreover, we also observe that a few victims become active in the Darknet after paying ransom. Our findings in this work can help authorities deeply understand ransomware activities in Bitcoin. While our study focuses on ransomware, our methods are potentially applicable to other cybercriminal activities that have similarly adopted bitcoins as their payments.

Model extraction attacks aim to duplicate a machine learning model through query access to a target model. Early studies mainly focus on discriminative models. Despite the success, model extraction attacks against generative models are less well explored. In this paper, we systematically study the feasibility of model extraction attacks against generative adversarial networks (GANs). Specifically, we first define fidelity and accuracy on model extraction attacks against GANs. Then we study model extraction attacks against GANs from the perspective of fidelity extraction and accuracy extraction, according to the adversary’s goals and background knowledge. We further conduct a case study where the adversary can transfer knowledge of the extracted model which steals a state-of-the-art GAN trained with more than 3 million images to new domains to broaden the scope of applications of model extraction attacks. Finally, we propose effective defense techniques to safeguard GANs, considering a trade-off between the utility and security of GAN models.

An information outbreak occurs on social media along with the COVID-19 pandemic and leads to infodemic. Predicting the popularity of online content, known as cascade prediction, allows for not only catching in advance hot information that deserves attention, but also identifying false information that will widely spread and require quick response to mitigate its impact. Among the various information diffusion patterns leveraged in previous works, the spillover effect of the information exposed to users on their decision to participate in diffusing certain information is still not studied. In this paper, we focus on the diffusion of information related to COVID-19 preventive measures. Through our collected Twitter dataset, we validated the existence of this spillover effect. Building on the finding, we proposed extensions to three cascade prediction methods based on Graph Neural Networks (GNNs). Experiments conducted on our dataset demonstrated that the use of the identified spillover effect significantly improves the state-of-the-art GNNs methods in predicting the popularity of not only preventive measure messages, but also other COVID-19 related messages.

Generative adversarial networks (GANs) have made unprecedented performance in image synthesis and play a key role in various downstream applications of computer vision. However, GAN models trained on sensitive data also pose a distinct threat to privacy. In this poster, we present a novel over-representation based membership inference attack. Unlike prior attacks against GANs which focus on the overall metrics, such as the attack accuracy, our attack aims to make inference from the high-precision perspective, which allows the adversary to concentrate on inferring a sample as a member confidently. Initial experimental results demonstrate that the adversary can achieve a high precision attack even if the overall attack accuracy is about 50% for a well-trained GAN model. Our work will raise awareness of the importance of precision when GAN owners evaluate the privacy risks of their models.

Election verifiability aims to ensure that the outcome produced by electronic voting systems correctly reflects the intentions of eligible voters, even in the presence of an adversary that may corrupt various parts of the voting infrastructure. Protecting such systems from manipulation is challenging because of their distributed nature involving voters, election authorities, voting servers and voting platforms. An adversary corrupting any of these can make changes that, individually, would go unnoticed, yet in the end will affect the outcome of the election. It is, therefore, important to rigorously evaluate whether the measures prescribed by election verifiability achieve their goals. We propose a formal framework that allows such an evaluation in a systematic and automated way. We demonstrate its application to the verification of various scenarios in Helios and Belenios, two prominent internet voting systems, for which we capture features and corruption models previously outside the scope of formal verification. Relying on the Tamarin protocol prover for automation, we derive new security proofs and attacks on deployed versions of these protocols, illustrating trade-offs between usability and security.

The Sinkhorn divergence has become a very popular metric to compare probability distributions in optimal transport. However, most works resort to the Sinkhorn divergence in Euclidean space, which greatly blocks their applications in complex data with nonlinear structure. It is therefore of theoretical demand to empower the Sinkhorn divergence with the capability of capturing nonlinear structures. We propose a theoretical and computational framework to bridge this gap. In this paper, we extend the Sinkhorn divergence in Euclidean space to the reproducing kernel Hilbert space, which we term "Hilbert Sinkhorn divergence" (HSD). In particular, we can use kernel matrices to derive a closed form expression of the HSD that is proved to be a tractable convex optimization problem. We also prove several attractive statistical properties of the proposed HSD, i.e., strong consistency, asymptotic behavior and sample complexity. Empirically, our method yields state-of-the-art performances on image classification and topological data analysis.

SUMMARY: Direct cell reprogramming, also called transdifferentiation, has great potential for tissue engineering and regenerative medicine. Boolean networks, a popular modelling framework for gene regulatory networks, make it possible to identify intervention targets for direct cell reprogramming with computational methods. In this work, we present our software, CABEAN, for the control of asynchronous Boolean networks. CABEAN identifies efficacious nodes, whose perturbations can drive the dynamics of a network from a source attractor (the initial cell type) to a target attractor (the desired cell type). CABEAN provides several control methods integrating practical constraints. Thus, it has the ability to provide a rich set of control sets, such that biologists can select suitable ones for validation based on specific experimental settings. AVAILABILITY AND IMPLEMENTATION: The executable binary and the user guide of the software are publicly available at https://satoss.uni.lu/software/CABEAN/.

Abstract Temporal networks are networks that edges evolve over time, hence link prediction in temporal networks aims at inferring new edges based on a sequence of network snapshots. In this paper, we propose a graph wavelet neural network (TT-GWNN) framework using topological and temporal features for link prediction in temporal networks. To capture topological and temporal features, we develope a second-order weighted random walk sampling algorithm. It combines network snapshots with both first-order and second-order weights into one weighted graph. Moreover, it incorporates a damping factor to assign greater weights to more recent snapshots. Next, we adopt graph wavelet neural networks to embed the vertices and use gated recurrent units for predicting new links. Extensive experiments demonstrate that TT-GWNN can effectively predict links on temporal networks.

With the development of next generation artificial intelligence, the interplay between knowledge-based approaches and machine learning approaches is gaining momentum. This trend drives the researchers to pay attention to possible and novel developments in relevant areas, either based on their theoretical foundations or based on their efficient applications. This special issue collects the newly developed works from logic, argumentation and artificial intelligence, to stimulate possible outcomes from their interactions. This volume includes 14 papers selected from 25 submissions accepted to the 2020 International Conferences on Logic and Artificial Intelligence at Zhejiang University (ZJULogAI). ZJULogAI was jointly organized by the University of Luxembourg and Zhejiang University as a three-day digital online event. It consists of three sub-events: the 5th Asian Workshop on Philosophical Logic (AWPL 2020), the 3rd International Conference on Logic and Argumentation (CLAR 2020) and the 6th Global Conference on Artificial Intelligence (GCAI 2020). Five experts (Christoph Benzmüller, Claude Sammut, Dag Westerståhl, Fei Wu and Marc van Zee) in logic and AI were invited to present their current work, covering the topics of ethical-legal AI systems, logic-based robots, big data intelligence and natural language and AI.

In recent years, great efforts have been made to analyze biological systems to understand the long-run behaviors. As a well-established formalism for modelling real-life biological systems, Boolean networks (BNs) allow their representation and analysis using formal reasoning and tools. Most biological systems are robust-they can withstand the loss of links and cope with external environmental perturbations. Hence, the BNs used to model such systems are necessarily large and dense, and yet modular. However, existing analysis methods only work well on networks of moderate size. Thus, there is a great need for efficient methods that can handle large-scale BNs and for doing so it is inevitable to exploit both the structural and dynamic properties of the networks. In this paper, we propose a method towards the optimal decomposition of BNs to balance the relation between the structure and dynamics of a network. We show that our method can greatly improve the existing decomposition-based attractor detection by analyzing a number of large real-life biological networks.

Within a framework for verifying parametric network protocols through induction, one needs to find invariants based on a protocol instance of a small number of nodes. In this paper, we propose a new approach to accelerate parameterized verification by adopting decision trees to represent the state space of a protocol instance. Such trees can be considered as a knowledge base that summarizes all behaviors of the protocol instance. With this knowledge base, we are able to efficiently construct an oracle to effectively assess candidates of invariants of the protocol, which are suggested by an invariant finder. With the discovered invariants, a formal proof for the correctness of the protocol can be derived in the framework after proper generalization. The effectiveness of our method is demonstrated by experiments with typical benchmarks.

Probabilistic game structures combine both nondeterminism and stochasticity, where players repeatedly take actions simultaneously to move to the next state of the concurrent game. Probabilistic alternating simulation is an important tool to compare the behaviour of different probabilistic game structures. In this paper, we present a sound and complete modal characterisation of this simulation relation by proposing a new logic based on probability distributions. The logic enables a player to enforce a property in the next state or distribution. Its extension with fixpoints, which also characterises the simulation relation, can express a lot of interesting properties in practical applications.

We study the problem of computing a minimal subset of nodes of a given asynchronous Boolean network that need to be perturbed in a single-step to drive its dynamics from an initial state to a target steady state (or attractor), which we call the source-target control of Boolean networks. Due to the phenomenon of state-space explosion, a simple global approach that performs computations on the entire network may not scale well for large networks. We believe that efficient algorithms for such networks must exploit the structure of the networks together with their dynamics. Taking this view, we derive a decomposition-based solution to the minimal source-target control problem which can be significantly faster than the existing approaches on large networks. We then show that the solution can be further optimized if we take into account appropriate information about the source state. We apply our solutions to both real-life biological networks and randomly generated networks, demonstrating the efficiency and efficacy of our approach.

Parameterized verification is shown to be a complicated and undecidable problem. The challenge of parameterized verification lies in how to construct appropriate invariants. Designing algorithms to find such invariants automatically has become an active research area since the last decade. With the advent of some recent works, automatically finding invariants has become possible, but most of these invariants are unreadable, making them difficult to be understood by protocol designers and researchers. Therefore, we propose an automatic framework that learns a set of readable and simple invariants to support in protocol design. It takes advantage of association rule learning, and combines the learning algorithm with parameterized verification. It is noteworthy that the gap between machine learning algorithms and parameterized verification seems to be huge, as they rely on statistical learning and symbolic reasoning, respectively. Our framework, however, builds a bridge through association rules and invariants, making their combination possible. Besides, we also propose an invariant-guided strengthening paradigm, providing an innovative perspective to existing abstraction-strengthening methods. Our framework has been successfully applied to several benchmarks, including an industrial-scale protocol FLASH.

MOTIVATION: The control of Boolean networks has traditionally focussed on strategies where the perturbations are applied to the nodes of the network for an extended period of time. In this work, we study if and how a Boolean network can be controlled by perturbing a minimal set of nodes for a single-step and letting the system evolve afterwards according to its original dynamics. More precisely, given a Boolean network (BN), we compute a minimal subset Cmin of the nodes such that BN can be driven from any initial state in an attractor to another 'desired' attractor by perturbing some or all of the nodes of Cmin for a single-step. Such kind of control is attractive for biological systems because they are less time consuming than the traditional strategies for control while also being financially more viable. However, due to the phenomenon of state-space explosion, computing such a minimal subset is computationally inefficient and an approach that deals with the entire network in one-go, does not scale well for large networks. RESULTS: We develop a 'divide-and-conquer' approach by decomposing the network into smaller partitions, computing the minimal control on the projection of the attractors to these partitions and then composing the results to obtain Cmin for the whole network. We implement our method and test it on various real-life biological networks to demonstrate its applicability and efficiency. SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.

Abstract Computation of steady-state probabilities is an important aspect of analysing biological systems modelled as probabilistic Boolean networks (PBNs). For small PBNs, efficient numerical methods to compute steady-state probabilities of PBNs exist, based on the Markov chain state-transition matrix. However, for large PBNs, numerical methods suffer from the state-space explosion problem since the state-space size is exponential in the number of nodes in a PBN. In fact, the use of statistical methods and Monte Carlo methods remain the only feasible approach to address the problem for large PBNs. Such methods usually rely on long simulations of a PBN. Since slow simulation can impede the analysis, the efficiency of the simulation procedure becomes critical. Intuitively, parallelising the simulation process is the ideal way to accelerate the computation. Recent developments of general purpose graphics processing units (GPUs) provide possibilities to massively parallelise the simulation process. In this work, we propose a trajectory-level parallelisation framework to accelerate the computation of steady-state probabilities in large PBNs with the use of GPUs. To maximise the computation efficiency on a GPU, we develop a dynamical data arrangement mechanism for handling different size PBNs with a GPU. Specially, we propose a reorder-and-split method to handle both large and dense PBNs. Besides, we develop a specific way of storing predictor functions of a PBN and the state of the PBN in the GPU memory. Moreover, we introduce a strongly connected component (SCC)-based network reduction technique to further accelerate the computation speed. Experimental results show that our GPU-based parallelisation gains approximately a 600-fold speedup for a real-life PBN compared to the state-of-the-art sequential method.

Cellular reprogramming, a technique that opens huge opportunities in modern and regenerative medicine, heavily relies on identifying key genes to perturb. Most of the existing computational methods for controlling which attractor (steady state) the cell will reach focus on finding mutations to apply to the initial state. However, it has been shown, and is proved in this article, that waiting between perturbations so that the update dynamics of the system prepares the ground, allows for new reprogramming strategies. To identify such sequential perturbations, we consider a qualitative model of regulatory networks, and rely on Binary Decision Diagrams to model their dynamics and the putative perturbations. Our method establishes a set identification of sequential perturbations, whether permanent (mutations) or only temporary, to achieve the existential or inevitable reachability of an arbitrary state of the system. We apply an implementation for temporary perturbations on models from the literature, illustrating that we are able to derive sequential perturbations to achieve trans-differentiation.

Boolean networks is a well-established formalism for modelling biological systems. A vital challenge for analyzing a Boolean network is to identify all the attractors. This becomes more challenging for large asynchronous Boolean networks, due to the asynchronous scheme. Existing methods are prohibited due to the well-known state-space explosion problem in large Boolean networks. In this paper, we tackle this challenge by proposing a SCC-based decomposition method. We prove the correctness of our proposed method and demonstrate its efficiency with two real-life biological networks.

This demo introduces L-CMP, an automatic learning-based parameterized verification tool. It can verify parameterized protocols by combining machine learning and model checking techniques. Given a parameterized protocol, L-CMP learns a set of auxiliary invariants and implements verification of the protocol using the invariants automatically. In particular, the learned auxiliary invariants are straightforward and readable. The experimental results show that L-CMP can successfully verify a number of cache coherence protocols, including the industrial-scale FLASH protocol. The video is available at https://youtu.be/6Dl2HiiiS4E, and L-CMPL-CMP can be downloaded at https://github.com/ ArabelaTso/Learning-Based-ParaVerifer.

Hashtag has emerged as a widely used concept of popular culture and campaigns, but its implications on people»s privacy have not been investigated so far. In this paper, we present the first systematic analysis of privacy issues induced by hashtags. We concentrate in particular on location, which is recognized as one of the key privacy concerns in the Internet era. By relying on a random forest model, we show that we can infer a user»s precise location from hashtags with accuracy of 70% to 76%, depending on the city. To remedy this situation, we introduce a system called Tagvisor that systematically suggests alternative hashtags if the user-selected ones constitute a threat to location privacy. Tagvisor realizes this by means of three conceptually different obfuscation techniques and a semantics-based metric for measuring the consequent utility loss. Our findings show that obfuscating as little as two hashtags already provides a near-optimal trade-off between privacy and utility in our dataset. This in particular renders Tagvisor highly time-efficient, and thus, practical in real-world settings.

As a well-established computational framework, probabilistic Boolean networks (PBNs) are widely used for modelling, simulation, and analysis of biological systems. To analyze the steady-state dynamics of PBNs is of crucial importance to explore the characteristics of biological systems. However, the analysis of large PBNs, which often arise in systems biology, is prone to the infamous state-space explosion problem. Therefore, the employment of statistical methods often remains the only feasible solution. We present ${\mathsf{ASSA-PBN}}$ , a software toolbox for modelling, simulation, and analysis of PBNs. ${\mathsf{ASSA-PBN}}$ provides efficient statistical methods with three parallel techniques to speed up the computation of steady-state probabilities. Moreover, particle swarm optimisation (PSO) and differential evolution (DE) are implemented for the estimation of PBN parameters. Additionally, we implement in-depth analyses of PBNs, including long-run influence analysis, long-run sensitivity analysis, computation of one-parameter profile likelihoods, and the visualization of one-parameter profile likelihoods. A PBN model of apoptosis is used as a case study to illustrate the main functionalities of ${\mathsf{ASSA-PBN}}$ and to demonstrate the capabilities of ${\mathsf{ASSA-PBN}}$ to effectively analyse biological systems modelled as PBNs.

Probabilistic Boolean networks (PBNs) is a well-established computational framework for modelling biological systems. The steady-state dynamics of PBNs is of crucial importance in the study of such systems. However, for large PBNs, which often arise in systems biology, obtaining the steady-state distribution poses a significant challenge. In this paper, we revive the two-state Markov chain approach to solve this problem. This paper contributes in three aspects. First, we identify a problem of generating biased results with the approach and we propose a few heuristics to avoid such a pitfall. Second, we conduct an extensive experimental comparison of the extended two-state Markov chain approach and another approach based on the Skart method. We analyze the results with machine learning techniques and we show that statistically the two-state Markov chain approach has a better performance. Finally, we demonstrate the potential of the extended two-state Markov chain approach on a case study of a large PBN model of apoptosis in hepatocytes.

Formal verification of parameterized protocols such as cache coherence protocols is a significant challenge. In this article, we propose an automatic proving approach and its prototype paraVerifier to handle this challenge within a unified framework as follows: (1) To prove the correctness of a parameterized protocol, our approach automatically discovers auxiliary invariants and the corresponding dependency relations among the discovered invariants and protocol rules from a small instance of the to-be-verified protocol, and (2) the discovered invariants and dependency graph are then automatically generalized into a parameterized form and sent to the theorem prover, Isabelle. As a side product, the final verification result of a protocol is provided by a formal and human-readable proof. Our approach has been successfully applied to a number of benchmarks, including snoopying-based and directory-based cache coherence protocols.

The development of positioning technologies has resulted in an increasing amount of mobility data being available. While bringing a lot of convenience to people's life, such availability also raises serious concerns about privacy. In this paper, we concentrate on one of the most sensitive information that can be inferred from mobility data, namely social relationships. We propose a novel social relation inference attack that relies on an advanced feature learning technique to automatically summarize users' mobility features. Compared to existing approaches, our attack is able to predict any two individuals' social relation, and it does not require the adversary to have any prior knowledge on existing social relations. These advantages significantly increase the applicability of our attack and the scope of the privacy assessment. Extensive experiments conducted on a large dataset demonstrate that our inference attack is effective, and achieves between 13% to 20% improvement over the best state-of-the-art scheme. We propose three defense mechanisms -- hiding, replacement and generalization -- and evaluate their effectiveness for mitigating the social link privacy risks stemming from mobility data sharing. Our experimental results show that both hiding and replacement mechanisms outperform generalization. Moreover, hiding and replacement achieve a comparable trade-off between utility and privacy, the former preserving better utility and the latter providing better privacy.

With the prevalence of location-based social networks (LBSNs), automated semantic annotation for places plays a critical role in many LBSN-related applications. Although a line of research continues to enhance labeling accuracy, there is still a lot of room for improvement. The crucial problem is to find a high-quality representation for each place. In previous works, the representation is usually derived directly from observed patterns of places or indirectly from calculated proximity amongst places or their combination. In this paper, we also exploit the combination to represent places but present a novel semi-supervised learning framework based on graph embedding, called Predictive Place Embedding (PPE). For place proximity, PPE first learns user embeddings from a user-tag bipartite graph by minimizing supervised loss in order to preserve the similarity of users visiting analogous places. User similarity is then transformed into place proximity by optimizing each place embedding as the centroid of the vectors of its check-in users. Our underlying idea is that a place can be considered as a representative of all its visitors. For observed patterns, a place-temporal bipartite graph is used to further adjust place embeddings by reducing unsupervised loss. Extensive experiments on real large LBSNs show that PPE outperforms state-of-the-art methods significantly.

Hashtags, created by social network users, have gained a huge popularity in recent years. As a kind of metatag for organizing information, hashtags in online social networks, especially in Instagram, have greatly facilitated users' interactions. In recent years, academia starts to use hashtags to reshape our understandings on how users interact with each other. #like4like is one of the most popular hashtags in Instagram with more than 290 million photos appended with it, when a publisher uses #like4like in one photo, it means that he will like back photos of those who like this photo. Different from other hashtags, #like4like implies an interaction between a photo's publisher and a user who likes this photo, and both of them aim to attract likes in Instagram. In this paper, we study whether #like4like indeed serves the purpose it is created for, i.e., will #like4like provoke more likes? We first perform a general analysis of #like4like with 1.8 million photos collected from Instagram, and discover that its quantity has dramatically increased by 1,300 times from 2012 to 2016. Then, we study whether #like4like will attract likes for photo publishers; results show that it is not #like4like but actually photo contents attract more likes, and the lifespan of a #like4like photo is quite limited. In the end, we study whether users who like #like4like photos will receive likes from #like4like publishers. However, results show that more than 90% of the publishers do not keep their promises, i.e., they will not like back others who like their #like4like photos; and for those who keep their promises, the photos which they like back are often randomly selected.

Parameterized verification of parameterized protocols like cache coherence protocols is an important but hard problem. Our tool paraVerifier handles this hard problem in a unified framework: (1) it automatically discovers auxiliary invariants and the corresponding causal relations from a small reference instance of the verified protocol; (2) the above invariants and causal relation information are automatically generalized into a parameterized form to construct a parameterized formal proof in a theorem prover (e.g., Isabelle). Our method is successfully applied to typical benchmarks including snooping and directory cache coherence protocol benchmarks. The correctness of these protocols is guaranteed by a formal and readable proof which is automatically generated. The notoriously hard FLASH protocol, which is at an industrial scale, is also verified.

In recent years, access control in online social networks has attracted academia a considerable amount of attention. Previously, researchers mainly studied this topic from a formal perspective. On the other hand, how users actually use access control in their daily social network life is left largely unexplored. This paper presents the first large-scale empirical study on users' access control usage on Twitter and Instagram. Based on the data of 150k users on Twitter and 280k users on Instagram collected consecutively during three months in New York, we have conducted both static and dynamic analysis on users' access control usage. Our findings include: female users, young users and Asian users are more concerned about their privacy; users who enable access control setting are less active and have smaller online social circles; global events and important festivals can influence users to change their access control setting. Furthermore, we exploit machine learning classifiers to perform an access control setting prediction. Through experiments, the predictor achieves a fair performance with the AUC equals to 0.70, indicating whether a user enables her access control setting or not can be predicted to a certain extent.

No abstract available.

No abstract available.

With the emerging of online social network services, quantitative studies on social influence become achievable. Leadership is one of the most intuitive and common forms for social influence, understanding it could result in appealing applications such as targeted advertising and viral marketing. In this work, we focus on investigating leaders' influence for event prediction in social networks. We propose an algorithm based on events that users conduct to discover leaders in social communities. Analysis on the leaders that we found on a real-life social network dataset leads us to several interesting observations, such as that leaders do not have significantly higher number of friends but are more active than other community members. We demonstrate the effectiveness of leaders' influence on users' behaviors by learning tasks: given a leader has conducted one event, whether and when a user will perform the event. Experimental results show that with only a few leaders in a community the event predictions are always very effective.

Molecular-scale Network-on-Chip (mNoC) crossbars use quantum dot LEDs as an on-chip light source, and chromophores to provide optical signal filtering for receivers. An mNoC reduces power consumption or enables scaling to larger crossbars for a reduced energy budget compared to current nanophotonic NoC crossbars. Since communication latency is reduced by using a high-radix crossbar, minimizing power consumption becomes a primary design target. Conventional Single Writer Multiple Reader (SWMR) photonic crossbar designs broadcast all packets, and incur the commensurate required power, even if only two nodes are communicating.

With the ubiquity of GPS-enabled devices and location-based social network services, research on human mobility becomes quantitatively achievable. Understanding it could lead to appealing applications such as city planning and epidemiology. In this paper, we focus on predicting whether two individuals are friends based on their mobility information. Intuitively, friends tend to visit similar places, thus the number of their co-occurrences should be a strong indicator of their friendship. Besides, the visiting time interval between two users also has an effect on friendship prediction. By exploiting machine learning techniques, we construct two friendship prediction models based on mobility information. The first model focuses on predicting friendship of two individuals with only one of their co-occurred places' information. The second model proposes a solution for predicting friendship of two individuals based on all their co-occurred places. Experimental results show that both of our models outperform the state-of-the-art solutions.

Relationship-based access control schemes have been studied to protect users' privacy in online social networks. In this paper, we propose cryptographic protocols for decentralized social networks to enforce relationship-based access control polices, i.e., K-common friends and k-depth. Our protocols are mainly built on pairing-based cryptosystems. We prove their security under the honest but curious adversary model, and we analyze their computation and communication complexities. Furthermore, we evaluate their efficiency through simulations on a real social network dataset.

Boolean networks are an important formalism for modelling biological systems and have attracted much attention in recent years. An important direction in Boolean networks is to exhaustively find attractors, which represent steady states when a biological network evolves for a long term. In this paper, we propose a new approach to improve the efficiency of BDD-based attractor detection. Our approach includes a monolithic algorithm for small networks, an enumerative strategy to deal with large networks, and two heuristics on ordering BDD variables. We demonstrate the performance of our approach on a number of examples, and compare it with one existing technique in the literature.

Nowadays in popular online social networks users can blacklist some of their friends in order to disallow them to access resources that other non-blacklisted friends may access. We identify three independent binary decisions to utilize users' blacklists in access control policies, resulting into eight access restrictions. We formally define these restrictions in a hybrid logic for relationship-based access control, and provide syntactical transformations to rewrite a hybrid logic access control formula when fixing an access restriction. This enables a flexible and user-friendly approach for restricting access in social networks. We develop efficient algorithms for enforcing a subset of access control policies with restrictions. The effectiveness of the access restrictions and the efficiency of our algorithms are evaluated on a Facebook dataset.

Abstract We formalize in a theorem prover the notion of provable anonymity. Our formalization relies on inductive definitions of message distinguishing ability and observational equivalence on traces observed by the intruder. Our theory differs from its original proposal and essentially boils down to the inductive definition of distinguishing messages with respect to a knowledge set for the intruder. We build our theory in Isabelle/HOL to achieve a mechanical framework for the analysis of anonymity protocols. Its feasibility is illustrated through two case studies of the Crowds and Onion Routing protocols.

Moore's law and the continuity of device scaling have led to an increasing number of cores/nodes on a chip, creating a need for new mechanisms to achieve high-performance and power-efficient Network-on-Chip (NoC). Nanophotonics based NoCs provide for higher bandwidth and more power efficient designs than electronic networks. Present approaches often use an external laser source, ring resonators, and waveguides. However, they still suffer from important limitations: large static power consumption, and limited network scalability. In this article, we explore the use of emerging molecular scale devices to construct nanophotonic networks: Molecular-scale Network-on-Chip (mNoC). We leverage on-chip emitters such as quantum dot LEDs, which provide electrical to optical signal modulation, and chromophores, which provide optical signal filtering for receivers. These devices replace the ring resonators and the external laser source used in contemporary nanophotonic NoCs. They reduce energy consumption or enable scaling to larger crossbars for a reduced energy budget. We present a Single Writer Multiple Reader (SWMR) bus based crossbar mNoC. Our evaluation shows that an mNoC can achieve more than 88% reduction in energy for a 64×64 crossbar compared to similar ring resonator based designs. Additionally, an mNoC can scale to a 256×256 crossbar with an average 10% performance improvement and 54% energy reduction.

The popularity of online social networks (OSNs) makes the protection of users' private information an important but scientifically challenging problem. In the literature, relationship-based access control schemes have been proposed to address this problem. However, with the dynamic developments of OSNs, we identify new access control requirements which cannot be fully captured by the current schemes. In this paper, we focus on public information in OSNs and treat it as a new dimension which users can use to regulate access to their resources. We define a new OSN model containing users and their relationships as well as public information. Based on this model, we introduce a variant of hybrid logic for formulating access control policies. A type of category relations among public information are exploited to further improve our logic for its usage in practice. In addition, we propose a few solutions to address the problem of information reliability in OSNs.

Trends in increasing web traffic demand an increase in server throughput while preserving energy efficiency and total cost of ownership. Present work in optimizing data center efficiency primarily focuses on the data center as a whole, using off-the-shelf hardware for individual servers. Server capacity is typically increased by adding more machines, which is cheap, though inefficient in the long run in terms of energy and area.

In this paper, we describe our analysis of a recently proposed electric vehicle charing protocol. The protocol builds on complicated cryptographic primitives such as commitment, zero-knowledge proofs, BBS+ signature and etc. Moreover, interesting properties such as secrecy, authentication, anonymity, and location privacy are claimed on this protocol. It thus presents a challenge for formal verification, as existing tools for security protocol analysis lack support for all the required features. In our analysis, we employ and combine the strength of two state-of-the-art symbolic verifiers, Tamarin and Prove if, to check all important properties of the protocol.

The expression of genes is a fundamental process in living cells, both eukaryotic and prokaryotic. The regulation of gene expression is achieved via sophisticated networks of interactions between DNA, RNA, proteins, and small chemical compounds. The qualitative and quantitative characterisation of interactions between genes is one of the major current research targets in systems biology. In this PhD research project, we view gene regulatory networks as Markov chains, resulting from popular formalisation frameworks such as Dynamic Bayesian Networks and Probabilistic Boolean Networks. This will allow us to reason about both the structure and strength of gene interactions. Our goal is to develop new algorithms and tools, which are tailored for the modelling and analysis of gene regulatory networks, by exploring model checking techniques that have been developed and widely used in computer science. More specifically, we will combine model checking techniques with sampling and optimisation methods from the literature to derive new techniques to solve the parameter estimation problem of Markov models of gene regulatory networks.

Abstract: Usage control extends access control by enabling the specification of requirements that should be satisfied before, while and after access. To ensure that the deployment of usage control policies in target domains achieves the required security goals, policy verification and analysis tools are needed. In this paper, we present an approach for the dynamic analysis of usage control policies using formal descriptions of target domains and their usage control policies. Our approach provides usage control management explicit labeled transition system semantics and enables the automated verification of usage control policies using model checking. 1

Nowadays, the accumulation of people's whereabouts due to location-based applications has made it possible to construct their mobility profiles. This access to users' mobility profiles subsequently brings benefits back to location-based applications. For instance, in on-line social networks, friends can be recommended not only based on the similarity between their registered information, for instance, hobbies and professions but also referring to the similarity between their mobility profiles. In this article, we propose a new approach to construct and compare users' mobility profiles. First, we improve and apply frequent sequential pattern mining technologies to extract the sequences of places that a user frequently visits and use them to model his mobility profile. Second, we present a new method to calculate the similarity between two users using their mobility profiles. More specifically, we identify the weaknesses of a similarity metric in the literature, and propose a new one which not only fixes the weaknesses but also provides more precise and effective similarity estimation. Third, we consider the semantics of spatio-temporal information contained in user mobility profiles and add them into the calculation of user similarity. It enables us to measure users' similarity from different perspectives. Two specific types of semantics are explored in this article: location semantics and temporal semantics . Last, we validate our approach by applying it to two real-life datasets collected by Microsoft Research Asia and Yonsei University, respectively. The results show that our approach outperforms the existing works from several aspects.

Through real-life experiments, it has been proved that spoofing is a practical threat to applications using the free civil service provided by Global Navigation Satellite Systems (GNSS). In this paper, we demonstrate a prototype that can verify the integrity of GNSS civil signals. By integrity we intuitively mean that civil signals originate from a GNSS satellite without having been artificially interfered with. Our prototype provides interfaces that can incorporate existing spoofing detection methods whose results are then combined into an overall evaluation of the signal's integrity, which we call integrity level. Considering the various security requirements from different applications, integrity levels can be calculated in many ways determined by their users. We also present an application scenario that deploys our prototype and offers a public central service -- localisation assurance certification. Through experiments, we successfully show that our prototype is not only effective but also efficient in practice.

Location-based services have been enduring a fast development for almost fifteen years. Due to the lack of proper privacy protection, especially in the early stage of the development, an enormous amount of user request records have been collected. This exposes potential threats to users' privacy as new contextual information can be extracted from such records. In this paper, we study query dependency which can be derived from users' request history, and investigate its impact on users' query privacy. To achieve our goal, we present an approach to compute the probability for a user to issue a query, by taking into account both user's query dependency and observed requests. We propose new metrics incorporating query dependency for query privacy, and adapt spatial generalisation algorithms in the literature to generate requests satisfying users' privacy requirements expressed in the new metrics. Through experiments, we evaluate the impact of query dependency on query privacy and show that our proposed metrics and algorithms are effective and efficient for practical applications.

Through real-life experiments, it has been proved, not only in theory but also in practice, that civil signals of Global Navigation Satellite Systems (GNSS) can be spoofed. Consequently, a number of spoofing detection techniques have been proposed to verify the integrity of GNSS signals. In this paper, we develop a novel trust framework based on subjective logic to evaluate the integrity of received GNSS civil signals. We formally define signal integrity for the first time in the framework and use it to precisely characterise different spoofing detection methods. Our framework captures the uncertainty during the inference of signal integrity which has been largely ignored or not explicitly specified in the literature. Our framework also gives rise to several natural ways to combine the outputs of various spoofing detection methods on signal integrity. We validate our framework through experiments using both real and simulated signals and the results show that our framework is effective.

Abstract In this paper, we develop an inductive approach to strand spaces, by introducing an inductive definition for bundles. This definition provides us not only a constructive illustration for bundles, but also an effective and rigorous technique of rule induction to reason about properties of bundles. With this induction principle, we can prove that our bundle model is sound in the sense that a bundle is a causally well-founded graph. This approach also gives an alternative to rigorously prove a generalized version of authentication tests. To illustrate the applicability of our approach, we have performed case studies on verification of secrecy and authentication properties of the Needham–Schroeder–Lowe and Otway–Rees protocols. Our approach has been mechanized using Isabelle/HOL.

With the prevalence of GNSS technologies, nowadays freely available for everyone, location-based vehicle services such as electronic tolling pricing systems and pay-as-you-drive services are rapidly growing. Because these systems collect and process travel records, if not carefully designed, they can threaten users' location privacy. Finding a secure and privacy-friendlysolution is a challenge for system designers. Besides location privacy, communication and computation overhead should be taken into account as well in order to make such systems widely adopted in practice. In this paper, we propose a new electronic toll pricing system based on group signatures. Our system preserves anonymity of users within groups, in addition to correctness and accountability. It also achieves a balance between privacy and overhead imposed upon user devices.

The popularity of location-based services leads to serious concerns on user privacy. A common mechanism to protect users' location and query privacy is spatial generalisation. As more user information becomes available with the fast growth of Internet applications, e.g., social networks, attackers have the ability to construct users' personal profiles. This gives rise to new challenges and reconsideration of the existing privacy metrics, such as k-anonymity. In this paper, we propose new metrics to measure users' query privacy taking into account user profiles. Furthermore, we design spatial generalisation algorithms to compute regions satisfying users' privacy requirements expressed in these metrics. By experimental results, our metrics and algorithms are shown to be effective and efficient for practical usage.

Wireless sensor networks with hundreds of sensor nodes have emerged in recent years as important platforms for a wide spectrum of monitoring tasks ranging from environmental to military applications. In order to support scalability and increase lifetime of these networks, sensor nodes are preferably grouped into clusters. A large number of clustering protocols have been proposed in the literature with different aims, requirements and efficiency. Previous comparative studies of such protocols were usually based on simulation, which, however, only provides average case results on the limited state space explored. To mend this situation, in this paper, we evaluate and compare four state-of-the-art clustering protocols, i.e., LEACH, GENLEACH, HEED and PANEL, with full state space exploration. Within our analytical framework that consists of a network configuration and an energy consumption model, we aim at analyzing the correctness and performance of the investigated protocols. Our analysis is conducted formally through probabilistic model checking using PRISM and has its focus on the quantitative aspects of the protocols.

Social networking sites have sprung up and become a hot issue of current society. In spite of the fact that these sites provide users with a variety of attractive features, much to users' dismay, however, they are prone to expose users' private information. In this paper, we propose an approach whi ch addresses the problem of collaboratively deciding privacy policies for, but not limited to, shared photos. Our approach utilizes trust relations in social networks and combines them with Condorcet's preferential voting scheme. We study properties of our trust-augmented voting scheme and develop two approximations to improve its efficiency. Our algorithms are compared and justified by experimental results, which support the usability of our trust-augmented voting scheme.

Transparency is crucial to ensuring fair, honest elections. Transparency is achieved by making information (e.g. election result) public. In e-voting literature, this publication is often described in terms of a bulletin board. While privacy of voting systems has been actively studied in recent years, resulting in various analysis frameworks, to date there has not been an explicit modelling of bulletin board in any such framework. Privacy implications of bulletin boards are thus understudied. In this paper, we extend the semantics of the framework of Jonker, Mauw and Pang to model a bulletin board and capture coercion-resistance. The usage of the extended framework is illustrated by an application to the Pret a Voter voting system. Moreover, we present an information-theoretical measure of privacy loss in elections.

We formalise in a theorem prover the notion of provable anonymity proposed by Garcia et al. Our formalization relies on inductive definitions of message distinguish ability and observational equivalence over observed traces by the intruder. Our theory differs from its original proposal which essentially boils down to the existence of a reinterpretation function. We build our theory in Isabelle/HOL to have a mechanical framework for the analysis of anonymity protocols. Its feasibility is illustrated through the onion routing protocol.

Cederquist et al. proposed an optimistic certified email protocol, which employs key chains to reduce the storage requirement of the trusted third party (TTP). We extend their protocol to satisfy the property of TTP transparency, using existing verifiably encrypted signature schemes. An implementation with the scheme based on bilinear pairing makes our extension one of the most efficient certified email protocols satisfying strong fairness, timeliness, and TTP transparency.

In the field of distributed computing, there are many round-based algorithms to solve fundamental problems, such as leader election and distributed consensus. Due to the nature of these algorithms, round numbers are unbounded and can increase infinitely during executions of the algorithms. This can lead to the state space explosion problem when verifying correctness of these algorithms using model checking. In this paper, we present a general idea of investigating the bounded distance of round numbers in round-based algorithms. We can manage to transform their state spaces into finite by maintaining such relations in a proper way, and thus make automatic verification of these algorithms possible. We apply this idea to several algorithms and present their verification results in the model checker Spin.

We propose a natural generalisation of asynchronous bounded delay (ABD) network models. The commonly used ABD models assume a known bound on message delay. This assumption is often too strict for real-life applications. To this end we introduce a novel probabilistic network model, called asynchronous bounded expected delay (ABE), which requires a known bound on the expected message delay. While the conditions of ABD networks restrict the set of possible executions, in ABE networks all asynchronous executions are possible, but executions with extremely long delays are less probable. The ABE model captures asynchrony that occurs in sensor networks and ad-hoc networks.

In voting, the notion of receipt-freeness has been proposed to express that a voter cannot gain any information to prove that she has voted in a certain way. Receipt-freeness aims to prevent vote buying, even when a voter chooses to renounce her privacy. In this paper, we distinguish various ways that a voter can communicate with the intruder to reduce her privacy and classify them according to their ability to reduce the privacy of a voter. We develop a formal framework combining knowledge reasoning and trace equivalences to formally model voting protocols and define vote privacy for the voters. Our framework is quantitative, in the sense that it defines a measure for the privacy of a voter. Therefore, the framework can precisely measure the level of privacy for a voter for each of the identified privacy classes. The quantification allows our framework to capture receipts that reduce, but not nullify, the privacy of the voter. This has not been identified and dealt with by other formal approaches.

Service composition, which provides a more effective way to combine several single services into a composite service, is a kind of software reuse techniques. However, one of the most important problems is how to perform service composition correctly and effectively so as to produce high-quality source codes for describing the resulted composite service. In this paper, we propose a model-driven method to solve this problem, where UML 2.0 sequence diagrams are extended to model the composition of Web services, extended statecharts are synthesized from sequence diagrams, then the statecharts are further transferred to the input language of a model checker for behavior consistency checking, and finally verified BPEL codes can be generated from improved sequence diagrams. Case studies have been performed to demonstrate the whole process and illustrate the significance of our approach.

The population protocol model has emerged as an elegant paradigm for describing mobile ad hoc networks, consisting of a number of nodes that interact with each other to carry out a computation. One essential property of self-stabilizing population protocols is that all nodes must eventually converge to the correct output value, with respect to all possible initial configurations. It has been shown that fairness constraints play a crucial role in designing population protocols. The Process Analysis Toolkit (PAT) has been developed to perform verifications under different fairness constraints efficiently. In particular, it can handle global fairness, which is required for the correctness of most of population protocols. It is an ideal candidate for automatically verifying population protocols. In this paper, we summarize our latest empirical evaluation of PAT on a set of self-stabilizing population protocols for ring networks. We report one previously unknown bug in a protocol for leader election identified using PAT.

The population protocol model [2] has emerged as an elegant computation paradigm for describing mobile ad hoc networks, consisting of a number of mobile nodes that interact with each other to carry out a computation. The interactions of nodes are subject to a fairness constraint. One essential property of population protocols is that all nodes must eventually converge to the correct output value (or configuration). In this paper, we aim to automatically verify self-stabilizing population protocols for leader election and token circulation in the Spin model checker [8]. We report our verification results and discuss the issue of modeling strong fairness constraints in spin.

In this paper, we present two extensions of the strand space method to model Kerberos V. First, we include time and timestamps to model security protocols with times- tamps: we relate a key to a crack time and combine it with timestamps in order to define a notion of recency. Therefore, we can check replay attacks in this new framework. Second, we extend the classic strand space theory to model protocol mixture. The main idea is to introduce a new relation rarr to model the causal relation between one primary protocol session and one of its following secondary protocol session. Accordingly, we also revisit the definition of unsolicited authentication test. To demonstrate the power of this new theory, we model the Kerberos V protocol, and prove its secrecy and authentication goals. Our framework and the proofs of the example have been mechanized using Isabelle/HOL.

Guttman and Javier Thayer introduced the notion of unsolicited authentication tests, and used it to prove the correctness of security protocols in which a key server authenticate its clients. As an example, they have applied unsolicited authentication tests to prove the authentication goals of the Otway-Rees protocol. However, unsolicited authentication tests seem not to he fully explored in that case study, and the proofs were complicated. In this paper, we revisit the unsolicited authentication tests, and show how to strengthen and apply them in more general cases. To justify our work, we also use this extension to prove all agents' authentication guarantee of the Otway-Rees protocol

Abstract We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2 n . The correctness consists of showing that the sliding window protocol is branching bisimilar to a queue of capacity 2 n . The proof is given entirely on the basis of an axiomatic theory, and has been checked in the theorem prover PVS.