Handshake Pattern Analysis

Message A show detailed analysis

Message A, sent by the initiator, benefits from sender and receiver authentication and is resistant to Key Compromise Impersonation. Assuming the corresponding private keys are secure, this authentication cannot be forged. Message contents benefit from message secrecy and some forward secrecy: the compromise of the responder's long-term private keys, even at a later date, will lead to message contents being decrypted by the attacker. 4,2

Message B show detailed analysis

Message B, sent by the responder, benefits from sender and receiver authentication and is resistant to Key Compromise Impersonation. Assuming the corresponding private keys are secure, this authentication cannot be forged. Message contents benefit from message secrecy and weak forward secrecy under a passive attacker: if the responder's long-term static keys were previously compromised, the later compromise of the initiator's long-term static keys can lead to message contents being decrypted by an attacker. 4,3

Message C show detailed analysis

Message C, sent by the initiator, benefits from sender and receiver authentication and is resistant to Key Compromise Impersonation. Assuming the corresponding private keys are secure, this authentication cannot be forged. Message contents benefit from message secrecy and weak forward secrecy under a passive attacker: if the initiator's long-term static keys were previously compromised, the later compromise of the responder's long-term static keys can lead to message contents being decrypted by an attacker. 4,3

Message D show detailed analysis

Message D, sent by the responder, benefits from sender and receiver authentication and is resistant to Key Compromise Impersonation. Assuming the corresponding private keys are secure, this authentication cannot be forged. Message contents benefit from message secrecy and weak forward secrecy under a passive attacker: if the responder's long-term static keys were previously compromised, the later compromise of the initiator's long-term static keys can lead to message contents being decrypted by an attacker. 4,3

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