Handshake Pattern Analysis

Message A show detailed analysis

Message A, sent by the initiator, does not benefit from sender authentication and does not provide message integrity. It could have been sent by any party, including an active attacker. Message contents do not benefit from message secrecy even against a purely passive attacker and any forward secrecy is out of the question. 0,0

Message B show detailed analysis

Message B, sent by the responder, does not benefit from sender authentication and does not provide message integrity. It could have been sent by any party, including an active attacker. Message contents benefit from some message secrecy and some forward secrecy, but not sufficiently to resist any active attacker. 0,1

Message C show detailed analysis

Message C, sent by the initiator, does not benefit from sender authentication and does not provide message integrity. It could have been sent by any party, including an active attacker. Message contents benefit from some message secrecy and some forward secrecy, but not sufficiently to resist any active attacker. 0,1

Message D show detailed analysis

Message D, sent by the responder, does not benefit from sender authentication and does not provide message integrity. It could have been sent by any party, including an active attacker. Message contents benefit from some message secrecy and some forward secrecy, but not sufficiently to resist any active attacker. 0,1

Generate Cryptographic Models for Formal Verification

Get Model active attacker Get Model passive attacker

Generate Secure Protocol Implementation Code

Get Implementation written in go Get Implementation written in rust

Generate Rust Implementation Code for WebAssembly Builds

Get Implementation written for wasm