The Community for Technology Leaders
2012 IEEE 25th Computer Security Foundations Symposium (2012)
Cambridge, MA USA
June 25, 2012 to June 27, 2012
ISSN: 1063-6900
ISBN: 978-0-7695-4718-3
TABLE OF CONTENTS
Papers

[Title page iii] (PDF)

pp. iii

Table of contents (PDF)

pp. v-vii

Committees (PDF)

pp. ix-x

Information-Flow Security for a Core of JavaScript (PDF)

D. Hedin , Chalmers Univ. of Technol., Gothenburg, Sweden
A. Sabelfeld , Chalmers Univ. of Technol., Gothenburg, Sweden
pp. 3-18

Secure Information Flow for Concurrent Programs under Total Store Order (PDF)

J. A. Vaughan , Univ. of California Los Angeles, Los Angeles, CA, USA
T. Millstein , Univ. of California Los Angeles, Los Angeles, CA, USA
pp. 19-29

ENCoVer: Symbolic Exploration for Information Flow Security (PDF)

M. Dam , Sch. of Comput. Sci. & Commun., KTH R. Inst. of Technol., Stockholm, Sweden
M. Balliu , Sch. of Comput. Sci. & Commun., KTH R. Inst. of Technol., Stockholm, Sweden
Gurvan Le Guernic , Sch. of Comput. Sci. & Commun., KTH R. Inst. of Technol., Stockholm, Sweden
pp. 30-44

Information-Flow Control for Programming on Encrypted Data (PDF)

D. Stefan , Stanford Univ., Stanford, CA, USA
R. Sharma , Stanford Univ., Stanford, CA, USA
J. C. Mitchell , Stanford Univ., Stanford, CA, USA
J. Zimmerman , Stanford Univ., Stanford, CA, USA
pp. 45-60

Symbolic Analysis of Cryptographic Protocols Containing Bilinear Pairings (PDF)

P. Laud , Cybernetica AS, Tartu, Estonia
A. Pankova , Inst. of Comput. Sci., Univ. of Tartu, Tartu, Estonia
pp. 63-77

Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties (PDF)

S. Meier , Inst. of Inf. Security, ETH Zurich, Zurich, Switzerland
B. Schmidt , Inst. of Inf. Security, ETH Zurich, Zurich, Switzerland
C. Cremers , Inst. of Inf. Security, ETH Zurich, Zurich, Switzerland
D. Basin , Inst. of Inf. Security, ETH Zurich, Zurich, Switzerland
pp. 78-94

Verifying Privacy-Type Properties in a Modular Way (PDF)

V. Cheval , LSV, INRIA Saclay, Cachan, France
M. Arapinis , Sch. of Comput. Sci., Univ. of Birmingham, Birmingham, UK
S. Delaune , LSV, INRIA Saclay, Cachan, France
pp. 95-109

Security Analysis of Role-Based Access Control through Program Verification (PDF)

P. Madhusudan , Univ. of Illinois, Urbana, IL, USA
A. L. Ferrara , Univ. of Bristol, Bristol, UK
G. Parlato , Univ. of Southampton, Southampton, UK
pp. 113-125

Gran: Model Checking Grsecurity RBAC Policies (PDF)

R. Focardi , DAIS, Univ. Ca' Foscari, Venezia, Italy
S. Calzavara , DAIS, Univ. Ca' Foscari, Venezia, Italy
M. Bugliesi , DAIS, Univ. Ca' Foscari, Venezia, Italy
M. Squarcina , DAIS, Univ. Ca' Foscari, Venezia, Italy
pp. 126-138

Labeled Sequent Calculi for Access Control Logics: Countermodels, Saturation and Abduction (PDF)

D. Garg , Max Planck Inst. for Software Syst., Germany
V. Genovese , Univ. of Luxembourg, Luxembourg, Luxembourg
D. Rispoli , Univ. of Torino, Turin, Italy
pp. 139-153

Secure Compilation to Modern Processors (PDF)

B. Jacobs , IBBT-DistriNet, Katholieke Univ., Leuven, Belgium
R. Strackx , IBBT-DistriNet, Katholieke Univ., Leuven, Belgium
P. Agten , IBBT-DistriNet, Katholieke Univ., Leuven, Belgium
F. Piessens , IBBT-DistriNet, Katholieke Univ., Leuven, Belgium
pp. 171-185

Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization (PDF)

J. D. Campo , Fac. de Ing., Univ. de la Republica, Montevideo, Uruguay
G. Betarte , Fac. de Ing., Univ. de la Republica, Montevideo, Uruguay
G. Barthe , IMDEA Software Inst., Madrid, Spain
C. Luna , Fac. de Ing., Univ. de la Republica, Montevideo, Uruguay
pp. 186-197

A Framework for the Cryptographic Verification of Java-Like Programs (PDF)

T. Truderung , Univ. of Trier, Trier, Germany
R. Kusters , Univ. of Trier, Trier, Germany
J. Graf , KIT, Karlsruhe, Germany
pp. 198-212

Refining Key Establishment (PDF)

C. Sprenger , Inst. of Inf. Security, ETH Zurich, Zurich, Switzerland
D. Basin , Inst. of Inf. Security, ETH Zurich, Zurich, Switzerland
pp. 230-246

Measuring Information Leakage Using Generalized Gain Functions (PDF)

C. Palamidessi , INRIA, Ecole Polytech., Palaiseau, France
K. Chatzikokolakis , INRIA, Ecole Polytech., Palaiseau, France
M. S. Alvim , Univ. of Pennsylvania, Philadelphia, PA, USA
G. Smith , Florida Int. Univ., Miami, FL, USA
pp. 265-279

The Thermodynamics of Confidentiality (PDF)

P. Malacaria , Sch. of Electron. Eng. & Comput. Sci., Queen Mary Univ. of London, London, UK
F. Smeraldi , Sch. of Electron. Eng. & Comput. Sci., Queen Mary Univ. of London, London, UK
pp. 280-290

Securing Interactive Programs (PDF)

D. Hedin , Dept. of Comput. Sci. & Eng., Chalmers Univ. of Technol., Gothenburg, Sweden
W. Rafnsson , Dept. of Comput. Sci. & Eng., Chalmers Univ. of Technol., Gothenburg, Sweden
A. Sabelfeld , Dept. of Comput. Sci. & Eng., Chalmers Univ. of Technol., Gothenburg, Sweden
pp. 293-307

Automatically Verified Mechanized Proof of One-Encryption Key Exchange (PDF)

B. Blanchet , INRIA, Ecole Normale Super., Paris, France
pp. 325-339

Generic Indifferentiability Proofs of Hash Designs (PDF)

P. Fouque , Ecole normale Super., INRIA Rennes, Rennes, France
M. Daubignard , Univ. of Grenoble (UJF), Verimag, France
Y. Lakhnech , Univ. of Grenoble (UJF), Verimag, France
pp. 340-353

Verified Security of Merkle-Damgård (PDF)

C. Kunz , Univ. Politec. de Madrid, Madrid, Spain
B. Gregoire , INRIA Sophia Antipolis-Mediterranee, Sophia-Antipolis, France
M. Berg , Saarland Univ., Saarbrucken, Germany
G. Barthe , IMDEA Software Inst., Madrid, Spain
M. Backes , Saarland Univ., Saarbrucken, Germany
M. Skoruppa , Saarland Univ., Saarbrucken, Germany
pp. 354-368

Provably Secure and Practical Onion Routing (PDF)

A. Kate , MPI-SWS, Saarbrucken, Germany
I. Goldberg , Univ. of Waterloo, Waterloo, ON, Canada
M. Backes , Saarland Univ., Saarbrucken, Germany
E. Mohammadi , Saarland Univ., Saarbrucken, Germany
pp. 369-385

Author index (PDF)

pp. 387
97 ms
(Ver )