Sanctioning blockchain addresses has become a common regulatory response to malicious activities. However, enforcement on permissionless blockchains remains challenging due to complex transaction flows and sophisticated fund-obfuscation techniques.

Research studies routinely publish summary statistics such as means and standard deviations to promote transparency while protecting participant privacy. Membership inference attacks (MIAs) can exploit these statistics to determine whether a specific individual contributed to a study, posing a risk especially in biomedical and health-related settings. However, existing attacks assume the adversary holds the exact data used in the study, an assumption that rarely holds when data evolves over time. Moreover, prior work has not quantified how much of the reported accuracy stems from true individual identification rather than from group-level traits shared within disease cohorts. We investigate the robustness and interpretability of two standard attacks—the L1-distance test and the log-likelihood ratio (LLR) test—under realistic conditions where the adversary has only noisy, partial, or temporally mismatched data. We derive a theoretical lower bound on inference error that cleanly separates a statistical term governed by pool size and feature dimensionality from a signal term capturing disease-driven shifts. Empirical evaluation on cross-sectional and longitudinal miRNA datasets, validated on Fitbit activity data, confirms that both attacks tolerate substantial noise and missing features, but that real-world temporal drift degrades accuracy far more steeply than synthetic perturbations predict, and that this degradation is individual-specific. We further show that attack accuracy on disease-specific cohorts exceeds that on size-matched random pools by approximately 10%, a separation that grows almost threefold when measured by true-positive rate at 1% false-positive rate. Moreover, individuals sharing disease traits but absent from the study are frequently misclassified as members, indicating that a substantial component of reported accuracy reflects shared condition rather than individual membership.

Recent advancements in hardware-based enclaved execution environments, such as Intel SGX, aim to protect critical model parameters in high-stakes machine learning applications increasingly moving to end-user or cloud environments. However, this also introduces the risk of privileged side-channel attacks, traditionally aimed mainly at cryptographic targets. In this paper, we develop a novel attack methodology that exploits input-dependent memory access patterns in common neural network activation functions to extract hidden model parameters. In several case studies using the SGX-Step attack framework and the Tensorflow Microlite library, we demonstrate complete recovery of first-layer weights and biases, along with partial recovery of deeper layer parameters under specific conditions. Our novel attack technique requires only 20 queries per input per weight to obtain all first-layer weights and biases, with an average absolute error of less than $1 \%$, improving over prior model stealing attacks. Furthermore, a broader ecosystem analysis reveals the widespread use of activation functions with input-dependent memory access patterns in popular machine learning frameworks and maths libraries. Our findings highlight the limitations of deploying confidential models in SGX enclaves and emphasise the need for stricter side-channel validation of machine learning implementations, akin to the vetting efforts applied to secure cryptographic libraries.

With the increasing usage of fake videos in misinformation campaigns, proving the provenance of an edited video becomes critical, in particular, without revealing the original footage. We formalize the notion and security model of proofs of video authenticity and give the first cryptographic video authentication protocol Eva, which supports lossy codecs and arbitrary edits and is proven secure under well-established cryptographic assumptions. Compared to previous cryptographic methods for image authentication, Eva is not only capable of handling significantly larger amounts of data originating from the complex lossy video encoding but also achieves linear prover time, constant RAM usage, and constant proof size with respect to video size. These improvements have optimal theoretic complexity and are enabled by our two new theoretical advancements of integrating lookup arguments with folding-based incrementally verifiable computation (IVC) and compressing IVC proof efficiently, which may be of independent interest. For our implementation of Eva, we then integrate them with the Nova folding scheme, which we call Loua. As for concrete performance, we additionally utilize various optimizations such as tailored circuit design and GPU acceleration to make Eva highly practical: for a 2-minute HD (1280 × 720) video encoded in H.264 at 30 frames per second, Eva generates a 448 B proof in about 2.4 hours on consumer-grade hardware at 2.6 µs per pixel, surpassing state-of-the-art cryptographic image authentication schemes by more than an order of magnitude in terms of prover time and proof size.

The Security Protocol and Data Model (SPDM) establishes device-level trust in hardware platforms through authentication, attestation, and secure session establishment. While prior research has focused on formal analyses and deployment considerations, the impact of implementation-level vulnerabilities, particularly under active physical adversaries, remains largely underexplored. This work presents FaultSpy, the first systematic framework for evaluating SPDM against Fault Injection Attacks (FIAs) and their combination with other prominent attack vectors, such as Man-In-The-Middle (MITM) attacks. Leveraging the fault injection simulation tool, FaultFinder, with our custom SPDM-specific hooks, we uncover nine concrete vulnerabilities spanning both threat models. These include bypassing mutual authentication, suppressing signature generation and verification, downgrading negotiated capabilities, skipping mandatory protocol steps, manipulating key update behavior, transmitting messages intended to be encrypted in plaintext, and extracting session keys. We further validate the feasibility of these attacks through practical voltage glitching experiments on an RP2350 microcontroller. Our findings demonstrate that FIAs-whether in isolation or combined with other attacks-significantly expand the SPDM attack surface, highlighting the need for robust implementation-level countermeasures.

With the increasing scale and complexity of online activities, accountability, as an after-the-fact mechanism, has become an effective complementary approach to ensure system security. Decades of research have delved into the connotation of accountability. They fail, however, to achieve practical accountability of decryption. This paper seeks to address this gap. We consider the scenario where a client (called encryptor, her) encrypts her data and then chooses a delegate (a.k.a. decryptor, him) that stores data for her. If the decryptor initiates an illegitimate decryption on the encrypted data, there is a non-negligible probability that this behavior will be detected, thereby holding the decryptor accountable for his decryption. We make three contributions. First, we review key definitions of accountability known so far. Based on extensive investigations, we formalize new definitions of accountability specifically targeting the decryption process, denoted as accountable decryption, and discuss the (im)possibilities when capturing this concept. We also define the security goals in correspondence. Second, we present a novel Trusted Execution Environment(TEE)-assisted solution aligning with definitions. Instead of fully trusting TEE, we take a further step, making TEE work in the “trust, but verify” model where we trust TEE and use its service, but empower users (i.e., decryptors) to detect the potentially compromised state of TEEs. Third, we implement a full-fledged system and conduct a series of evaluations. The results demonstrate that our solution is efficient. Even in a scenario involving$300,000$log entries, the decryption process concludes in approximately 5.5ms, and malicious decryptors can be identified within 69ms.

Implantable Medical Devices (IMDs) are widely deployed today and often use wireless communication. Establishing a secure communication channel to these devices is challenging in practice. To address this issue, researchers have proposed IMD key exchange protocols, particularly ones that leverage an Out-Of-Band (OOB) channel such as audio, vibration and physiological signals. While these solutions have advantages over traditional key exchange, they are often proposed in an ad-hoc manner and lack a systematic evaluation of their security, usability and deployability properties. In this paper, we provide an in-depth analysis of existing OOB-based solutions for IMDs and, based on our findings, propose a novel IMD key exchange protocol that includes a new class of OOB channel based on human bodily motions. We implement prototypes and validate our designs through a user study (N = 24). The results demonstrate the feasibility of our approach and its unique features, establishing a new direction in the context of IMD security.

User authentication with discrete authenticators, such as YubiKeys, is becoming increasingly popular. The authenticators can be external or on-device. They work using challenge-response protocols and public key cryptography. Multiple accounts can be associated with each authenticator. Compared with other forms of authentication, this approach has advantages in security and usability. There are, however, significant limitations which persist. In particular, if users possess only one authenticator, they lack resilience to loss and malfunction. On the other hand, if they possess multiple authenticators, they lack practical solutions to keep authenticators synchronised. In this paper, we present three solutions which combine the usability of a single authenticator with the resilience of multiple authenticators. We also present two key derivation functions which are used in our solutions. All three solutions maintain core security and privacy properties found in existing systems. Meanwhile, each solution provides additional value in different use cases. The security of our solutions is analysed using ProVerif.

Transparency protocols are protocols whose actions can be publicly monitored by observers (such observers may include regulators, rights advocacy groups, or the general public). The observed actions are typically usages of private keys such as decryptions, and signings. Examples of transparency protocols include certificate transparency, cryptocurrency, transparent decryption, and electronic voting. These protocols usually pose a challenge for automatic verification, because they involve sophisticated data types that have strong properties, such as Merkle trees, that allow compact proofs of data presence and tree extension.We address this challenge by introducing new features in ProVerif, and a methodology for using them. With our methodology, it is possible to describe the data type quite abstractly, using ProVerif axioms, and prove the correctness of the protocol using those axioms as assumptions. Then, in separate steps, one can define one or more concrete implementations of the data type, and again use ProVerif to show that the implementations satisfy the assumptions that were coded as axioms. This helps make compositional proofs, splitting the proof burden into several manageable pieces. We illustrate the methodology and features by providing the first formal verification of the transparent decryption and certificate transparency protocols with a precise modelling of the Merkle tree data structure.

The blockchain-based smart contract lacks privacy, since the contract state and instruction code are exposed to the public. Combining smart-contract execution with Trusted Execution Environments provides an efficient solution, called TEE-assisted smart contracts (TCSC), for protecting the confidentiality of contract states. However, the combination approaches are varied, and a systematic study is absent. Newly released systems may fail to draw upon the experience learned from existing protocols, such as repeating known design mistakes or applying TEE technology in insecure ways. In this paper, we first investigate and categorize existing systems into two types: the layer-one solution and the layer-two solution. Then, we establish an analysis framework to capture their common aspects, covering desired properties (for contract services), threat models, and security considerations (for underlying systems). Based on our taxonomy, we identify their ideal functionalities, and uncover fundamental flaws and challenges in each specification’s design. We believe that this work would provide a guide for the development of TEE-assisted smart contracts, as well as a framework to evaluate future TCSC systems.

This paper proposes Concurrent-Access Obfuscated Store (CAOS), a construction for remote data storage that provides access-pattern obfuscation in a honest-but-curious adversarial model, while allowing for low bandwidth overhead and client storage. Compared to other approaches, the main advantage of CAOS is that it supports concurrent access without a proxy, for multiple read-only clients and a single read-write client. Concurrent access is achieved by letting clients maintain independent maps that describe how the data is stored. Even though the maps might diverge from client to client, the protocol guarantees that clients will always have access to the data. Efficiency and concurrency are achieved at the expense of perfect obfuscation: in CAOS the extent to which access patterns are hidden is determined by the resources allocated to its built-in obfuscation mechanism. To assess this trade-off we provide both a security and a performance analysis of CAOS. We additionally provide a proof-of-concept implementation available at https://github.com/meehien/caos.

We present DECIM, an approach to solve the challenge of detecting endpoint compromise in messaging. DECIM manages and refreshes encryption/decryption keys in an automatic and transparent way: it makes it necessary for uses of the key to be inserted in an append-only log, which the device owner can interrogate in order to detect misuse. We propose a multi-device messaging protocol that exploits our concept to allow users to detect unauthorised usage of their device keys. It is co-designed with a formal model, and we verify its core security property using the Tamarin prover. We present a proof-of-concept implementation providing the main features required for deployment. We find that DECIM messaging is efficient even for millions of users. The methods we introduce are not intended to replace existing methods used to keep keys safe (such as hardware devices, careful procedures, or key refreshment techniques). Rather, our methods provide a useful and effective additional layer of security.

We develop foundations and several constructions for security protocols that can automatically detect, without false positives, if a secret (such as a key or password) has been misused. Such constructions can be used, e.g., to automatically shut down compromised services, or to automatically revoke misused secrets to minimize the effects of compromise. Our threat model includes malicious agents, (temporarily or permanently) compromised agents, and clones.Previous works have studied domain-specific partial solutions to this problem. For example, Google's Certificate Transparency aims to provide infrastructure to detect the misuse of a certificate authority's signing key, logs have been used for detecting endpoint compromise, and protocols have been proposed to detect cloned RFID/smart cards. Contrary to these existing approaches, for which the designs are interwoven with domain-specific considerations and which usually do not enable fully automatic response (i.e., they need human assessment), our approach shows where automatic action is possible. Our results unify, provide design rationales, and suggest improvements for the existing domain-specific solutions.Based on our analysis, we construct several mechanisms for the detection of misuse. Our mechanisms enable automatic response, such as revoking keys or shutting down services, thereby substantially limiting the impact of a compromise.In several case studies, we show how our mechanisms can be used to substantially increase the security guarantees of a wide range of systems, such as web logins, payment systems, or electronic door locks. For example, we propose and formally verify an improved version of Cloudflare's Keyless SSL protocol that enables key misuse detection.

The security of public key validation protocols for web-based applications has recently attracted attention because of weaknesses in the certificate authority model, and consequent attacks. Recent proposals using public logs have succeeded in making certificate management more transparent and verifiable. However, those proposals involve a fixed set of authorities. This means an oligopoly is created. Another problem with current log-based system is their heavy reliance on trusted parties that monitor the logs. We propose a distributed transparent key infrastructure (DTKI), which greatly reduces the oligopoly of service providers and allows verification of the behaviour of trusted parties. In addition, this paper formalises the public log data structure and provides a formal analysis of the security that DTKI guarantees.

Du-Vote is a new remote electronic voting protocol that eliminates the often-required assumption that voters trust general-purpose computers. Trust is distributed in Du-Vote between a simple hardware token issued to the voter, the voter's computer, and a server run by election authorities. Verifiability is guaranteed with high probability even if all these machines are controlled by the adversary, and privacy is guaranteed as long as at least either the voter's computer, or the server and the hardware token, are not controlled by the adversary. The design of the Du-Vote protocol is presented in this paper. A new non-interactive zero-knowledge proof is employed to verify the server's computations. Du-Vote is a step towards tackling the problem of internet voting on user machines that are likely to have malware. We anticipate that the methods of Du-Vote can be used in other applications to find ways of achieving malware tolerance, that is, ways of securely using platforms that are known or suspected to have malware.

Privacy is a core human need, but society sometimes has the requirement to do targeted, proportionate investigations in order to provide security. To reconcile individual privacy and societal security, we explore whether we can have surveillance in a form that is verifiably accountable to citizens. This means that citizens get verifiable proofs of the quantity and nature of the surveillance that actually takes place. In our scheme, governments are held accountable for the extent to which they exercise their surveillance power, and political parties can pledge in election campaigns their intention about reducing (or increasing) this figure. We propose a general idea of accountable escrow to reconciling and balancing the requirements of individual privacy and societal security. We design a balanced crypto system for asynchronous communication (e.g., email). We propose a novel method for escrowing the decryption capability in public-key cryptography. A government can decrypt it in order to conduct targeted surveillance, but doing so necessarily puts records in a public log against which the government is held accountable.

We present StatVerif, which is an extension of the ProVerif process calculus with constructs for explicit state, in order to be able to reason about protocols that manipulate global state. Global state is required by protocols used in hardware devices (such as smart cards and the trusted platform m odule), as well as by protocols involving databases that store persistent information. We provide the operational semantics of StatVerif. We extend the ProVerif compiler to a compiler for StatVerif, which takes processes written in the extended process language and produces Horn clauses. Our compilation is carefully engineered to avoid many false attacks. We prove the correctness of the StatVerif compiler. We illustrate our method on two examples: a small hardware security device and a contract signing protocol. We are able to prove their desired properties automatically.

The balance between coercion-resistance, election verifiability and usability remains unresolved in remote electronic voting despite significant research over the last few years. We propose a change of perspective, replacing the requirement of coercion-resistance with a new requirement of coercion-evidence: there should be public evidence of the amount of coercion that has taken place during a particular execution of the voting system. We provide a formal definition of coercion-evidence that has two parts. Firstly, there should be a coercion-evidence test that can be performed against the bulletin board to accurately determine the degree of coercion that has taken place in any given run. Secondly, we require coercer independence, that is the ability of the voter to follow the protocol without being detected by the coercer. To show how coercion-evidence can be achieved, we propose a new remote voting scheme, Caveat Coercitor, and we prove that it satisfies coercion-evidence. Moreover, Caveat Coercitor makes weaker trust assumptions than other remote voting systems, such as JCJ/Civitas and Helios, and has better usability properties.

Cloud computing means entrusting data to information systems that are managed by external parties on remote servers, in the “cloud”, raising new privacy and confidentiality concerns. We propose a general technique for designing cloud services that allows the cloud to see only encrypted data, while still facilitating some data-dependent computations. The technique is based on key translations and mixes in web browsers. We focus on a particular kind of software-as-a-service, namely, services that support applications, evaluations and decisions. Such services include job application management, public tender management (e.g., for civil construction), and conference management. We identify the specific security and privacy risks that existing systems pose. We propose a protocol that addresses them, and forms the basis of a system that offers strong security and privacy guarantees. We express the protocol and its properties in the language of ProVerif, and prove that it does provide the intended properties. We describe an implementation of a particular instance of the protocol called ConfiChair, which is geared to the evaluation of papers submitted to conferences.

Mobile telephony equipment is daily carried by billions of subscribers everywhere they go. Avoiding linkability of subscribers by third parties, and protecting the privacy of those subscribers is one of the goals of mobile telecommunication protocols. We use formal methods to model and analyse the security properties of 3G protocols. We expose two novel threats to the user privacy in 3G telephony systems, which make it possible to trace and identify mobile telephony subscribers, and we demonstrate the feasibility of a low cost implementation of these attacks. We propose fixes to these privacy issues, which also take into account and solve other privacy attacks known from the literature. We successfully prove that our privacy-friendly fixes satisfy the desired unlinkability and anonymity properties using the automatic verification tool ProVerif.

We present StatVerif, which is an extension the ProVerif process calculus with constructs for explicit state, in order to be able to reason about protocols that manipulate global state. Global state is required by protocols used in hardware devices (such as smart cards and the TPM), as well as by protocols involving databases that store persistent information. We provide the operational semantics of StatVerif. We extend the ProVerif compiler to a compiler for StatVerif: it takes processes written in the extended process language, and produces Horn clauses. Our compilation is carefully engineered to avoid many false attacks. We prove the correctness of the StatVerif compiler. We illustrate our method on two examples: a small hardware security device, and a contract signing protocol. We are able to prove their desired properties automatically.

We present a Horn-clause-based framework for analysing security protocols that use \emph{platform configuration registers} (PCRs), which are registers for maintaining state inside the Trusted Platform Module (TPM). In our model, the PCR state space is unbounded, and our experience shows that a na\"\i ve analysis using ProVerif or SPASS does not terminate. To address this, we extract a set of instances of the Horn clauses of our model, for which ProVerif does terminate on our examples. We prove the soundness of this extraction process: no attacks are lost, that is, any query derivable in the more general set of clauses is also derivable from the extracted instances. The effectiveness of our framework is demonstrated in two case studies: a simplified version of Microsoft Bit locker, and a digital envelope protocol that allows a user to choose whether to perform a decryption, or to verifiably renounce the ability to perform the decryption.

An attacker that can identify messages as coming from the same source, can use this information to build up a picture of targets' behaviour, and so, threaten their privacy. In response to this danger, unlinkable protocols aim to make it impossible for a third party to identify two runs of a protocol as coming from the same device. We present a framework for analysing unlinkability and anonymity in the applied pi calculus. We show that unlinkability and anonymity are complementary properties; one does not imply the other. Using our framework we show that the French RFID e-passport preserves anonymity but it is linkable therefore anyone carrying a French e-passport can be physically traced.

We propose a symbolic semantics for the finite applied pi calculus. The applied pi calculus is a variant of the pi calculus with extensions for modelling cryptographic protocols. By treating inputs symbolically, our semantics avoids potentially infinite branching of execution trees due to inputs fr om the environment. Correctness is maintained by associating with each process a set of constraints on terms. We define a symbolic labelled bisimulation relation, which is shown to be sound but not complete with respect to standard bisimulation. We explore the lack of completeness and demonstrate that the symbolic bisimulation relation is sufficient for many practical examples. This work is an important step towards automation of observational equivalence for the finite applied pi calculus, e.g. for verification of anonymity or strong secrecy properties.

Anonymity with identity escrowattempts to allow users of an online service to remain anonymous, while providing the possibility that the service owner can break the anonymity in exceptional circumstances, such as to assist in a criminal investigation. In the article, we propose an identity escrow protocol that distributes user identity among several escrow agents. The main feature of our scheme is it is based on standard encryption algorithms and it provides user anonymity even if all but one escrow holders are dishonest acting in a coalition. We also present analysis of the anonymity property of our protocol in the applied pi-calculus. We review a related scheme by Marshall and Molina-Jiminez [2003] that aimed to achieve goals similar to ours, and show that their scheme suffers from serious weaknesses.

Peer-to-peer (P2P) based marketplaces have a number of advantages over traditional centralized systems (such as eBay). Peers form a distributed hash table and store sale offers for other peers. A key problem in such a system is ensuring that the peers store and report all sale offers fairly, and do not for instance favor their own offers. We give a solution to this problem based on trusted computing, but unlike other approaches we do not measure and restrict all firmware and software running on a peer. Instead, we tie offers to monotonic counters in such a way that any attempt to not report an offer, or report it falsely, will be detected.

Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. We study three privacy-type properties of electronic voting protocols: in increasing order of strength, they are vote-privacy, receipt-freeness and coercion-resistance. We use the applied pi calculus, a formalism well adapted to modelling such protocols, which has the advantages of being based on well-understood concepts. The privacy-type properties are expressed using observational equivalence and we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies vote-privacy. We illustrate our definitions on three electronic voting protocols from the literature. Ideally, these three properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy receipt-freeness or coercion-resistance may not do so in the presence of corrupt officials. Our model and definitions allow us to specify and easily change which authorities are supposed to be trustworthy.

We investigate the composition of protocols that share a common secret. This situation arises when users employ the same password on different services. More precisely we study whether resistance against guessing attacks composes when the same password is used. We model guessing attacks using a common definition based on static equivalence in a cryptographic process calculus close to the applied pi calculus. We show that resistance against guessing attacks composes in the presence of a passive attacker. However, composition does not preserve resistance against guessing attacks for an active attacker. We therefore propose a simple syntactic criterion under which we show this composition to hold. Finally, we present a protocol transformation that ensures this syntactic criterion and preserves resistance against guessing attacks.

We present a framework for evaluating and generating access control policies.The framework contains a modelling formalism called RW, which is supported by a model checking tool.RW is designed for modelling access control policies, and verifying their properties.The RW language is very expressive, allowing us to model complex access conditions which can depend on data values, other permissions, and agent roles.A property expresses the capability of a coalition of agents to achieve a goal, which may include reading and overwriting certain information.Given a model built based on a policy and a property, the model-checking algorithm decides whether the goal defined by the property is achievable by the coalition within the permissions the policy provides.In the case that the goal is achievable, the algorithm outputs strategies which may be used by the coalition to achieve the goal.The unachievability of legitimate goals may suggest that the policy does not provide the users enough permissions to carry out their actions.The achievability of malicious goals may reveal certain security holes in the policy.When malicious goals are achievable, the resulting strategies help to provide clues on amending the policy.The tool implements the algorithm and thus performs the RW model-checking.It can also convert a policy written in the RW language into a policy file in XACML.An access control system can then be built on the converted policy file.

research-article Free Access Share on Minimal refinements of specifications in model and termporal logics Authors: Nikos Gorogiannis School of Computing, University of the West of England, BS 16 1QY, Bristol, UK School of Computing, University of the West of England, BS 16 1QY, Bristol, UKView Profile , Mark Ryan School of Computer Science, University of Birmingham, B15 2TT, Birmingham, UK School of Computer Science, University of Birmingham, B15 2TT, Birmingham, UKView Profile Authors Info & Claims Formal Aspects of ComputingVolume 19Issue 1pp 35–62https://doi.org/10.1007/s00165-006-0014-3Published:01 March 2007Publication History 0citation13DownloadsMetricsTotal Citations0Total Downloads13Last 12 Months8Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

In both scenarios we seek to produce a refinement of a system.Refinement (see e.g.[AL91]) can be viewed as behaviour-containment; if A and B are two systems, then A refines B iff behaviours(A) ⊆ behaviours(B).We will be using transition systems to represent designs of systems (and from now on we will use the terms system and model interchangeably), and as such, an appropriate notion of behaviour is the computation tree.Correspondingly, the set of behaviours exhibited by a transition system is the set of computation trees that results from the unravelling of the transition system.More specific definitions will be given in the following section.In both examples, a refinement of a design is sought.However, refining a system yields an implementation, or a more 'concrete' version of it, but not necessarily a useful one: depending on the formalism used, it is frequently the case that trivial models exist that refine almost every other model.For example, in the case of the database access control system, it is true that an empty transition system does not allow any behaviours at all and, therefore, refines the original one; it is hardly a useful one though.In other words, we are interested in refining the original model but only so much as is necessary in order to satisfy a given guiding property.In this way, behaviours of the original system are only sacrificed if necessary.Thus, instead of just looking for designs that refine the initial one and satisfy the new requirement, we will use refinement to order the designs.We are led, then, to the concept of minimal refinement.Minimal refinement can be used whenever the designer has a model of a system that already circumscribes the allowed behaviours of the system.Then, a new property can be applied and a new design obtained, that satisfies the new requirement, refines the initial design and exhibits as many of its behaviours as possible.A corollary of this is that by using minimal refinement we get automatic preservation of safety properties.The contributions of this paper lie, firstly, in the introduction of the notion of minimal refinement as a method for the stepwise addition of requirements in a model.Secondly, we investigate and prove results concerning several issues around minimal refinement such as the soundness and decidability of algorithms for computing minimal refinements.In what follows we will define this process and study its theoretical and applied aspects.We will focus on representations of designs based on transition systems, and on modal and temporal logics as languages for expressing requirements.We begin by introducing the theoretical background in Sect. 2.Then, we will proceed to formalise these intuitions and define minimal refinement in a precise way in Sect.3. In the same section, the problems that arise from our definition are discussed, and specific technical questions aiming at resolving those problems are specified.These questions are investigated in the context of modal logic in Sect. 4. In the aim of addressing expressiveness issues related to modal logic, we further develop the investigation of these questions into the realm of temporal logic in Sect. 5. Finally, we conclude and summarise the possible avenues for extending the work presented in this paper, in Sect.6.The definitions behind minimal refinement and part of the results presented in Sect. 4 have appeared in [GR02].The results presented in Sect. 5 have appeared in [Gor03]. Preliminaries General backgroundBefore discussing specific logics, we will approach the subject from a higher level.Therefore, let L and M be sets, corresponding to the set of formulae and the set of models of a logic.Let, also, | ⊆ M × L be a satisfaction relation.The class of models that satisfies a formula φ will be denoted by mod(φ).Let ⊆ M × M be a preorder (i.e., a transitive and reflexive relation) on models.The strict counterpart of , denoted by < is defined by the condition M < N iff M N and N M. Given a set S ⊆ M, the minimisation operator is defined in the usual way, min (S) {M ∈ S | ∀ N ∈ S, N < M}.As noted in the introduction, we will be looking at an operation of the form of min (mod(φ)).This operation resembles one often found in the areas known as theory (or belief) change (see, e.g., [Gro88, Dal88, KM89, KM91]) and non-monotonic reasoning (e.g, [KLM90, BMP97, BEF93]), among others.The shared intuition is that, when given a property φ in some logic, instead of selecting all the structures that satisfy φ (mod(φ)) we employ some extra-logical information and treat some models inside mod(φ) in a preferential way.This information takes frequently the form of a relation over models and is usually called a preference relation.Minimal refinements of specifications in modal and temporal logics 419 Modal logicIn Sect.4, we will generally work with a finite set A of propositional variables.The modal language L K of the logic K m on A with m modalities is defined inductively; if p ∈ A then p ∈ L K ; if φ and ψ are in L K then so are ¬ φ and φ ∧ ψ; if φ ∈ L K then 3 i φ ∈ L K for all 1 i m.The usual propositional abbreviations apply as well as the modal 2 i ≡ ¬ 3 i ¬ .The axiomatisation of K m follows. P.Any propositional tautology is an axiom.K. Any formula of the form 2 i (φ → ψ) → (2 i φ → 2 i ψ) with 1 i m is an axiom.Its rules of inference are: MP.Modus ponens: if φ and φ → ψ, then ψ.Nec.Necessitation: if φ, then 2 i φ, for all 1 i m.The logic of K m is defined to be the smallest subset of L K that contains all the instances of the above axioms and is closed under the two rules of inference.The fact that a formula φ ∈ L K is in is denoted by φ.If T is a set of sentences and φ a sentence, then φ is deducible from T , written T φ, if there exists a number n 0 and sentences ψ 1 , . . ., ψ n ∈ T such that ψ 1 ∧ • • • ∧ ψ n → φ.The set T is called consistent if T ⊥ and inconsistent otherwise.The most popular semantics for modal logics is through Kripke models.

In this paper we formally study important properties of electronic voting protocols. In particular we are interested in coercion-resistance and receipt-freeness. Intuitively, an election protocol is coercion-resistant if a voter A cannot prove to a potential coercer C that she voted in a particular way. We assume that A cooperates with C in an interactive fashion. Receipt-freeness is a weaker property, for which we assume that A and C cannot interact during the protocol: to break receipt-freeness, A later provides evidence (the receipt) of how she voted. While receipt-freeness can be expressed using observational equivalence from the applied pi calculus, we need to introduce a new relation to capture coercion-resistance. Our formalization of coercion-resistance and receipt-freeness are quite different. Nevertheless, we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies privacy, the basic anonymity property of voting protocols, as defined in previous work. Finally we illustrate the definitions on a simplified version of the Lee et al. voting protocol

A multi-party contract signing protocol allows a set of participants to exchange messages with each other with a view to arriving in a state in which each of them has a pre-agreed contract text signed by all the others. Such a protocol was introduced by Garay and MacKenzie in 1999; it consists of a main protocol and a sub-protocol involving a trusted party. Their protocol was shown to have a flaw by Chadha, Kremer and Scedrov in CSFW 2004. Those authors also presented a fix - a revised sub-protocol for the trusted party. In our work, we show an attack on the revised protocol for any number n > 4 of signers. Furthermore, we generalise our attack to show that the message exchange structure of Garay and MacKenzie's main protocol is flawed: whatever the trusted party does will result in unfairness for some signer. This means that it is impossible to define a trusted party protocol for Garay and MacKenzie's main protocol; we call this "resolve-impossibility".

Software systems inevitably require update and revision during their lifetime. The concept of features is often used to model system update: a feature is a unit of functionality which may be integrated into a base system. Possible features of an email client program include: spam filtering; absence messages; selective forwarding; and encryption. In our work, we use AI techniques to understand the operation of feature integration more clearly. In particular, we have taken SMV (symbolic model verifier) feature integrator (SFI), a tool which automates feature integration on systems described using the model checker SMV. Then we have taken update which is an operation of theory change, closely related to belief revision, and defined over propositional logic. We formulate and prove a theorem stating that SFI feature integration is an update operation.

We provide a symbolic algorithm for synthesizing winning strategies in Alternating Time Temporal Logic. ATL has game semantics, which makes it suitable for modeling open systems where coalitions of agents work together to achieve their goals. A typical use of the algorithm would begin with a highly non-deterministic set of agents, A, for which we wish to synthesize behavior. These may be composed with a set of opponent agents, which provide an environment. The desired behavior is then written in>-LTL, and a strategy for A to implement this is synthesized. If A implements this strategy, then the system will be guaranteed to satisfy the desired property. The algorithm presented here is part of a work in progress and updates can be found at http://www.cs.bham.ac.uk/ /spl sim/ ath/atl/spl I.bar/synthesis.

The paper is a theoretical study of a generalization of the lexicographic rule for combining ordering relations. We define the concept of priority operator: a priority operator maps a family of relations to a single relation which represents their lexicographic combination according to a certain priority on the family of relations. We present four kinds of results. • We show that the lexicographic rule is the only way of combining preference relations which satisfies natural conditions (similar to those proposed by Arrow). • We show in what circumstances the lexicographic rule propagates various conditions on preference relations, thus extending Grosof's results. • We give necessary and sufficient conditions on the priority relation to determine various relationships between combinations of preferences. • We give an algebraic treatment of this form of generalized prioritization. Two operators, called but and on the other hand, are sufficient to express any prioritization. We present a complete equational axiomatization of these two operators. These results can be applied in the theory of social choice (a branch of economics), in non‐monotonic reasoning (a branch of artificial intelligence), and more generally wherever relations have to be combined.

The semantic framework for the modal logic of knowledge due to Halpern and Moses provides a way to ascribe knowlegde to agents in distributed and multiagent systems. In this paper we study two special cases of this framework:full systemsandhypercubes. Both model static situtations in which no agents has any information about another agent's state. Full systems and hypercubes are an appropriate model for the initial configurations of many systems of interest. We establish a correspondence between full systems and hypercube systems and certain classes of Kripke frames. We show that these classes of systems correspond to the same logic. Moreover, this logic is also the same as that generated by the larger class ofweakly directed frames. We provide a sound and complete axiomatization, S5WDnof this logic, and study its computational complexity. Finally, we show that under certain natural assumptions, in a model where knowledge evolves over time, S5WDncharacteristics the properties of knowledge not just at the initial configuration, but also at all later configurations. In this particular, this holds forhomogeneous broadcast systems,which capture settings in which agents are intially ignorant of each others local states, operate synchronously, have perfect recall, and can communicate only by broadcasting.

A formalism is motivated and described for representing defaults in specifications. The formalism is called ordered theory presentations. The ability to represent defaults narrows the gap between a customer's initial requirements and a formal specification, and supports reuse on both a small and a large scale. Issues are illustrated throughout reference to the lift example. The application of the formalism to specification revision is considered.>

Starting from a logic which specifies how to make deductions from a set of sentences (a flat theory), a way to generalize this to a partially ordered bag of sentences (a structured theory) is given. The partial order is used to resolve conflicts. If phi occurs below psi , then psi is accepted only insofar as it does not conflict with phi . The study starts with a language L, a set of interpretations M and a satisfaction relation. The key idea is to define, for each structured theory, a preorder on interpretations. Models of the structured theory are defined to be maximal interpretations in the ordering. A revision operator that takes a structured theory and a sentence and returns a structured theory is defined. The consequence relation has the properties of weak monotonicity, weak cut, and weak reflexivity with respect to this operator, but fails their strong counterparts.>