Logic for information security
19–22 January 2010
University of Hyderabad, Gachibowli, India
University of Hyderabad, Gachibowli, India
The workshop Logic for information security is part of ISLA 2010, the third Indian School on Logic and its Applications. The workshop focuses on logical analysis of protocols for secure communication, with a variety of topics, including process calculi for modelling and analysis of protocols, aspects of system security, modal logics for analysis of protocols, combinatorial mathematics for bit exchange, and zero knowledge protocols.
The workshop happens in the first week of ISLA 2010, from 19 January till 22 January, 2010. The following speakers will enthrall the audience.
Cryptographic protocols are a means to attain secure communication over an insecure network which rely on mathematical primitives like encryption and digital signatures to achieve this objective. But even if cryptography is secure, protocols may have logical flaws that allow a malicious agent to learn secrets that it ought not to. To model such “logical attacks” and check protocols for absence of these, the standard model used is the one proposed by Dolev and Yao. This model forms the basis of many automatic verification tools for cryptographic protocols that are used in practice.
In recent times, researchers have shown an interest in extending the reach of protocol verification tools to a wide variety of cryptographic protocols, which use sophisticated primitives like zero knowledge proofs, blind signatures, etc. There is a need to rework elements of the Dolev-Yao theory to cover these kinds of protocols. In this talk, we will look at a candidate extension of the Dolev-Yao theory to model protocols using zero-knowledge proofs.
In the mid-19th century, Thomas Kirkman and Jacob Steiner gave birth to what later became known as design theory, a subdiscipline of combinatorial mathematics. Tools and techniques from that area can be used to design unconditionally secure (communicative) protocols. The epistemic logician can also focus on the epistemic properties of such protocols, or reformulate their specifications (such as security requirements) in such terms. Individual, common and distributed knowledge all play a role. Following original contributions from the 1980s onward by Winkler, Fischer, Wright and others, we focus on the case of computationally unlimited agents using card deals. Given various agents or players, two among them (sender and receiver, say, but note that they both send and receive) may wish to communicate a secret. We present some results for the restricted case where secrets concern card ownership, and for the general case where any secret bit can be exchanged by means of such card deals.
Protocols for secure archival storage are becoming increasingly important as the use of digital storage for sensitive documents is gaining wider practice. Wong et al. combined verifiable secret sharing with proactive secret sharing without reconstruction and proposed a verifiable secret redistribution protocol for long term storage. However, their protocol requires that each of the receivers is honest during redistribution. We proposed an extension to their protocol wherein we relaxed the requirement that all the recipients should be honest to the condition that only a simple majority amongst the recipients need to be honest during the re(distribution) processes. Further, both of these protocols make use of Feldman’s approach for achieving integrity during the (re)distribution processes. In this talk, we present a revised version of our earlier protocol, and its adaptation to incorporate Pedersen's approach instead of Feldman’s thereby achieving information theoretic secrecy while retaining integrity guarantees.
I will discuss a framework for modelling of multi-agent systems where agents’ actions effect information exchange, by means of reading and writing values of system variables assigned special rights of access. This framework combines and extends features of several well-studied models including interpreted systems, concurrent game structures, and reactive modules. I will argue that this framework can adequately deal with various situations arising in information security, and will present a logical formalism for specification of, and reasoning about, information security issues in multi-agent systems. This talk is based on a work in progress.
We propose a general, formal definition of the concept of malware (malicious software) as a single sentence in the language of a certain modal logic. Our definition is general thanks to its abstract formulation, which, being abstract, is independent of—but nonetheless generally applicable to—the manifold concrete manifestations of malware. From our formulation of malware, we derive equally general and formal definitions of benware (benign software), anti-malware (“antibodies” against malware), and medware (medical software or “medicine” for affected software). We provide theoretical tools and practical techniques for the detection, comparison, and classification of malware and its derivatives. Our general defining principle is causation of (in)correctness.
This is joint work with Julian C Bradfield.
Keywords. malware (Trojans, viruses, worms, rootkits, botnets, etc.); benware; anti-malware; medware; applied modal logic; formal software-systems engineering.
Process calculi were developed for specifying and reasoning about systems of concurrently executing processes. Abadi and Gordon developed a variation on Robin Milner’s Pi calculus, called the Spi calculus, for specifying protocols (assuming ideal cryptographic systems) and reasoning about secrecy and authentication. Further extensions led to the development of the Applied Pi Calculus by Abadi and Fournet. I will discuss how process calculi can be used to specify simple protocols and reason about their security properties in terms of the operational semantics of process calculi.
We present a survey of programming language techniques to specify and enforce information flow policies. The programming language techniques are especially interesting because the standard security mechanisms (like access control models, firewalls, antivirus software) are unsatisfactory for protecting confidential information in the emerging, large-scale networked information systems. Military, medical, and financial information systems, as well as web based services such as mail, shopping and business-to-business transactions are applications that create serious privacy questions for which there are no good answers at present.
It is observed that the definition of noninterference is too strong for many scenarios. We present two approaches which weaken the noninterference definition of security: quantifying interference by Clark et al and abstract noninterference by Giacobazzi et al.
Typically, Dolev-Yao theories are treated as first-order theories with constraints and protocols as extensions of such theories. While this has proved useful for analysing security protocols for potential attacks, such an approach tends to hide the logical reasoning underlying the Dolev-Yao model. On the other hand, non-cryptographic analyses such as that of the Russian Cards problem explicate the underlying logic by treating information hiding as disjunctions. However, they miss the power of cryptographic primitives which can be seen as the logical equivalents of infinite disjunctions. Thus, it is interesting to study an extension of the dolev yao model with finite disjunctions, thus making a connection with the logical approaches mentioned above. We discuss such a proposal, and show its connections to zero-knowledge proofs.
The work presented here is joint with A Baskar (CMI) and S P Suresh (CMI).
Hans van Ditmarsch (University of Seville)
S P Suresh (Chennai Mathematical Institute)