[uh i don't necessarily agree this is why we trust iOS Signal vs say a web page as it exists] #realworldcrypto
WAICT [is not whack??] #realworldcrypto
Code Verify: content, manifest, hash, store in public transparency log #realworldcrypto
Code Verify is a browser extension that checks the log #realworldcrypto
Each leaf of the manifest merkle tree is hash of one js or css file #realworldcrypto
Web documents are complicated 😅 #realworldcrypto
WAICT— embedding into the browser #realworldcrypto
Merkle Patricia Trees instead of traditional Merkle history trees, more efficient auditing #realworldcrypto
Need immediate recovery through transparent opt-out #realworldcrypto
GitHub - waict-wg/waict-integrity-spec: A draft proposal for the integrity mechanism for the WAICT spec

A draft proposal for the integrity mechanism for the WAICT spec - waict-wg/waict-integrity-spec

GitHub
prototype code working in firefox! #realworldcrypto
Next up, 'Signal Lost (Integrity): The Signal App is More than the Sum of its Protocols', presented by Noemi Terzo and Kien Tuong Truong #realworldcrypto
'Signal' is definitely more than just 'The Signal Protocol' #realworldcrypto
ACI: account identifier, PNI: phone number identifier #realworldcrypto
Affects the desktop and android clients, patched and fixed #realworldcrypto
Leverages Sealed Sender #realworldcrypto
The server can send Sealed Sender messages on behalf of anyone without detection (but the system is supposed to be secure in the setting that the server is insecure!) #realworldcrypto
Existing Sealed Sender doesn't authenticate messages 😭 #realworldcrypto
How did we get here? #realworldcrypto
'Boring' stuff matters: open source, documentation!!!, communication with community #realworldcrypto
Ensure that cryptographic logic is _unified_ in a single native library [Is this possible in practice? Sounds less performant] #realworldcrypto
Break time! #realworldcrypto
Next up, the Levchin Prize! #realworldcrypto
The first set of winners: Diffie and Hellman! #realworldcrypto
The second set of winners are the Tamarin prover team!! #realworldcrypto
@cascremers.bsky.social gives the Levchin Prize invited talk on Tamarin #realworldcrypto
Tamarin is a constraint solver impersonating a theorem prover #realworldcrypto
Tamarin prover: Home

Undecidable problem— we can't be sure it will ever terminate #realworldcrypto
Much more precise handling of cryptographic primitives, including those that are motivated by the symbolic modeling of protocols #realworldcrypto
If Tamarin terminates, there is always either an attack or a proof of security (if it doesn't terminate, oop) #realworldcrypto
✨layers of abstraction✨ #realworldcrypto
Can find complex attacks that humans will probably never find on their own #realworldcrypto
Find attacks not by programming in the attacks, but by modeling the protocol, the security notions, the state transitions, and seeing what shakes out #realworldcrypto
Many success stories of real world protocols #realworldcrypto
New version of Tamarin out, and there's a new book! #realworldcrypto
Future predictions: #realworldcrypto
Starting up a Tamarin Foundation! #realworldcrypto
Don't want to be married to any particular methodology, but do want to learn from the other methodologies #realworldcrypto
Struggled in the UC framework whether I've correctly modeled the attacker correctly #realworldcrypto
Q: Insights on investing on web ui, what helps users? A: Being stubborn; thinking more about making something that people can use; open source projects are fragile #realworldcrypto
Next up, 'Finding Bugs and Features Using Cryptographically-Informed Functional Testing', presented by Fernando Virdia eprint.iacr.org/2024/1122 #realworldcrypto

Finding Bugs and Features Usin...
Finding Bugs and Features Using Cryptographically-Informed Functional Testing

In 2018, Mouha et al. (IEEE Trans. Reliability, 2018) performed a post-mortem investigation of the correctness of reference implementations submitted to the SHA3 competition run by NIST, finding previously unidentified bugs in a significant portion of them, including two of the five finalists. Their innovative approach allowed them to identify the presence of such bugs in a black-box manner, by searching for counterexamples of expected cryptographic properties of the implementations under test. In this work, we extend their approach to key encapsulation mechanisms (KEMs) and digital signature schemes (DSSs). We perform our tests on multiple versions of the LibOQS collection of post-quantum schemes to capture implementations at different points of the recent Post-Quantum Cryptography Standardization Process run by NIST. We identify multiple bugs, ranging from software bugs (segmentation faults, memory overflows) to cryptographic bugs, such as ciphertext malleability in KEMs claiming IND-CCA security. We also observe various features of KEMs and DSSs that do not contradict any security guarantees but could appear counter-intuitive. Finally, we compare this methodology with a traditional fuzzing campaign against LibOQS and SUPERCOP, observing that traditional fuzzing harnesses appear less effective in surfacing software and logical bugs.

IACR Cryptology ePrint Archive
Checking if KEM implementations actually achieve IND-CCA in practice by mutating #realworldcrypto
'There is no obvious negative consequence, but it is also not intuitive.' #realworldcrypto
Cryptographically-informed testing #realworldcrypto
Finds bug classes not found by KATs and fuzzing #realworldcrypto
Next up, 'Formosa Crypto: End-to-end formally verified crypto software', presented by Santiago Arranz-Olmos and Ignacio Cuevas #realworldcrypto
Achieving end-to-end security for crypto software #realworldcrypto