16 ms·

> 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

by a1369209993 3y ago

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

mike_d 3y ago
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.
- pclmulqdq 3y ago
  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.
  - mike_d 3y ago
    https://www.schneier.com/blog/archives/2011/04/schneiers_law.html https://www.schneier.com/blog/archives/2011/04/schneiers_law...
  - cobratbq 3y ago
    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.)
    - mike_d 3y ago
      > 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.
      - cobratbq 3y ago
        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.
        mike_d 3y ago
        > 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-explains-lattice-ice40-fpga-details/ https://hackaday.com/2018/09/27/three-part-deep-dive-explain... https://github.com/sylefeb/Silice/blob/draft/projects/ice40-warmboot/README.md 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.
        cobratbq 3y ago
- cobratbq 3y ago
  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.)
cobratbq 3y ago
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.

mike_d 3y ago

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.

pclmulqdq 3y ago
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.
- mike_d 3y ago
  https://www.schneier.com/blog/archives/2011/04/schneiers_law.html https://www.schneier.com/blog/archives/2011/04/schneiers_law...
- cobratbq 3y ago
  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.)
  - mike_d 3y ago
    > 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.
    - cobratbq 3y ago
      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.
      - mike_d 3y ago
        > 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-explains-lattice-ice40-fpga-details/ https://hackaday.com/2018/09/27/three-part-deep-dive-explain... https://github.com/sylefeb/Silice/blob/draft/projects/ice40-warmboot/README.md 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.
        cobratbq 3y ago
cobratbq 3y ago
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.)

cobratbq 3y ago

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.