Commit fe9a9e18 authored by Nadim Kobeissi's avatar Nadim Kobeissi 💾
Browse files

Tidy up examples folder

parent 1557f8e7
Pipeline #819 passed with stages
in 2 minutes and 13 seconds
// SPDX-FileCopyrightText: © 2019-2021 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: GPL-3.0-only
attacker[active]
principal Alice[
generates k
knows private m
b = BLIND(k, m)
]
Alice -> Sarah: b
principal Sarah[
knows private s
gs = G^s
blindsig = SIGN(s, b)
]
Sarah -> Alice: blindsig, gs
principal Alice[
unblindedsig = UNBLIND(k, m, blindsig)
_ = SIGNVERIF(gs, m, unblindedsig)?
]
queries[
confidentiality? m
]
type skey.
type pkey.
type nonce.
fun pk(skey): pkey.
fun encrypt(bitstring, pkey): bitstring.
reduc forall x: bitstring, y: skey; decrypt(encrypt(x,pk(y)),y) = x.
free c: channel.
free M: nonce [private].
query attacker(M).
let processA(pkB: pkey) =
in(c,(n1: nonce, n2: nonce));
out(c, encrypt((n1, n2, M ), pkB)).
let processB(skB: skey, pkB: pkey) =
new n1: nonce; new n2: nonce;
out(c, (n1, n2));
in(c, mes: bitstring);
let (=n1, x1: nonce, x2: nonce) = decrypt(mes, skB) in
out(c, (x1, encrypt((x1, x2, n1), pkB))).
process
new skB: skey; let pkB = pk(skB) in
out(c, pkB);
((!processA(pkB)) | (!processB(skB, pkB)))
// SPDX-FileCopyrightText: © 2019-2021 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: GPL-3.0-only
attacker[active]
principal Client[
generates clientRandom
generates c
gc = G^c
]
principal Server[
knows private certificateKey
knows public hostname
generates serverRandom
generates s
gs = G^s
certificate = HASH(certificateKey, hostname)
gCertificate = G^certificateKey
]
Client -> Server: clientRandom, [gc]
Server -> Client: serverRandom, [gs]
principal Server[
knows public derived
knows public c_hs_traffic
knows public s_hs_traffic
knows public key
knows public iv
sharedSecretServer = gc^s
helloHashServer = HASH(clientRandom, gc, serverRandom, gs)
earlySecretServer = HKDF(nil, nil, nil)
emptyHashServer = HASH(nil)
derivedSecretServer = HKDF(earlySecretServer, derived, emptyHashServer)
handshakeSecretServer = HKDF(derivedSecretServer, sharedSecretServer, nil)
clientHandshakeTrafficSecretServer = HKDF(handshakeSecretServer, c_hs_traffic, helloHashServer)
serverHandshakeTrafficSecretServer = HKDF(handshakeSecretServer, s_hs_traffic, helloHashServer)
clientHandshakeKeyServer = HKDF(clientHandshakeTrafficSecretServer, key, nil)
serverHandshakeKeyServer = HKDF(serverHandshakeTrafficSecretServer, key, nil)
clientHandshakeIVServer = HKDF(clientHandshakeTrafficSecretServer, iv, nil)
serverHandshakeIVServer = HKDF(serverHandshakeTrafficSecretServer, iv, nil)
]
principal Client[
knows public derived
knows public c_hs_traffic
knows public s_hs_traffic
knows public key
knows public iv
sharedSecretClient = gs^c
helloHashClient = HASH(clientRandom, gc, serverRandom, gs)
earlySecretClient = HKDF(nil, nil, nil)
emptyHashClient = HASH(nil)
derivedSecretClient = HKDF(earlySecretClient, derived, emptyHashClient)
handshakeSecretClient = HKDF(derivedSecretClient, sharedSecretClient, nil)
clientHandshakeTrafficSecretClient = HKDF(handshakeSecretClient, c_hs_traffic, helloHashClient)
serverHandshakeTrafficSecretClient = HKDF(handshakeSecretClient, s_hs_traffic, helloHashClient)
clientHandshakeKeyClient = HKDF(clientHandshakeTrafficSecretClient, key, nil)
serverHandshakeKeyClient = HKDF(serverHandshakeTrafficSecretClient, key, nil)
clientHandshakeIVClient = HKDF(clientHandshakeTrafficSecretClient, iv, nil)
serverHandshakeIVClient = HKDF(serverHandshakeTrafficSecretClient, iv, nil)
]
principal Server[
e1 = AEAD_ENC(serverHandshakeKeyServer, certificate, nil)
certVerifyServer = SIGN(certificateKey, HASH(helloHashServer, e1))
e2 = AEAD_ENC(serverHandshakeKeyServer, certVerifyServer, nil)
e3 = AEAD_ENC(serverHandshakeKeyServer, gCertificate, nil)
]
Server -> Client: e1, e2, e3
principal Client[
d1 = AEAD_DEC(serverHandshakeKeyClient, e1, nil)?
d2 = AEAD_DEC(serverHandshakeKeyClient, e2, nil)?
d3 = AEAD_DEC(serverHandshakeKeyClient, e3, nil)?
_ = SIGNVERIF(d3, HASH(helloHashClient, e1), d2)?
]
principal Server[
]
queries[
confidentiality? certificate
]
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