Eighth Workshop on
Formal and Computational Cryptography
FCC 2012
Harvard University, June 27th28th, 2012
The 8th Workshop on Formal and Computational
Cryptography will be held at the University of Harvard
in Cambridge, MA, USA and is affiliated with
Computer Security Foundations Symposium  CSF 2012, June
Background, aim, and scope
Since the 1980s, two approaches have been developed for
analyzing security protocols and systems that rely on
cryptography. One of the approaches is based on a
computational model that considers issues of
computational complexity and probability. Messages are
modelled as bitstrings and security properties are defined
in a strong form, in essence guaranteeing security with
overwhelming probability against all probabilistic
polynomialtime attacks. However, it is difficult to prove
security of large, complex protocols in this model. The
other approach relies on a
symbolic model of protocol execution in which
messages are modelled using a term algebra and cryptographic
primitives are treated as perfect blackboxes, e.g. the only
way to decrypt a ciphertext is to use the corresponding
decryption key. This abstraction enables significantly
simpler and often automated analysis of complex protocols.
Since this model places strong constraints on the attacker,
a fundamental question is whether such an analysis implies
the strong security properties defined in the computational
model.
This workshop focuses on approaches that combine and relate
symbolic and computational protocol analysis. Over the last
few years, there has been a spate of research results in
this area. One set of results establish correspondence
theorems between the two models, in effect showing that, for
a certain class of protocols and properties, security in the
symbolic model implies security in the computational
model. In other work, researchers use languagebased
techniques such as process calculi, type systems, and
protocol logics to reason directly about the computational
model. Finally, several projects are investigating ways of
mechanizing computationally sound proofs of cryptographic
mechanisms. The workshop seeks results in this area of
computationally sound protocol analysis: foundations and
tools.
Important dates
 Deadline for submission: April 20, 2012 (extended)
 Notification: May 11, 2012
 Final abstract due: May 25, 2012
 Workshop: June 27th28th, 2012
