Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(10)
Automated Verification
Computer Security
Cryptographic Algorithm
Cryptographic Protocol
Formal Verification
Lambda Calculus
Protocol Analysis
Protocol Implementation
Public Key Encryption
Source Code
Subscribe
Academic
Publications
Computationally Sound Verification of Source Code
Computationally Sound Verification of Source Code,10.1145/1866307.1866351,Michael Backes,Matteo Maffei,Dominique Unruh
Edit
Computationally Sound Verification of Source Code
(
Citations: 5
)
BibTex

RIS

RefWorks
Download
Michael Backes
,
Matteo Maffei
,
Dominique Unruh
Increasing attention has recently been given to the
formal verification
of the
source code
of cryptographic protocols. The standard approach is to use symbolic abstractions of cryptography that make the analysis amenable to automation. This leaves the possibility of attacks that exploit the mathematical properties of the cryptographic algorithms themselves. In this paper, we show how to conduct the
protocol analysis
on the
source code
level (F# in our case) in a computationally sound way, i.e., taking into account cryptographic security definitions. We build upon the prominent F7 verification framework (Bengtson et al., CSF 2008) which comprises a security typechecker for F# protocol implementations using symbolic idealizations and the concurrent
lambda calculus
RCF to model a core fragment of F#. To leverage this prior work, we give conditions under which symbolic security of RCF programs using cryptographic idealizations implies computational security of the same programs using cryptographic algorithms. Combined with F7, this yields a computationally sound,
automated verification
of F# code containing publickey encryptions and signatures. For the actual computational soundness proof, we use the CoSP framework (Backes, Hofheinz, and Unruh, CCS 2009). We thus inherit the modularity of CoSP, which allows for easily extending our proof to other cryptographic primitives.
Published in 2010.
DOI:
10.1145/1866307.1866351
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
dl.acm.org
)
(
portal.acm.org
)
(
portal.acm.org
)
(
doi.acm.org
)
(
www.informatik.unitrier.de
)
More »
Citation Context
(3)
...The theory of F7 is based on the symbolic model, although in some circumstances it can be adapted to be provably computationally sound [
5
][27]...
...Work on RCF, the concurrent lambda calculus underpinning F7, is directly related. [
5
] provides conditions under...
Francois Dupressoir
,
et al.
Guiding a GeneralPurpose C Verifier to Prove Cryptographic Protocols
...[
1
,9,14,19]). In contrast, there is little prior work on computeraided cryptographic proofs in the computational model...
Gilles Barthe
,
et al.
ComputerAided Security Proofs for the Working Cryptographer
...The theory of F7 is based on the symbolic model, although in some circumstances it can be adapted to be provably computationally sound [
5
][25].,[
5
] provides conditions under which symbolic security of programs in RCF using cryptographic idealizations implies computational security using cryptographic algorithms...
Andrew D. Gordon
,
et al.
Guiding a GeneralPurpose C Verifier to Prove Cryptographic Protocols
References
(34)
Guessing Attacks and the Computational Soundness of Static Equivalence
(
Citations: 28
)
Martín Abadi
,
Mathieu Baudet
,
Bogdan Warinschi
Journal:
Journal of Computer Security  JCS
, vol. 18, no. 5, pp. 398412, 2006
Mobile values, new names, and secure communication
(
Citations: 319
)
Martín Abadi
,
Cédric Fournet
Journal:
Sigplan Notices  SIGPLAN
, vol. 36, no. 3, pp. 104115, 2001
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
(
Citations: 292
)
Martín Abadi
,
Phillip Rogaway
Conference:
IFIP International Conference on Theoretical Computer Science  IFIP TCS
, pp. 322, 2000
Cryptographically Sound Implementations for Communicating Processes
(
Citations: 15
)
Pedro Adão
,
Cédric Fournet
Conference:
International Colloquium on Automata, Languages and Programming  ICALP
, pp. 8394, 2006
CoSP: a general framework for computational soundness proofs
(
Citations: 6
)
Michael Backes
,
Dennis Hofheinz
,
Dominique Unruh
Journal:
Science of Computer Programming  SCP
, pp. 6678, 2009
Sort by:
Citations
(5)
Guiding a GeneralPurpose C Verifier to Prove Cryptographic Protocols
(
Citations: 3
)
Francois Dupressoir
,
Andrew D. Gordon
,
Jan Juerjens
,
David A. Naumann
Conference:
Computer Security Foundations Workshop  CSFW
, pp. 317, 2011
ComputerAided Security Proofs for the Working Cryptographer
Gilles Barthe
,
Benjamin Gr'egoire
,
Sylvain Heraud
,
Santiago Zanella B'eguelin
Conference:
International Crytology Conference  CRYPTO
, vol. 6841, pp. 7190, 2011
Guiding a GeneralPurpose C Verifier to Prove Cryptographic Protocols
Andrew D. Gordon
,
TU Dortmund
,
Fraunhofer ISST
,
David A. Naumann
Published in 2011.
Refinement Types for Secure Implementations
(
Citations: 63
)
Jesper Bengtson
,
Karthikeyan Bhargavan
,
C'edric Fournet
,
Andrew D. Gordon
,
Sergio Maffeis
Conference:
Computer Security Foundations Workshop  CSFW
, pp. 1732, 2008
Cryptographic Verification by Typing for a Sample Protocol Implementation
(
Citations: 1
)
Cédric Fournet
,
Karthikeyan Bhargavan
,
Andrew Gordon