Articles

Applied Rigorous Methods

protocol mag bWith 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.

Cryptography

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.
  • Security 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

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.

Current Foci: Verification of Infrastructure Clouds and Compositions

  • Application of model checking to cloud security, where we formalize cloud topologies as graphs and security goals as state patterns and analyze infrastructure cloud topologies and dynamics with respect to overall security goals.
  • Compositional Reasoning, in which we for instance considered the composability of vertical protocol stacks. See Vertical Protocol Composition.

Relevant Projects

Selected Papers

Cryptography

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.

Modeling and Formal Methods

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.

References

[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.