Fiona :transbian: :autism: 🔜 eth0, 40c3
Autistic Binary Trans Woman in IT (because of course).
🏳️⚧️ 🇺🇦 🇵🇸 🇪🇺 🇹🇼 🏴 🏴
I’m a Cryptographer in the space industry adding actual security (PQC) to QKD.
I am a very outspoken supporter and past user of #OpenHRT!
Boosts are pretty much always welcome.
Beware of hot takes.
Luigi is the hero that we need and deserve!
Please don’t read too much into my follows, non-follows and unfollows.
I sometimes post images from my phone, but prefer to post alt-texts on a keyboard. If one is missing on a picture, give it a few minutes, it will be there soon.
In an open relationship with @Senna@mk.absturztau.be. 😊
Still denying any notion that I’m a cat girl, ignore the purring when I get to cuddle with someone!
Unsolicited advice given in good faith is unironically welcome, I’d rather have correct information and receiving it doesn’t hurt my ego. That doesn’t necessarily mean that I’ll follow it, but that I’ll take it into account.
If I make you uncomfortable or overstep your boundaries, please tell me directly and right away, I promise to by nice about it, but I have some genuine blind spots when it comes to what the average person considers nice. (See e.g. the previous paragraph!) In turn you can trust me to do the same and that I won’t hold grudges about genuine mistakes.
- 0 Posts
- 1 Comment
@lagrangeinterpolator@awful.systems @dgerard@awful.systems To add a note on computer verifiable proofs, a story from my own PhD (Cryptography).
It was the night before either the submission-deadline or the deadline for the rebuttal for PQ-Wireguard. Andy and Peter had already retired for the night, basically announcing that they would do the final touches in the morning, with Kai-Chun and me instead working late to finish some TODOs and in exchange being done the following day.
I pretty much got most of the stuff I had been working on done and moved to the Tamarin proofs for some editorial work there and noticed that a statement, for which we had a Tamarin verified proof didn’t seem to make sense. As in: I could give a counter-example in the form of an instantiation of PQ-WG, where that property would be trivially not there! (I believe it was anonymity and that trivially doesn’t hold for any KEMs where the ciphertext reveals the public key, which is not something that is at all incompatible with standard KEM-notions.)
Turns out: Tamarin works in an idealized model and what the proof actually meant was more akin to “There is nothing fundamental in your model that prevents PQ-WG from having that property if you instantiation doesn’t add problems there”.
Which is a very different statement of course!
The end of the story was basically that we called out supervisors late at night, when their work-days really were meant to be over and they wanted to spend time with their partners, that the house was on fire and what we should do.
IIRC the final version of the paper mostly states something along the lines of “it holds if the KEMs don’t leak it”, but the important thing here is that this was computer-verified, just in a model that turned out to be insufficient.
And no, I don’t think anyone here did anything wrong. When I approached Cas Cremers with the issue later his response was also kinda “yeah, symbolic models really struggle in that area”.
And furthermore: I am the last person to deny the need for computer-verifiable proofs, textual proofs have turned out to be disasters, but we really need to be aware of what can go wrong and what they mean.