Commit 62544a8c authored by Nadim Kobeissi's avatar Nadim Kobeissi 💎

Remove exa3.vp "counter-example" (it isn't really)

The model is wrong and doesn't actually show a counter-example.
parent ef837feb
Pipeline #701 passed with stages
in 2 minutes and 42 seconds
// SPDX-FileCopyrightText: © 2019-2020 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: GPL-3.0-only
attacker[active]
principal P1[
knows private k
knows private m
knows public c
generates n1
generates n2
]
P1 -> P2: n1, n2
principal P2[
x1 = HASH(n1)
x2 = HASH(n2)
]
P2 -> P1: x1, x2
principal P1[
k1 = AEAD_ENC(k, HASH(HASH(x1)), c)
k2 = AEAD_ENC(k, x2, c)
msg = AEAD_DEC(k2, AEAD_ENC(k1, m, c), c)
]
P1 -> P2: msg
queries[
confidentiality? m
]
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment