Research using the Ada TCB in StrongSwan

[dguido]

https://twitter.com/kensan42/status/457259429319413760
http://www.codelabs.ch/tkm/ike-separation.pdf
https://www.strongswan.org/blog/2013/04/06/strongswan-5.0.3-released.html
https://strongswan.org/testing/testresults/tkm/
https://codelabs.ch/tkm/

[dguido]

TKM does not support the encryption modes we use :-(.

Supported cipher suites and modes from the docs:

• Encryption Algorithm: IANA 12 aka aes128, aes192, aes256
• Psuedo-random Function: IANA 7 aka prfsha512
• Integrity Algorithm: IANA 14 aka sha2_256, sha2_384, sha2_512
• Diffie-Hellman Group: IANA 15 and 16 aka modp3072 and modp4096
• Authentication Method: IANA 1 aka RSA Digital Signature

We're using the following config for IKEv2 crypto:

# ike=encryption-integrity-prf-dhgroup
ike=aes128gcm16-sha2_256-prfsha256-ecp256!

# esp = encryption-integrity-dhgroup
esp=aes128gcm16-sha2_256-ecp256!

We would have to make the following changes to support TKIM, none of which I want to make:

• Bulk encryption: Drop AES-GCM for AES-CBC
• DH exchange: Drop P-256 ECC for RSA
• Certificates: Drop P-256 ECC for RSA

More info about IKEv2 cipher suites can be found in the StrongSwan docs and from IANA.

TKM may also have other limitations that we would run into, noted at the bottom of their docs.