Search

Abstract: This paper continues the program initiated in [5], towards a derivation system for security protocols. The general idea is that complex protocols can be formally derived, starting from basic security components, using a sequence of refinements and transformations, just like logical proofs are derived starting from axioms, using proof rules and transformations. The claim is that in practice, many protocols are already derived in such a way, but informally. Capturing this practice in a suitable formalism turns out to be a considerable task. The present paper proposes rules for composing security protocols from given security components. In general, security protocols are, of course, not compositional: information revealed by one may interfere with the security of the other. However, annotating protocol steps by pre- and post-conditions, allows secure sequential composition. Establishing that protocol components satisfy each other’s invariants allows more general forms of composition, ensuring that the individually secure sub-protocols will not interact insecurely in the composite protocol. The applicability of the method is demonstrated on modular derivations of two standard protocols, together with their simple security properties. [Copyright &y& Elsevier]

Abstract: In [19], the authors presented a type-theoretic approach to the verification of security protocols. In this approach, a universal type system is proposed to capture in a finite way all the possible computations (internal actions or protocol instrumentations) that could be performed by a smart malicious intruder. This reduces the verification of cryptographic protocols to a typing problem where types are attack scenarios. In this paper, we recall this type system and we prove its completeness i.e. if the intruder can learn a message from a given protocol instrumentation, then this message could be infered from the type system. A significant result of this paper is the presentation of a new transformation that allows us to abstract a non-terminating type inference system into a terminating deductive proof system. We demonstrate how these results could be used to establish the security of cryptographic protocols from the secrecy standpoint. Finally, the usefulness and the efficiency of the whole approach is illustrated by proving the correctness of a new version of the Needham-Shoreder protocol with respect to the secrecy property. [Copyright &y& Elsevier]

Abstract: This paper serves to bring three independent but important areas of computer science to a common meeting point: Formal Concept Analysis (FCA), Chu Spaces, and Domain Theory (DT). Each area is given a perspective or reformulation that is conducive to the flow of ideas and to the exploration of cross-disciplinary connections. Among other results, we show that the notion of states in Scott’s information system corresponds precisely to that of formal concepts in FCA with respect to all finite Chu spaces, and the entailment relation corresponds to “association rules”. [Copyright &y& Elsevier]

Abstract: Language-based approaches to information security have led to the development of security type systems that permit the programmer to describe confidentiality policies on data. Security type systems are usually intended to enforce noninterference, a property that requires that high-security information not affect low-security computation. However, in practice, noninterference is often too restrictive—the desired policy does permit some information leakage. To compensate for the strictness of noninterference, practical approaches include some mechanism for declassifying high-security information. But such declassification is potentially dangerous, and its use should be restricted to prevent unintended information leaks. Zdancewic and Myers previously introduced the notion of robust declassification in an attempt to capture the desired restrictions on declassification, but that work did not propose a method for determining when a program satisfies the robust declassification condition. This paper motivates robust declassification and shows that a simple change to a security type system can enforce it. The idea is to extend the lattice of security labels to include integrity constraints as well as confidentiality constraints and then require that the decision to perform a declassification have high integrity. [Copyright &y& Elsevier]

Abstract: The superficial similarity between the Chu construction and the Hyland-Tan double glueing construction G has been observed widely. This paper establishes a more formal mathematical relationship between the two. We show that double glueing on relations subsumes the Chu construction on sets: we present a full monoidal embedding of the category chu(Set, K) of biextensional Chu spaces over Κ into G(Rel K ), and a full monoidal embedding of the category Chu(Set, K) of Chu spaces over Κ into IG(Rel K ), where we define IG, the intensional double glueing construction, by substituting multisets for sets in G. We define a biextensional collapse from IG to G which extends the familiar notion on Chu spaces. This yields a new interpretation of the monic specialisation implicit in G as a form of biextensionality. [Copyright &y& Elsevier]

Abstract: In this paper we use the concept of resource cumulation to model various forms of computation. The space of cumulations (called a cumulator) is simply represented as a five tuple consisting of a well-founded partial order, a monoid and a volume function. The volume function is introduced to simplify reasoning about limit points and other topological properties. A specification command is a set of cumulations. Typical phenomena of concurrency such as reactiveness, safety and liveness, fairness, real time and branching time naturally arise from the model. In order to support a programming theory, we introduce a specification language that incorporates sequentiality, nondeterminism, simple parallelism, negation and general recursions. A new fixpoint technique is used to model general recursions. The language is applied to the case study on CSP, which becomes a special model of cumulative computing with a combination of four resource cumulators of alphabet, termination, trace and refusal. All laws of cumulative computing are also valid for CSP and the generalization from CSP to Timed CSP can be achieved by simply combining the four cumulators with real time. Loops whose bodies may take zero time can then be modeled more satisfactorily. [Copyright &y& Elsevier]