nach oben

2009 | Buch

Kapitel lesen Erstes Kapitel lesen

Foundations of Security Analysis and Design V

FOSAD 2007/2008/2009 Tutorial Lectures

herausgegeben von: Alessandro Aldini, Gilles Barthe, Roberto Gorrieri

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

FOSAD has been one of the foremost educational events established with the goal of disseminating knowledge in the critical area of security in computer systems and networks. Offering a good spectrum of current research in foundations of security, FOSAD also proposes panels dedicated to topical open problems, and giving presentations about ongoing work in the field, in order to favour discussions and novel scientific collaborations.

This book presents thoroughly revised versions of ten tutorial lectures given by leading researchers during three International Schools on Foundations of Security Analysis and Design, FOSAD 2007/2008/2009, held in Bertinoro, Italy, in September 2007, August 2008, and August/September 2009. The topics covered in this book include cryptographic protocol analysis, program and resource certification, identity management and electronic voting, access and authorization control, wireless security, mobile code and communications security.

Inhaltsverzeichnis

Frontmatter

Foundations of Security Analysis and Design

FOSAD 2007

Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties

Abstract

In this tutorial, we give an overview of the Maude-NRL Protocol Analyzer (Maude-NPA), a tool for the analysis of cryptographic protocols using functions that obey different equational theories. We show the reader how to use Maude-NPA, and how it works, and also give some of the theoretical background behind the tool.

Santiago Escobar, Catherine Meadows, José Meseguer

FOSAD 2008

An Introduction to Certificate Translation

Abstract

In a Proof-Carrying Code scenario, certificate generation remains a challenging problem. Typically, it is implemented as a compiler module that targets low-level executable code. Hence, since automatic, the properties under verification are limited to very simple safety policies. Discharging verification conditions automatically for arbitrarily complex properties is unfeasible. Therefore, it requires the support of tool-based interactive verification, which commonly targets high-level structured code. To connect source code verification and compiled code certification we have proposed a technique to build, from a certificate of the source program, a certificate for the result of its compilation. In this tutorial, we illustrate the principles of this technique, certificate translation, in the context of a certified quicksort algorithm. For each transformation step that defines the compiler, we explain the corresponding transformation of the certificate.

Gilles Barthe, César Kunz

Federated Identity Management

Abstract

This paper addresses the topic of federated identity management. It discusses in detail the following topics: what is digital identity, what is identity management, what is federated identity management, Kim Cameron’s 7 Laws of Identity, how can we protect the user’s privacy in a federated environment, levels of assurance, some past and present federated identity management systems, and some current research in FIM.

David W. Chadwick

Electronic Voting in the Netherlands: From Early Adoption to Early Abolishment

Abstract

This paper discusses how electronic voting was implemented in practice in the Netherlands, which choices were made and how electronic voting was finally abolished. This history is presented in the context of the requirements of the election process, as well as the technical options that are available to increase the reliability and security of electronic voting.

Bart Jacobs, Wolter Pieters

FOSAD 2009

Logic in Access Control (Tutorial Notes)

Abstract

Access control is central to security in computer systems. Over the years, there have been many efforts to explain and to improve access control, sometimes with logical ideas and tools. This paper is a partial survey and discussion of the role of logic in access control. It considers logical foundations for access control and their applications, in particular in languages for security policies. It focuses on some specific logics and their properties. It is intended as a written counterpart to a tutorial given at the 2009 International School on Foundations of Security Analysis and Design.

Martín Abadi

The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols

Abstract

We introduce the Open-source Fixed-point Model Checker OFMC for symbolic security protocol analysis, which extends the On-the-fly Model Checker (the previous OFMC). The native input language of OFMC is the AVISPA Intermediate Format IF. OFMC also supports AnB, a new Alice-and-Bob-style language that extends previous similar languages with support for algebraic properties of cryptographic operators and with a simple notation for different kinds of channels that can be used both as assumptions and as protocol goals. AnB specifications are automatically translated to IF.

OFMC performs both protocol falsification and bounded session verification by exploring, in a demand-driven way, the transition system resulting from an IF specification. OFMC’s effectiveness is due to the integration of a number of symbolic, constraint-based techniques, which are correct and terminating. The two major techniques are the lazy intruder, which is a symbolic representation of the intruder, and constraint differentiation, which is a general search-reduction technique that integrates the lazy intruder with ideas from partial-order reduction. Moreover, OFMC allows one to analyze security protocols with respect to an algebraic theory of the employed cryptographic operators, which can be specified as part of the input. We also sketch the ongoing integration of fixed-point-based techniques for protocol verification for an unbounded number of sessions.

Sebastian Mödersheim, Luca Viganò

Verification of Concurrent Programs with Chalice

Abstract

A program verifier is a tool that allows developers to prove that their code satisfies its specification for every possible input and every thread schedule. These lecture notes describe a verifier for concurrent programs called Chalice.

Chalice’s verification methodology centers around permissions and permission transfer. In particular, a memory location may be accessed by a thread only if that thread has permission to do so. Proper use of permissions allows Chalice to deduce upper bounds on the set of locations modifiable by a method and guarantees the absence of data races for concurrent programs. The lecture notes informally explain how Chalice works through various examples.

K. Rustan M. Leino, Peter Müller, Jan Smans

Certified Static Analysis by Abstract Interpretation

Abstract

A certified static analysis is an analysis whose semantic validity has been formally proved correct with a proof assistant. We propose a tutorial on building a certified static analysis in Coq. We study a simple bytecode language for which we propose an interval analysis that allows to verify statically that no array-out-of-bounds accesses will occur.

Frédéric Besson, David Cachera, Thomas Jensen, David Pichardie

Resource Usage Analysis and Its Application to Resource Certification

Abstract

Resource usage is one of the most important characteristics of programs. Automatically generated information about resource usage can be used in multiple ways, both during program development and deployment. In this paper we discuss and present examples on how such information is obtained in COSTA, a state of the art static analysis system. COSTA obtains safe symbolic upper bounds on the resource usage of a large class of general-purpose programs written in a mainstream programming language such as Java (bytecode). We also discuss the application of resource-usage information for code certification, whereby code not guaranteed to run within certain user-specified bounds is rejected.

Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, Damiano Zanardini

Analysis of Security Threats, Requirements, Technologies and Standards in Wireless Sensor Networks

Abstract

As sensor networks are more and more being implemented in real world settings, it is necessary to analyze how the different requirements of these real-world applications can influence the security mechanisms. This paper offers both an overview and an analysis of the relationship between the different security threats, requirements, applications, and security technologies. Besides, it also overviews some of the existing sensor network standards, analyzing their security mechanisms.

Javier Lopez, Rodrigo Roman, Cristina Alcaraz

Backmatter

Titel: Foundations of Security Analysis and Design V
herausgegeben von: Alessandro Aldini
Gilles Barthe
Roberto Gorrieri
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-642-03829-7
Print ISBN: 978-3-642-03828-0
DOI: https://doi.org/10.1007/978-3-642-03829-7