- Details

With the term rigorous methods, I refer to **cryptography** and **formal methods** (there are others, I don't mention).

I use both kinds of methods to reach security and privacy goals.

Both areas have in common that they establish security properties with respect to a system model, adversary model, security specification and proof methodology.

**Other Interests:** [Information Security] [Identity & Privacy]

Let's have a crude and certainly incomplete comparison of their methods.

I'm mostly considering **asymmetric cryptography** (cf. [Menezes1996] and [Goldreich2007]) and then mostly primitives close to **anonymous credential systems**.

**System model**is, for instance, based on interactive Turing machines (ITM) or I/O automata (basically a model for computations).**Adversary model**is usually an all-quantified probabilistic and computationally bounded machine bounded by polynomial execution time.**S****ecurity specification**is done as, for instance, as game against the adversary or ideal functionality that captures the ideal protocol behavior.**Proof methodology**is, for instance, simulatability with ideal-world/real-world models (Reactive Simulatability or Universal Composability) and/or reduction to a computational hardness assumption (e.g., X = hardness of RSA): "If the adversary manages to break the security of the protocol, he could break fundamental assumption X, as well."

Formal methods is a wide field, whereas I'm only looking at the **analysis of security and privacy properties** of protocols and systems (cf. [Ryan2000]).

**System model**is, for instance, based on multi-set rewriting (e.g., ASLan) or process algebra (e.g., CSP), usually quite remote from actual computations or algebraic properties.**Adversary model**is, for instance, a Doley-Yao network adversary (intruder model), which is agnostic of computational power, but gives the intruder control over insecure network and transformations on terms.**Security specification**is done as formalized security goals, mostly in the algebra or first-order logic. In model checking of trace-based (e.g., authentication or secrecy), it is checked whether an**attack trace**exists, that violates the property.**Proof methodology**is model checking (e.g., exhaustive state space exploration or refinement between models) or theorem proving.

**Application of model checking to cloud security**,**Compositional Reasoning**, in which we for instance considered the composability of vertical protocol stacks. See Vertical Protocol Composition.

**Cloud Security Assurance**, application of language formalization and model checking.**Cryptography for Privacy-enhanced Identity Management**, a crypto topic to enhance the reach of anonymous credential systems in terms of efficiency and expressibility.

Jan Camenisch and Thomas Groß. Efficient attributes for anonymous credentials. In ACM Transactions on Information and System Security (TISSEC), 2011.

Jan Camenisch, Nathalie Casati, Thomas Groß and Victor Shoup. Credential Authenticated Identification and Key Exchange. In Advances in Cryptology - CRYPTO 2010, pages 255-276. LNCS 6223. Springer, August 2010.

Patrik Bichsel, Jan Camenisch, Thomas Groß and Victor Shoup. Anonymous Credentials on a Standard Java Card. In ACM Computer and Communications Security (CCS), 2009, pages 600-610. ACM Press, November 2009.

Thomas Groß and Sebastian Mödersheim. Vertical Protocol Composition. In proceedings of the IEEE Computer Security Foundations Symposium (CSF) 2011.

Sören Bleikertz and Thomas Groß. A Virtualization Assurance Language for Isolation and Deployment. In proceedings of IEEE POLICY 2011.

Thomas Groß, Birgit Pfitzmann and Ahmad-Reza Sadeghi. Browser Model for Security Analysis of Browser-Based Protocols. In Proceedings of the 10th European Symposium on Research in Computer Security (ESORICS), volume 3679 of Lecture Notes in Computer Science, pages 489-508. Springer-Verlag, Berlin Germany, September 2005.

[Menezes1996] Alfred J. Menezes, Paul C. van Oorschot and Scott A. Vanstone. Handbook of Applied Cryptography (Discrete Mathematics and Its Applications). CRC Press, Oct 1996.

[Goldreich2007] Oded Goldreich. Foundations of Cryptography: Volume 1, Basic Tools: Basic Tools. Cambridge University Press, Jan 2007.

[Ryan2000] Peter Ryan, Steve Schneider, Michael Goldsmith, Gavin Lowe and Bill Roscoe. Modelling and Analysis of Security Protocols. Addison Wesley, Dec 2000.