VerifHub

VerifHub allows Verifpal® users to easily share and discuss Verifpal models of cryptographic protocols. The VerifHub service provides unique URIs for each shared model which includes a syntax-highlighted model, an automatically generated diagram and a summary of the analysis results.

Switch to Diagram View

communication-obfuscated-no-bob-to-bob-hsm.vp

Submitted on 29 Dec 21 21:53 UTC.

attacker[active]

principal Charlie[
]

principal Alice[
]

principal Alice_hsm[
]

principal Bob[
]

principal Bob_hsm[
]

principal Charlie[
	knows private private_charlie
	public_charlie = G^private_charlie
]

Charlie -> Bob: [public_charlie]

Bob -> Bob_hsm: [public_charlie]

principal Bob_hsm[
	knows private private_bob
	public_bob = G^private_bob
]

Bob_hsm -> Bob: [public_bob]

Bob -> Alice: [public_bob]

Alice -> Alice_hsm: [public_bob]

Charlie -> Alice: [public_charlie]

Alice -> Alice_hsm: [public_charlie]

principal Alice_hsm[
	knows private private_alice
	public_alice = G^private_alice
]

Alice_hsm -> Alice: [public_alice]

principal Alice[
]

Alice -> Charlie: public_alice

principal Charlie[
	public_alice_signed_by_charlie = SIGN(private_charlie, public_alice)
]

Charlie -> Alice: [public_alice_signed_by_charlie]

Alice -> Alice_hsm: [public_alice_signed_by_charlie]

principal Alice_hsm[
	_ = SIGNVERIF(public_charlie, public_alice, public_alice_signed_by_charlie)?
]

principal Alice[
	knows private private_message
]

principal Alice_hsm[
	generates symmetric_key
	symmetric_key_enc = PKE_ENC(public_bob, symmetric_key)
]

principal Alice_hsm[
	knows private private_message
	private_message_signed_by_alice = SIGN(private_alice, private_message)
	enc_private_message = ENC(symmetric_key, private_message)
]

Alice_hsm -> Alice: [enc_private_message], [symmetric_key_enc], [private_message_signed_by_alice]

principal Alice_hsm[
	generates private_alice_ep
	public_alice_ep = G^private_alice_ep
	public_alice_ep_signed_by_alice = SIGN(private_alice, public_alice_ep)
]

Alice_hsm -> Alice: [public_alice_ep], [public_alice_ep_signed_by_alice]

Alice -> Bob: public_alice, public_alice_ep, public_alice_ep_signed_by_alice, public_alice_signed_by_charlie

Bob -> Bob_hsm: [public_alice], [public_alice_ep], [public_alice_ep_signed_by_alice], [public_alice_signed_by_charlie]

principal Bob_hsm[
	_ = SIGNVERIF(public_charlie, public_alice, public_alice_signed_by_charlie)?
	_ = SIGNVERIF(public_alice, public_alice_ep, public_alice_ep_signed_by_alice)?
	generates private_bob_ep
	public_bob_ep = G^private_bob_ep
	public_bob_ep_signed_by_bob = SIGN(private_bob, public_bob_ep)
]

Bob_hsm -> Bob: [public_bob_ep], [public_bob_ep_signed_by_bob]

Bob -> Alice: public_bob_ep, public_bob_ep_signed_by_bob

Alice -> Alice_hsm: [public_bob_ep], [public_bob_ep_signed_by_bob]

principal Alice_hsm[
	_ = SIGNVERIF(public_bob, public_bob_ep, public_bob_ep_signed_by_bob)?
]

principal Alice_hsm[
	knows public hkdf_salt
	knows public hkdf_info
	yx = public_bob_ep^private_alice_ep
	bx = public_bob^private_alice_ep
	ya = public_bob_ep^private_alice
	ikm_5_alicehsm = CONCAT(yx, bx, ya, public_alice_ep, public_bob_ep)
	ikm_alicehsm = CONCAT(ikm_5_alicehsm, public_alice, public_bob)
	k_alicehsm = HKDF(hkdf_salt, ikm_alicehsm, hkdf_info)
]

principal Alice_hsm[
	k_enc_private_message = ENC(k_alicehsm, enc_private_message)
	k_symmetric_key_enc = ENC(k_alicehsm, symmetric_key_enc)
]

Alice_hsm -> Alice: [k_enc_private_message], [k_symmetric_key_enc]

Alice -> Bob: k_enc_private_message, k_symmetric_key_enc, private_message_signed_by_alice

queries[
	confidentiality? private_message
]

Switch to Model View

Title:communication-obfuscated-no-bob-to-bob-hsm.vp Note over Charlie: Note over Alice: Note over Alice_hsm: Note over Bob: Note over Bob_hsm: Note over Charlie: knows private private_charlie\n public_charlie = G^private_charlie\n Charlie -> Bob: [public_charlie] Bob -> Bob_hsm: [public_charlie] Note over Bob_hsm: knows private private_bob\n public_bob = G^private_bob\n Bob_hsm -> Bob: [public_bob] Bob -> Alice: [public_bob] Alice -> Alice_hsm: [public_bob] Charlie -> Alice: [public_charlie] Alice -> Alice_hsm: [public_charlie] Note over Alice_hsm: knows private private_alice\n public_alice = G^private_alice\n Alice_hsm -> Alice: [public_alice] Note over Alice: Alice -> Charlie: public_alice Note over Charlie: public_alice_signed_by_charlie = SIGN(private_charlie, public_alice)\n Charlie -> Alice: [public_alice_signed_by_charlie] Alice -> Alice_hsm: [public_alice_signed_by_charlie] Note over Alice_hsm: _ = SIGNVERIF(public_charlie, public_alice, public_alice_signed_by_charlie)?\n Note over Alice: knows private private_message\n Note over Alice_hsm: generates symmetric_key\n symmetric_key_enc = PKE_ENC(public_bob, symmetric_key)\n Note over Alice_hsm: knows private private_message\n private_message_signed_by_alice = SIGN(private_alice, private_message)\n enc_private_message = ENC(symmetric_key, private_message)\n Alice_hsm -> Alice: [enc_private_message], [symmetric_key_enc], [private_message_signed_by_alice] Note over Alice_hsm: generates private_alice_ep\n public_alice_ep = G^private_alice_ep\n public_alice_ep_signed_by_alice = SIGN(private_alice, public_alice_ep)\n Alice_hsm -> Alice: [public_alice_ep], [public_alice_ep_signed_by_alice] Alice -> Bob: public_alice, public_alice_ep, public_alice_ep_signed_by_alice, public_alice_signed_by_charlie Bob -> Bob_hsm: [public_alice], [public_alice_ep], [public_alice_ep_signed_by_alice], [public_alice_signed_by_charlie] Note over Bob_hsm: _ = SIGNVERIF(public_charlie, public_alice, public_alice_signed_by_charlie)?\n _ = SIGNVERIF(public_alice, public_alice_ep, public_alice_ep_signed_by_alice)?\n generates private_bob_ep\n public_bob_ep = G^private_bob_ep\n public_bob_ep_signed_by_bob = SIGN(private_bob, public_bob_ep)\n Bob_hsm -> Bob: [public_bob_ep], [public_bob_ep_signed_by_bob] Bob -> Alice: public_bob_ep, public_bob_ep_signed_by_bob Alice -> Alice_hsm: [public_bob_ep], [public_bob_ep_signed_by_bob] Note over Alice_hsm: _ = SIGNVERIF(public_bob, public_bob_ep, public_bob_ep_signed_by_bob)?\n Note over Alice_hsm: knows public hkdf_salt\n knows public hkdf_info\n yx = public_bob_ep^private_alice_ep\n bx = public_bob^private_alice_ep\n ya = public_bob_ep^private_alice\n ikm_5_alicehsm = CONCAT(yx, bx, ya, public_alice_ep, public_bob_ep)\n ikm_alicehsm = CONCAT(ikm_5_alicehsm, public_alice, public_bob)\n k_alicehsm = HKDF(hkdf_salt, ikm_alicehsm, hkdf_info)\n Note over Alice_hsm: k_enc_private_message = ENC(k_alicehsm, enc_private_message)\n k_symmetric_key_enc = ENC(k_alicehsm, symmetric_key_enc)\n Alice_hsm -> Alice: [k_enc_private_message], [k_symmetric_key_enc] Alice -> Bob: k_enc_private_message, k_symmetric_key_enc, private_message_signed_by_alice

Analysis Results

The model submitter provided the following analysis results:

Query 1 (Confidentiality): PASS

Please note that these results are not verified to be accurate. The model submitter may choose to provide false analysis results if they so desire. It is strongly recommended that you re-run the analysis of this model locally if you wish to verify the authenticity of the analysis results above.

Discuss This Model

© Copyright 2019- Nadim Kobeissi. All Rights Reserved. “Verifpal” and the “Verifpal” logo/mascot are registered trademarks of Nadim Kobeissi. Verifpal software is provided as free and open source software, licensed under the GPLv3. Verifpal User Manual, as well as this website, are provided under the CC BY-NC-ND 4.0 license. Published by Symbolic Software.