Hacker News Reader

Comment by a1369209993 | Hacker News Reader

a1369209993

> the RNG isn't initialized

Or used.

sk_identity is static over the lifetime of the device, so doesn't need new entropy.

sk_device is generated after pk_user is recieved, so can use HASH(sk_identity,pk_user) as entropy. This results in the same pk_device for every session with a given pk_user, which theoretically enables traffic analysis, but the security model implies traffic analysis is out-of-scope.

signature and enc_sig might need entropy as well, but can still use HASH(sk_identity,pk_user).

View on HN

You could... but I guess my bigger point is that wasn't even addressed.

This is my first time seeing Verifpal, but it looks like a huge foot gun in the wrong hands. Here the author was lead to believe there was some sort of formal validation of his roll-your-own crypto, while glossing over obvious potential implementation flaws.

This is how roll-your-own cryptography often works out. You set the parameters of the attacks you want to defend against, defend against them perfectly, and ignore the practical realities of what attacks are actually coming.

If you are great at it, you will come up with something very efficient that defends only against the attack surface you need. If you are not great at it, you will have an insecure system.

https://www.schneier.com/blog/archives/2011/04/schneiers_law...

I understand the "roll-your-own-crypto" comment. Note that I am taking the perspective of the protocol here, right? So, sure, vulnerabilities in the program are definitely a possibility. (See also other comments explaining more details about the device.) This is part of an experiment to see what can be accomplished with the TKey, which offers an interesting combo of security features.

Feel free to pour me an avalanche of missed attacks. I would be interested to know if your attacks are on the protocol level or in other ways. C programming risks are obviously there. RNG risks are obviously there. You are right that there are plenty of considerations in the program too. They are just not part of this post. (I also commented on the RNG remarks in other replies.)

I think if you read the comments aimed at this protocol, we're all saying that if this is a fun/school project, it sounds good, but if this is a commercial product, use something that has been proven to work.

No protocol exists completely separate from its implementation.

> No protocol exists completely separate from its implementation.

That's a fair point. I am well aware of this.

> Feel free to pour me an avalanche of missed attacks.

Sure. Based on your other comments you are using a USB device that explicitly provides no security guarantees when someone has physical access to it, so any attempt to secure the communications between the host and device are moot.

I'd love to respond to this, but your comment "... that explicitly provides no security guarantees when someone has physical access to it, .." is too abstract for me. I'll make a few guesses.

- Is the device hackable? AFAIK not at this moment. The firmware is minimal. It is a relatively new device, so maybe I am not fully informed.

- Is the device stealable/swappable? Yes. However, it isn't possible/easy to access the internal device-secret (UDS) therefore, swapping it out leads to different secret for the program, cascading into the identity, therefore authentication would fail. (Also, if you steal it, then it's gone. :-P)

- There are protections against opening it up. I'm not an expert on this, so I cannot reliably reproduce from memory the ways it is resistant to this. However, it already means your destroying hardware in the process.

> Is the device hackable? AFAIK not at this moment. The firmware is minimal. It is a relatively new device

It is just a package around an inexpensive FPGA chip. Published and un-published attacks against it exist. For these reasons the TKey developers call out "[a]ll physical and electrical attacks applied to the board [are out of scope]" in the threat model.

https://hackaday.com/2018/09/27/three-part-deep-dive-explain...

https://github.com/sylefeb/Silice/blob/draft/projects/ice40-...

> There are protections against opening it up.

I'd love to see photos if yours is any different than what is on the website.

You're right. I misremembered; read up on a lot of things in last months. Doesn't really matter, because we're discussing a protocol anyways.

I get that Verifpal is not perfect, doesn't do everything. I have considered switching. However, a significant part of proving the mechanism is having correct definitions for all of the needed primitives. If Verifpal tackles the right, correct definitions of the primitives, that is already a significant step, right? Considering the protocol is not complicated, or trying to be, one might try a less complex solution to start with. I am not planning to "gloss over" and there is a bigger pictures. But, feel free to make any missed dimensions concrete. (Note, you might want to check some other comments, as I explain a bit more about the device.)

See also my other comments. The device is tillitis TKey. There is a True RNG (source of entropy) but not recommended, i.e. not cryptographically-secure. However, together with Blake2s (in firmware) or another hash-function, you can at least approximate a source of reasonably secure randomness. Needs to be part of the your user program (to be loaded onto TKey), so you can make this as complicated as you like. You can indeed use the input-data as entropy/seed-bytes and hash it with other data and entropy from TRNG.

I haven't tested yet how fast the TRNG refreshes. Right now, I take 4 bytes (1 collection) of TRNG entropy to be hashed with a static byte-buffer.

The RNG would be used for (sk_device,pk_device). So 'identity' keypair for authn, 'device' (ephemeral) keypair for key-exchange.

Reply on news.ycombinator.com