Commit 7a09dcec authored by Nadim Kobeissi's avatar Nadim Kobeissi 💎

Add third counter-example from Bruno (to be fixed)

parent 54f4d0f8
Pipeline #699 passed with stages
in 2 minutes and 24 seconds
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