Verified Commit 98d325de authored by Nadim Kobeissi's avatar Nadim Kobeissi 💎

Add exa2.vp test

parent 844c273c
......@@ -239,6 +239,10 @@ var verifpalTests = []VerifpalTest{
Model: "exa.vp",
ResultsCode: "c1",
},
{
Model: "exa2.vp",
ResultsCode: "c1",
},
{
Model: "fakeauth.vp",
ResultsCode: "a0",
......
// 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
principal P2[
x1 = HASH(n1)
]
P2 -> P1: x1
principal P1[
k1 = AEAD_ENC(k, n1, c)
k2 = AEAD_ENC(k, x1, c)
msg = AEAD_DEC(k2, AEAD_ENC(k1, m, c), c)
]
P1 -> P2: msg
queries[
confidentiality? m
]
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