Superficial scald,a functional disorder of stored apples X. Control of α-farnesene autoxidation

A wide range of antioxidants (amine, phenolic and one sulphur-containing) were all found to inhibit the autoxidation of α-farnesene in vitro. Some were somewhat more effective than others but no class showed any marked superiority. When added to apples as a dip or by injection, only amine type antioxidants inhibited the autoxidation of α-farnesene in vitro. Phenolic antioxidants were ineffective and some acted as pro-oxidants, notably α-tocopherol. In all instances the severity of superficial scald was proportional to the extent of α-farnesene oxidation.     

A Guided Tour through some Extensions of the Event Calculus

Kowalski and Sergot's Event Calculus (EC) is a simple temporal formalism that, given a set of event occurrences, derives the maximal validity intervals (MVIs) over which properties initiated or terminated by these events hold. In this paper, we conduct a systematic analysis of EC by which we gain a better understanding of this formalism and determine ways of augmenting its expressive power. The keystone of this endeavor is the definition of an extendible formal specification of its functionalities. This formalization has the effects of casting determination of MVIs as a model checking problem, of setting the ground for studying and comparing the expressiveness and complexity of various extensions of EC, and of establishing a semantic reference against which to verify the soundness and completeness of implementations. We extend the range of queries accepted by EC, which is limited to Boolean combinations of MVI verification or computation requests, to support arbitrary quantification over events and modal queries. We also admit specifications based on preconditions. We demonstrate the added expressive power by encoding a number of diagnosis problems. Moreover, we provide a systematic comparison of the expressiveness and complexity of the various extended event calculi against each other. Finally, we propose a declarative encoding of these enriched event calculi in the logic programming language λProlog and prove the soundness and completeness of the resulting logic programs.     

Relating state-based and process-based concurrency through linear logic (full-version)

This paper has the purpose of reviewing some of the established relationships between logic and concurrency, and of exploring new ones.Concurrent and distributed systems are notoriously hard to get right. Therefore, following an approach that has proved highly beneficial for sequential programs, much effort has been invested in tracing the foundations of concurrency in logic. The starting points of such investigations have been various idealized languages of concurrent and distributed programming, in particular the well established state-transformation model inspired by Petri nets and multiset rewriting, and the prolific process-based models such as the π-calculus and other process algebras. In nearly all cases, the target of these investigations has been linear logic, a formal language that supports a view of formulas as consumable resources. In the first part of this paper, we review some of these interpretations of concurrent languages into linear logic and observe that, possibly modulo duality, they invariably target a small semantic fragment of linear logic that we call LV^obs.In the second part of the paper, we propose a new approach to understanding concurrent and distributed programming as a manifestation of logic, which yields a language that merges those two main paradigms of concurrency. Specifically, we present a new semantics for multiset rewriting founded on an alternative view of linear logic and specifically LV^obs. The resulting interpretation is extended with a majority of linear connectives into the language of ω-multisets. This interpretation drops the distinction between multiset elements and rewrite rules, and considerably enriches the expressive power of standard multiset rewriting with embedded rules, choice, replication, and more. Derivations are now primarily viewed as open objects, and are closed only to examine intermediate rewriting states. The resulting language can also be interpreted as a process algebra. For example, a simple translation maps process constructors of the asynchronous π-calculus to rewrite operators. The language of ω-multisets forms the basis for the security protocol specification language MSR 3. With relations to both multiset rewriting and process algebra, it supports specifications that are process-based, state-based, or of a mixed nature, with the potential of combining verification techniques from both worlds. Additionally, its logical underpinning makes it an ideal common ground for systematically comparing protocol specification languages.     

One Picture Is Worth a Dozen Connectives: A Fault-Tree Representation of NPATRL Security Requirements

In this paper, we show how we can increase the ease of reading and writing security requirements for cryptographic protocols at the Dolev-Yao level of abstraction by developing a visual language based on fault trees. We develop such semantics for a subset of NRL protocol analyzer temporal requirements language (NPATRL), a temporal language used for expressing safety requirements for cryptographic protocols, and show that the subset is sound and complete with respect to the semantics. We also show how the fault trees can be used to improve the presentation of some specifications that we developed in our analysis of the group domain of interpretation (GDOI) protocol. Other examples involve a property of Kerberos 5 and a visual account of the requirements in Lowe's authentication hierarchy.     

Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types

This paper presents a shallow and efficient embedding of the security protocol specification language MSR into an extension of rewriting logic with dependent types. The latter is an instance of the open calculus of constructions which integrates key concepts from equational logic, rewriting logic, and type theory. MSR is based on a form of first-order multiset rewriting extended with existential name generation and a flexible type infrastructure centered on dependent types with subsorting. The encoding presented in this paper has served as the basis for the implementation of an MSR specification and analysis environment using the first-order rewriting engine Maude.     

Cryptographically sound security proofs for basic and public-key Kerberos

We present a computational analysis of basic Kerberos with and without its public-key extension PKINIT in which we consider authentication and key secrecy properties. Our proofs rely on the Dolev–Yao style model of Backes, Pfitzmann, and Waidner, which allows for mapping results obtained symbolically within this model to cryptographically sound proofs if certain assumptions are met. This work was the first verification at the computational level of such a complex fragment of an industrial protocol. By considering a recently fixed version of PKINIT, we extend symbolic correctness results we previously attained in the Dolev–Yao model to cryptographically sound results in the computational model.