references

References

Papers, websites, and various flotsam that we need to keep track of:

Open Attestation.com - Attestation system for OpenStack. Looks to be integrated in the OpenStack project tightly. Still need to see what is actually there. * Very little documentation besides building and installing. Trust Agent Flowcharts and Sequence Diagrams Here
IBM Integrity Measurement Architecture - Linux enhanced with a TPM-based Linux Security Module.
- See IMA for summary of IMA and related publications.
Intel Software Guard Extensions - Secure execution for software that encrypts memory when not resident in cache.
Talk with Dr. Alex Slay at Hopkins to explore if we may leverage the "Big Sky" model. Can't find a website for this one.
Haskell Protocol Example - High-level look at parsing protocols in a "real world" Haskell application.
Trusted Virtual Machine Management for Virtualization in Critical Environments - Looks like Armored Software in 2013
[HIS (Host Integrity at Startup) Presentation] (https://www.ncsi.com/nsatc11/presentations/wednesday/real_world/white.pdf) - NSA research project that takes measurements at startup to see if a system has been changed or compromised. Presentation shows basic idea as well as some real world deployment considerations.

The Inductive Approach to Verifying Cryptographic Protocols - Larry Paulson's classic work on protocol verification
TAPS: A First-Order Verifier for Cryptographic Protocols - Ernie Cohen's paper on protocol verification that "follows" Paulson's. Recommended by Konrad Slind.
Computer-Aided Cryptographic Proofs - Work by Gilles Barthe and others on crypto protocol verification. Recommended by Konrad Slind
Native Communications Security Package for Haskell
Prudent Engineering Practice for Cryptographic Protocols - High level discussion about protocols and how they should be defined.
Strand Spaces: Proving Security Protocols Correct - In depth discussion of strand spaces and using them for verification. Examples include Needham-Schroeder for comparison to other work.
Strand Spaces: Why is a security protocol correct? - Companion to the previous paper discussing semantics of strand spaces.
Implementing Spi Calculus using Nominal Techniques - Paper on implementing spi calculus in Isabelle.

Introduction to the TPM 1.2 - Excellent introduction to the TPM and protocols that use it.
Berlios TPM Emulator - Advocates a software-based TPM emulator and describes its usage. Also reinforces concepts concerning the fundamental structure and functionality of the TPM.
Verifying the TPM 1.2 - Our paper on TPM verification. Includes a description of the CA-based attestation protocol.
Attacking Intel Trusted Execution Technology (paper and slides) - Invisible Things Lab paper on how to attack TPM-based trusted boot environments.
vTPM: Virtualizing the Trusted Platform Module - IBM people talking about doing pretty much exactly what we want to do in Xen-- chaining trust to a vTPM running in Xen so guest Dom U's can use it.
vTPM Configuring in Xen 4.3 - Describes how this guy got a vTPM up and running for Guest DomU's in: "Ubuntu 12.4 (as host), Xen 4.3, Linux Kernel 3.7.1 for Dom0, and Linux Kernel 3.7.9 for DomU kernel."
Virtual Trusted Platform Module - A short overview of the design of implementing a vTPM in Xen