security protocols
formal methods
applied cryptography
analysis tools
automated verification
protocols and standards
ACM Conference on Computer and Communications Security (CCS)
IEEE Symposium on Security and Privacy (S&P)
Journal of Information Security and Applications
IEEE Symposium on Security and Privacy (S&P)
IEEE Symposium on Security and Privacy (S&P)
We have developed several tools for the symbolic analysis of security protocols.
The executive summary is: for standard analysis with respect to various adversary models, or learning about security protocols, use Scyther. If you want machine-checked proofs, use scyther-proof. For advanced analysis and cutting-edge features, use Tamarin.
A high-level overview of their differentiating features you find here.
Below is a selection of protocol models for our analysis tools. Several people were involved of the construction of these models, including:
The selection below is by no means complete. Additional models can be found included in the distributions of the tools, as well as other in papers not listed here.
Using the compromising adversaries version of Scyther tool, we performed a large-scale analysis of the IKE protocol suite, which included all variations of the handshake protocols. A full report can be found in the ESORICS 2011 paper.
| IKEv1 and IKEv2 protocol suites | |
|---|---|
| Scyther models: | IKE model directory |
| Analysed in: | Key Exchange in IPsec revisited: Formal Analysis of IKEv1 and IKEv2 |
| Protocol origin: | RFC 4306 and RFC 5996 |
What's missing? The current models approximate Diffie-Hellman behaviour, and it would be interesting to perform a more precise analysis with the Tamarin prover. Furthermore, parameter negotiation is currently abstracted away, and this could be modeled more precisely.
We analyzed the family of authentication protocols defined in the ISO/IEC 9798 standard. We found a large number of weaknesses using the Scyther tool. We then proposed fixes and verified the correctness of our fixes using Scyther-proof. The results are described in the POST 2012 paper. Based on our recommendations, the ISO/IEC 9798 standard has been updated.
| ISO/IEC 9798 authentication protocols | |
|---|---|
| Scyther models: | model directory for the original protocols |
| Scyther-proof models: | project page for the original and repaired protocols |
| Analysed in: | Provably repairing the ISO/IEC 9798 standard for entity authentication |
| Protocol origin: | ISO/IEC 9798 standard for entity authentication |
Scyther has been used to analyze the PKM protocols that are part of the IEEE 802.16e (WIMAX) standard.
| IEEE 802.16e (WIMAX) PKM protocols | |
|---|---|
| Scyther models: | PKM models |
| Analysed in: | A framework for compositional verification of security protocols |
| Protocol origin: | IEEE 802.16e (WIMAX) standard |
We used our tools to analyze several Authenticated Key Exchange (AKE) protocols with respect to their intended adversary models.
The protocols in the table below that have Scyther models were analyzed using the compromising-adversaries variant of Scyther tool. The underlying theory, which extends the original operational semantics underlying Scyther, and the analysis results are described in the ESORICS 2010 paper. In the accompanying CSL 2010 paper, we introduced the concept of a protocol security hierarchy and analyzed the other protocols with Scyther models, determining their relative strengths.
During initial analysis, we automatically discovered an attack on HMQV that uses the session-state reveal query. (Such attacks are of theoretical interest but not apply to most current deployments.)
The Scyther models for these protocols are part of the Scyther (compromise version) distribution and can be found in the Protocols/AdversaryModels/directory. Alternatively, the relevant protocol models can be directly accessed here.
One drawback of some of the Scyther models is their relatively coarse modeling of the adversary's capabilities with respect to Diffie-Hellman exponentiation. More precise models can be analysed using the Tamarin prover, as presented in the Tamarin paper. In that paper we perform a large case study, which involves all the protocols in the below table that have Tamarin models. The complete list of Tamarin models in this case study can be found here.
| HMQV | |
|---|---|
| Scyther models: | HMQV |
| Analysed in: | Modeling and Analyzing Security in the Presence of Compromising Adversaries |
| Protocol origin: | HMQV: A High-Performance Secure Diffie-Hellman Protocol |
| DHKE-1 | |
|---|---|
| Scyther models: | DHKE-1 |
| Analysed in: | Modeling and Analyzing Security in the Presence of Compromising Adversaries Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries |
| Protocol origin: | On formal models for secure key exchange (version 4) |
| Bilateral Key Exchange | |
|---|---|
| Scyther models: | BKE |
| Analysed in: | Modeling and Analyzing Security in the Presence of Compromising Adversaries |
| BCNP-1 and BCNP-2 | |
|---|---|
| Scyther models: | BCNP-1, BCNP-2 |
| Analysed in: | Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries |
| Protocol origin: | One-round key exchange in the standard model |
| Signed Diffie-Hellman | |
|---|---|
| Scyther models: | Signed-DH |
| Analysed in: | Modeling and Analyzing Security in the Presence of Compromising Adversaries |
| Tamarin models: | Signed-DH |
| Analysed in: | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties |
| KEA+ | |
|---|---|
| Scyther models: | KEA+ |
| Analysed in: | Modeling and Analyzing Security in the Presence of Compromising Adversaries |
| Tamarin models: | Tamarin |
| Analysed in: | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties |
| Protocol origin: | Security Analysis of KEA Authenticated Key Exchange Protocol |
| TS1, TS2, and TS3 (2004 and 2008 versions) | |
|---|---|
| Scyther models: | model directory |
| Analysed in: | Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries |
| Tamarin models: | model directory |
| Analysed in: | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties |
| Protocol origin: | One-Round Protocols for Two-Party Authenticated Key Exchange (2004) Updated version (2008) |
| NAXOS | |
|---|---|
| Scyther models: | NAXOS |
| Analysed in: | Modeling and Analyzing Security in the Presence of Compromising Adversaries Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries |
| Tamarin models: | NAXOS |
| Analysed in: | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties |
| Protocol origin: | Stronger security of authenticated key exchange |
| KAS1 and KAS2 | |
|---|---|
| Tamarin models: | KAS1, KAS2 |
| Analysed in: | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties |
| Protocol origin: | A Generic Variant of NIST's KAS2 Key Agreement Protocol |
| STS-MAC (Station-to-Station) and fixed variants | |
|---|---|
| Tamarin models: | model directory |
| Analysed in: | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties |
| Protocol origin: | Authentication and authenticated key exchanges |
| UM (Unified Model) | |
|---|---|
| Tamarin models: | UM |
| Analysed in: | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties |
| Protocol origin: | Authenticated Diffe-Hellman Key Agreement Protocols |
Tamarin was used to analyse the Yubikey and YubiHSM protocols.
| Yubikey and YubiHSM | |
|---|---|
| Tamarin models: | Yubikey and YubiHSM |
| Analysed in: | YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM |
pdfdiff.py is a small python script that can be used to view the difference between two PDF or PS files.
Download pdfdiff.py 0.92, released on October 4, 2007.
After downloading, either run it through python or make it executable (chmod +x pdfdiff.py) to use it directly from the commandline.
Note that for most Linux distributions, installing xpdf is usually sufficient to get it working. (Afterwards one might want to upgrade to a better diff viewer though).
pdfdiff.py is now hosted on Github: please visit the pdfdiff project page.
(Feel free to invent your own cases, and let me know.)
pdfdiff takes two arguments, each being the filename of a PDF file, and generates a textual diff between the two. It visualises this diff using the first diff-viewer it finds on the system.
pdfdiff relies on pdftotext to extract the plaintext from a PDF file. However, small changes in the text between two PDF files can make a huge difference in the resulting extracted text. More often than not, the difference is so large that doing a diff on the output does not yield a sensible result.
The main function of this program, pdfdiff, is to normalize the output of pdftotext, such that the result is suitable for diff viewing. To achieve this, it attempts to detect sentence endings to reformat paragraphs and lines. Along the way, it removes some ligature encodings to give diff viewers an easier time. After this normalisation procedure, diff viewers commonly yield a substantially better comparison between the contents of the files.
Note that if a single file is provided as input, pdfdiff will directly output the normalised text, enabling its use as a preprocessor for other tools.
