No. 4 (2002)
Published:
2002-12-30
ARTICLES FROM THIS ISSUE
-
Is it possible to decide whether a cryptographic protocol is secure or not?
Abstract
We consider the so called ``cryptographic protocols`` whose aim is to ensure some security properties when communication channels are not reliable. Such protocols usually rely on cryptographic primitives. Even if it is assumed that the cryptographic primitives are perfect, the security goals may not be achieved: the protocol itself may have weaknesses which can be exploited by an attacker. We survey recent work on decision techniques for the cryptographic protocol analysis.
-
CAPSL and MuCAPSL
Abstract
Secure communication generally begins with a~connection establishment phase in which messages are exchanged by client and server protocol software to generate, share, and use secret data or keys. This message exchange is referred to as an authentication or key distribution cryptographic protocol. CAPSL is a formal language for specifying cryptographic protocols. It is also useful for addressing the correctness of the protocols on an abstract level, rather than the strength of the underlying cryptographic algorithms. We outline the design principles of CAPSL and its integrated specification and analysis environment. Protocols for secure group management are essential in applications that are concerned with confidential authenticated communication among coalition members, authenticated group decisions, or the secure administration of group membership and access control. We will also discuss our progress on designing a new extension of CAPSL for multicast protocols, called MuCAPSL.
-
Process calculi and the verification of security protocols
Abstract
Recently there has been much interest towards using formal methods in the analysis of security protocols. Some recent approaches take advantage of concepts and techniques from the field of process calculi. Process calculi can be given a formal yet simple semantics, which permits rigorous definitions of such concepts as ``attacker``, ``secrecy`` and ``authentication``. This feature has led to the development of solid reasoning methods and verification techniques, a few of which we outline in this paper.
-
Asymmetric cryptography and practical security
Abstract
Since the appearance of public-key cryptography in Diffie-Hellman seminal paper, many schemes have been proposed, but many have been broken. Indeed, for many people, the simple fact that a cryptographic algorithm withstands cryptanalytic attacks for several years is considered as a kind of validation. But some schemes took a long time before being widely studied, and maybe thereafter being broken. A~much more convincing line of research has tried to provide ``provable`` security for cryptographic protocols, in a complexity theory sense: if one can break the cryptographic protocol, one can efficiently solve the underlying problem. Unfortunately, very few practical schemes can be proven in this so-called ``standard model`` because such a security level rarely meets with efficiency. A convenient but recent way to achieve some kind of validation of efficient schemes has been to identify some concrete cryptographic objects with ideal random ones: hash functions are considered as behaving like random functions, in the so-called ``random oracle model``, block ciphers are assumed to provide perfectly independent and random permutations for each key in the ``ideal cipher model``, and groups are used as black-box groups in the ``generic model``. In this paper, we focus on practical asymmetric protocols together with their ``reductionist`` security proofs. We cover the two main goals that public-key cryptography is devoted to solve: authentication with digital signatures, and confidentiality with public-key encryption schemes.
-
Analysis of cryptographic protocols using logics of belief: an overview
Abstract
When designing a cryptographic protocol or explaining it, one often uses arguments such as ``since this message was signed by machine B, machine A can be sure it came from B`` in informal proofs justifying how the protocol works. Since it is, in such informal proofs, often easy to overlook an essential assumption, such as a trust relation or the belief that a message is not a replay from a previous session, it seems desirable to write such proofs in a formal system. While such logics do not replace the recent techniques of automatic proofs of safety properties, they help in pointing the weaknesses of the system. In this paper, we present briefly the BAN (Burrows-Abadi-Needham) formal system [10, 11] as well as some derivative. We show how to prove some properties of a~simple protocol, as well as detecting undesirable assumptions. We then explain how the manual search for proofs can be made automatic. Finally, we explain how the lack of proper semantics can be a bit worrying.
-
CardS4: modal theorem proving on Java smart cards
Abstract
We describe a successful implementation of a theorem prover for modal logic S4 that runs on a Java smart card with only 512 KBytes of RAM and 32 KBytes of EEPROM. Since proof search in S4 can lead to infinite branches, this is ``proof of principle`` that non-trivial modal deduction is feasible even on current Java cards. We hope to use this prover as the basis of an on-board security manager for restricting the flow of ``secrets`` between multiple applets residing on the same card, although much work needs to be done to design the appropriate modal logics of ``permission`` and ``obligations``. Such security concerns are the major impediments to the commercial deployment of multi-application smart cards.
-
A formal dynamic semantics of Java: an essential ingredient of Java security
Abstract
Security is becoming a major issue in our highly networked and computerized era. Malicious code detection is an essential step towards securing the execution of applications in a highly inter-connected context. In this paper, we present a formal definition of Java dynamic semantics. This semantics has been used as a basis to develop efficient, rigorous and provably correct static analysis tools and a certifying compiler aimed to detect and prevent the presence of malicious code in Java applications. We propose a small step operational semantics of a large subset for Java. The latter includes features that have not been completely addressed in the related work or addressed in another semantics style. We provide a fully-fledged semantic handling of exceptions, reachable statements, modifiers and class initialization.
