Skip to content
Permalink
Branch: master
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
783 lines (699 sloc) 23.2 KB
/*
IK:
<- s
...
-> e, es, s, ss
<- e, ee, se
*/
theory Disco_IK
begin
builtins: diffie-hellman, xor
functions: sponge/1
///////////////////////////////////////
// Rules: Pre-Messages
///////////////////////////////////////
//
// <- s
// ====
rule Responder_Init:
let
s_pub = 'g'^~s_priv
in
// tamarin: `s_pub` is public knowledge to adversaries and initiators
[Fr(~s_priv)]
--[Identity(~s_priv, s_pub)]->
[!ResponderIdentity(~s_priv, s_pub), Out(s_pub)]
///////////////////////////////////////
// Rules: Messages
///////////////////////////////////////
//
// Initiator: Initialize
// ========================
// an initiator as a long-term keypair that is not necessarily known
// to adversaries, and that can be re-used with servers
rule Initiator_Init:
let
s_pub = 'g'^~s_priv
in
[Fr(~s_priv)]--[Identity(~s_priv, s_pub)]->[!InitiatorIdentity(~s_priv, s_pub)]
//
// Initiator: Write First Message
// ========================
// write -> e, es, s, ss
rule Initiator_WriteMsg1:
let
// dh
e_pub = 'g'^~e_priv
// init + prologue
input1 = <'prologue', 'AD', 'Noise_IK', 'strobe_init'>
// -> e
input2 = <e_pub, 'CLR', input1>
// -> es
es = rs^~e_priv
input3 = <es, 'AD', input2>
// -> s
input4 = <'ENC', input3>
encrypted_s = sponge(input4) ⊕ s_pub
input5 = <s_pub, input4>
// -> ss
ss = rs^~s_priv
input6 = <ss, 'AD', input5>
// -> payload1
input7 = <'ENC', input6>
ciphertext1 = sponge(input7) ⊕ ~payload1
input8 = <~payload1, input7>
// -> tag1
input9 = <'MAC', input8>
tag1 = sponge(input9)
input10 = <'0000000000000000', input9>
// helpers
id = e_pub
in
[!InitiatorIdentity(~s_priv, s_pub), !ResponderIdentity(~unknown, rs), Fr(~e_priv), Fr(~payload1)]
--[InitHandshake(e_pub, s_pub, rs), Sent1(e_pub, s_pub, rs, ~payload1)]->
[Initiator_0(e_pub, s_pub, rs, input10), Out(<rs, e_pub, encrypted_s, ciphertext1, tag1>)]
//
// Responder: Read First Message, Write Second Message
// ===================================================
// read -> e, es, s, ss
// write <- e, ee, se
rule Responder_ReadMsg1_WriteMsg2:
let
// dh
re = 'g'^unknown
e_pub = 'g'^~e_priv
// init + prologue
input1 = <'prologue', 'AD', 'Noise_IK', 'strobe_init'>
// ----------------------------------------------
// -> e
input2 = <re, 'CLR', input1>
// -> es
es = re^~s_priv
input3 = <es, 'AD', input2>
// -> s
input4 = <'ENC', input3>
rs = 'g'^unknown2
rs = sponge(input4) ⊕ encrypted_rs
input5 = <rs, input4>
// -> ss
ss = rs^~s_priv
input6 = <ss, 'AD', input5>
// -> payload1
input7 = <'ENC', input6>
payload1 = sponge(input7) ⊕ ciphertext1
input8 = <payload1, input7>
// -> tag1
input9 = <'MAC', input8>
tag1 = sponge(input9)
input10 = <'0000000000000000', input9>
// ----------------------------------------------
// <- e
input11 = <e_pub, 'CLR', input10>
// <- ee
ee = re^~e_priv
input12 = <ee, 'AD', input11>
// <- se
se = rs^~e_priv
input13 = <se, 'AD', input12>
// <- payload2
input14 = <'ENC', input13>
ciphertext2 = sponge(input14) ⊕ ~payload2
input15 = <~payload2, input14>
// <- tag2
input16 = <'MAC', input15>
tag2 = sponge(input16)
input17 = <'0000000000000000', input16>
/// Split
/// =====
/// strobe: we don't care about RATCHET because this is implementation level mitigation
c1 = sponge(<'initiator', 'AD', input17>)
c2 = sponge(<'responder', 'AD', input17>)
// helpers
id = re
me = s_pub
them = rs
in
[!ResponderIdentity(~s_priv, s_pub), In(<s_pub, re, encrypted_rs, ciphertext1, tag1>), Fr(~e_priv), Fr(~payload2)]
// common theme: we use a peer's ephemeral key ~e_priv as a unique identifier as well
--[ResponderInit(id, me, them), Shared('responder', id, me, them, c1, c2), Received1(id, me, them, payload1), Sent2(id, me, them, ~payload2)]->
[Responder_final(id, me, them, c1, c2), Out(<re, e_pub, ciphertext2, tag2>)]
// Responder_final(session_id, my_id, their_id, c1, c2)
// Out(<
// re: their public key as unique identifier for the session,
// e_pub, ciphertext2, tag2: noise handshake message
// )
//
// Initiator: Read Second Message
// ==============================
// read <- e, ee, se
rule Initiator_ReadMsg2:
let
// dh
re = 'g'^unknown
// <- e
input2 = <re, 'CLR', input1>
// <- ee
ee = re^~e_priv
input3 = <ee, 'AD', input2>
// <- se
se = re^~s_priv
input4 = <se, 'AD', input3>
// <- payload2
input5 = <'ENC', input4>
payload2 = sponge(input5) ⊕ ciphertext2
input6 = <payload2, input5>
// <- tag2
input7 = <'MAC', input6>
tag2 = sponge(input7)
input8 = <'0000000000000000', input7>
// split
c1 = sponge(<'initiator', 'AD', input8>)
c2 = sponge(<'responder', 'AD', input8>)
// helpers
id = e_pub
me = s_pub
them = rs
in
[Initiator_0(e_pub, s_pub, rs, input1), !InitiatorIdentity(~s_priv, s_pub), In(<e_pub, re, ciphertext2, tag2>)]
--[Shared('initiator', id, me, them, c1, c2), Received2(id, me, them, payload2)]->
[Initiator_final(id, me, them, c1, c2)]
//
// Post-Handshake
// ==============================
// ->
// <-
// Initiator -> Responder
rule Initiator_SendApplicationData:
let
input1 = <'ENC', c1>
ciphertext = sponge(input1) ⊕ ~plaintext
input2 = <~plaintext, input1>
input3 = <'MAC', input2>
tag = sponge(input2)
in
[Initiator_final(id, me, them, c1, c2), Fr(~plaintext)]
--[SentAppData('initiator', id, me, them, ~plaintext)]->
// tamarin: we kill the state to avoid loops
[Out(<id, ciphertext, tag>)]
rule Responder_ReceiveApplicationData:
let
input1 = <'ENC', c1>
plaintext = sponge(input1) ⊕ ciphertext
input2 = <plaintext, input1>
input3 = <'MAC', input2>
tag = sponge(input2)
in
[Responder_final(id, me, them, c1, c2), In(<id, ciphertext, tag>)]
--[ReceivedAppData('responder', id, me, them, plaintext)]->
[]
// Responder -> Initiator
rule Responder_SendApplicationData:
let
input1 = <'ENC', c2>
ciphertext = sponge(input1) ⊕ ~plaintext
input2 = <~plaintext, input1>
input3 = <'MAC', input2>
tag = sponge(input2)
in
[Responder_final(id, me, them, c1, c2), Fr(~plaintext)]
--[SentAppData('responder', id, me, them, ~plaintext)]->
[Out(<id, ciphertext, tag>)]
rule Initiator_ReceiveApplicationData:
let
input1 = <'ENC', c2>
plaintext = sponge(input1) ⊕ ciphertext
input2 = <plaintext, input1>
input3 = <'MAC', input2>
tag = sponge(input2)
in
[Initiator_final(id, me, them, c1, c2), In(<id, ciphertext, tag>)]
--[ReceivedAppData('initiator', id, me, them, plaintext)]->
[]
///////////////////////////////////////
// Rules: Lemma Helpers
///////////////////////////////////////
// allows us to model what happens when a long-term static key `s` is broken
rule Attack_s_revealed:
[!InitiatorIdentity(~s_priv, s_pub)]--[Reveal(s_pub)]->[Out(~s_priv)]
rule Attack_rs_revealed:
[!ResponderIdentity(~s_priv, s_pub)]--[Reveal(s_pub)]->[Out(~s_priv)]
///////////////////////////////////////
// Lemmas: Sanity Checks
///////////////////////////////////////
//
// Can we run the protocol?
// ========================
// These are "exists-trace" lemmas to see if we can go through
// the state transitions as intended.
// first handshake payload is sent and received
lemma Payload1Received:
exists-trace
"
Ex id initiator responder payload1 #i #j .
(
Sent1(id, initiator, responder, payload1) @ #i &
Received1(id, responder, initiator, payload1) @ #j &
#i < #j
)
"
// TODO: include that Reaveal never happens as well
// second handshake payload is sent and received
lemma Payload2Received:
exists-trace
"
Ex id initiator responder payload1 payload2 #i #j #l .
(
Sent1(id, initiator, responder, payload1) @ #i &
Received1(id, responder, initiator, payload1) @ #j &
Sent2(id, responder, initiator, payload2) @ #j &
Received2(id, initiator, responder, payload2) @ #l &
#i < #j &
#j < #l
)
"
// correct session keys can be negotiated
lemma SessionEstablished:
exists-trace
"
Ex id initiator responder c1 c2 #i #j . (
Shared('initiator', id, initiator, responder, c1, c2) @ #i &
Shared('responder', id, responder, initiator, c1, c2) @ #j
)
"
// app data messages can be sent
lemma AppDataInitiator:
exists-trace
"
Ex id me them plaintext #t1 #t2 .
SentAppData('initiator', id, me, them, plaintext) @ #t1 &
ReceivedAppData('responder', id, them, me, plaintext) @ #t2 &
#t1 < #t2
"
lemma AppDataResponder:
exists-trace
"
Ex id me them plaintext #t1 #t2 .
SentAppData('responder', id, me, them, plaintext) @ #t1 &
ReceivedAppData('initiator', id, them, me, plaintext) @ #t2 &
#t1 < #t2
"
//
// Does the protocol makes sense?
// ==============================
// These lemmas check that some states can only happen only due to honest behavior.
// session keys are negotiated by honest peers => session was started by honest peers
lemma CorrectPathToFinal:
"
All id initiator responder c1 c2 #i #j . (
Shared('initiator', id, initiator, responder, c1, c2) @ #i &
Shared('responder', id, responder, initiator, c1, c2) @ #j
)
==>
(
Ex #k #l payload1.
Sent1(id, initiator, responder, payload1) @k &
Received1(id, responder, initiator, payload1) @ #l &
#k < #l &
#l = #j &
#j < #i
)
"
// app data is sent and received correctly => session was honest
lemma CorrectPathToAppDataInitiator:
"
All id responder initiator plaintext #t4 #t5 . (
SentAppData('responder', id, responder, initiator, plaintext) @ #t4 &
ReceivedAppData('initiator', id, initiator, responder, plaintext) @ #t5 &
#t4 < #t5
)
==>
(
Ex #t1 #t2 #t3 c1 c2 payload1.
Sent1(id, initiator, responder, payload1) @t1 &
Received1(id, responder, initiator, payload1) @ #t2 &
Shared('responder', id, responder, initiator, c1, c2) @ #t2 &
Shared('initiator', id, initiator, responder, c1, c2) @ #t3 &
#t1 < #t2 &
#t2 < #t3
)
"
///////////////////////////////////////
// Lemmas: Key Security
///////////////////////////////////////
//
// These are generic security properties that we expect from such protocols
//
// private keys of peers never leak from protocol attacks
lemma KeySecrecy:
"
All e_priv e_pub #i #j . (
// for all identities created (initiator or responder)
Identity(e_priv, e_pub) @ #i &
// where the private key of the identity is known to the attacker
K(e_priv) @ #j
) ==> Ex #k . (Reveal(e_pub) @ #k & #k < j) // it must be that it was revealed
"
// session keys cannot leak in honest protocol
lemma SessionSecrecy:
"
All id initiator responder init_priv resp_priv c1 c2 #i #j #t1 #t2 . (
// for all successful sessions between initiator and responder
Shared('responder', id, responder, initiator, c1, c2) @ #i &
Shared('initiator', id, initiator, responder, c1, c2) @ #j &
// where initiator and responder are honest actors
Identity(init_priv, initiator) @ #t1 & #t1 < #j &
Identity(resp_priv, responder) @ #t2 & #t2 < #i
) ==> (
// the adversary NEVER learns these session keys, even later
not ( (Ex #m . K(c1) @ #m) | (Ex #m . K(c2) @ #m) ) |
// or their keys were revealed before the session
(Ex #k . Reveal(initiator) @ #k & #k < #j) |
(Ex #k . Reveal(responder) @ #k & #k < #j)
)
"
// honest initiator can successfuly setup session with honest responder
lemma InitiatorSession:
"
All id initiator responder resp_priv c1 c2 #i #t2 . (
// all session the initiator successfuly negotiates
Shared('initiator', id, initiator, responder, c1, c2) @ #i &
// with an honest responder
Identity(resp_priv, responder) @ #t2 & #t2 < #i
)
==> (
// implies NO leakage of one of the session keys
not((Ex #k . K(c1) @ #k) | (Ex #k . K(c2) @ #k)) |
// or leakage of initiator ltk before the session happened
(Ex #k . Reveal(initiator) @ #k & #k < #i) |
// or leakage of the responder ltk before the session happened
(Ex #k . Reveal(responder) @ #k & #k < #i)
)
"
// honest responder can successfuly setup session with honest initiator
lemma ResponderSession:
"
All id initiator responder init_priv c1 c2 #i #t2 . (
// all session the responder successfuly negotiates
Shared('responder', id, responder, initiator, c1, c2) @ #i &
// with an honest initiator
Identity(init_priv, initiator) @ #t2 & #t2 < #i
) ==> (
// implies NO leakage of one of the session keys
not((Ex #k . K(c1) @ #k) | (Ex #k . K(c2) @ #k)) |
// or leakage of initiator ltk before the session happened
(Ex #k . Reveal(initiator) @ #k & #k < #i) |
// or leakage of the responder ltk before the session happened
(Ex #k . Reveal(responder) @ #k & #k < #i)
)
"
///////////////////////////////////////
// Lemmas: Payload Security Property
///////////////////////////////////////
//
// see the Noise Protocol Framework specification
// section 7.7. Payload security properties
//
// IK src dst
// <- s
// ...
// -> e, es, s, ss 1 2
// <- e, ee, se 2 4
// -> 2 5
// <- 2 5
//
// -> e, es, s, ss 1
// ===================
// Sender authentication vulnerable to key-compromise
// impersonation (KCI). The sender authentication is based
// on a static-static DH ("ss") involving both parties'
// static key pairs. If the recipient's long-term private key
// has been compromised, this authentication can be forged.
// Note that a future version of Noise might include signatures,
// which could improve this security property, but brings other
// trade-offs.
// sanity check:
// =============
// 1. if the responder static-key is compromised @ t1
// => Exists a payload1 @ t2 that is forged by an adversary who don't know the initiator's static-key
lemma payload1_src_1_check:
exists-trace
"
// if static public key of (honest) responder is compromised =>
All responder #i . Reveal(responder) @ #i
==>
Ex id initiator init_priv payload1 #t1 #t2 #t3 . (
// Exists an (honest) initiator
Identity(init_priv, initiator) @ #t1 &
// and payload1 is known to the adversary
K(payload1) @ #t2 & #i < #t2 & #t2 < #t3 &
// and it is received as coming from the initiator
Received1(id, responder, initiator, payload1) @ #t3 & #i < #t3 &
// and initiator did not sent payload1 to the responder
not (Ex #k . Sent1(id, initiator, responder, payload1) @ #k)
)
"
// proof:
// ======
// 1. for all sessions where both the initiator and responder are not corrupted => the adversary doesn't know the payload
/*
lemma payload1_src_1_proof:
"
All id initiator responder payload1 #i . (
// for all session
Received1(id, responder, initiator, payload1) @ #i &
// where initiator (if honest) was not compromised before
not (Ex #k . Reveal(initiator) @ #k & #k < #i) &
// and responder was not compromised before
not (Ex #k . Reveal(responder) @ #k & #k < #i)
) ==> (
// the payload1 cannot be known to the adversary
not (Ex #m . K(payload1) @ #m)
)
"
*/
// this should be equivalent:
lemma payload1_src_1_proof_eq:
"
All id initiator responder payload1 #i .
// for all session
Received1(id, responder, initiator, payload1) @ #i
==> (
// implies payload is not known to the adversary
not (Ex #m . K(payload1) @ #m) |
// or initiator (if honest) was compromised before the session happened
(Ex #k . Reveal(initiator) @ #k & #k < #i) |
// or responder was compromised before the session happened
(Ex #k . Reveal(responder) @ #k & #k < #i)
)
"
// -> e, es, s, ss 2
// =============================
// Encryption to a known recipient, forward secrecy for sender
// compromise only, vulnerable to replay. This payload is encrypted
// based only on DHs involving the recipient's static key pair.
// If the recipient's static private key is compromised, even at
// a later date, this payload can be decrypted. This message can also
// be replayed, since there's no ephemeral contribution from the recipient.
// sanity check:
// =============
// 1. responder ltk compromised at any time before or after payload was received => payload compromised
// 2. replay
lemma payload1_dst_2_check:
exists-trace
"
Ex id responder initiator payload1 #t1 #t3 #t4 #t5.
// payload1 sent honestly
Sent1(id, initiator, responder, payload1) @ #t1 &
// payload1 received honestly
Received1(id, responder, initiator, payload1) @ #t3 &
// the responder was not compromised (by Reveal at least)
not(Ex #t2 . Reveal(responder) @ #t2 & #t2 < #t3) &
// responder is then compromised (by Reveal)
Reveal(responder) @ #t4 & #t3 < #t4 &
// adversary learns payload1 after that
K(payload1) @ #t5 & #t4 < #t5
"
lemma payload1_replay_check:
exists-trace
"
Ex id responder initiator payload1 #i #j.
// for all payload1 received
Received1(id, responder, initiator, payload1) @ #i &
// exists the same payload1 received at a different time
Received1(id, responder, initiator, payload1) @ #j &
not #i = #j
"
// proof:
// ======
// 1. responder ltk compromised at any time before or after payload was received => payload compromised
// 2. replay
lemma payload1_dst_2_proof:
"
All id responder initiator payload1 #t1 #t2 . (
// payload1 received
Received1(id, responder, initiator, payload1) @ #t1 &
// payload1 known later
K(payload1) @ #t2 & #t1 < #t2 &
// but not before
not (Ex #t0 . K(payload1) @ #t0 & #t0 < #t1)
) ==> (
// must be because responder was compromised
Ex #t3 . Reveal(responder) @ #t3 & #t1 < #t3
)
"
lemma payload1_replay:
"
All id responder initiator payload1 #i .
// for all payload1 received
Received1(id, responder, initiator, payload1) @ #i ==> (
// exists the same payload1 received later
Ex #j . Received1(id, responder, initiator, payload1) @ #j & #i < #j
)
"
// <- e, ee, se 2
// ===================
// Sender authentication resistant to key-compromise impersonation (KCI).
// The sender authentication is based on an ephemeral-static DH
// ("es" or "se") between the sender's static key pair and the recipient's
// ephemeral key pair. Assuming the corresponding private keys are secure,
// this authentication cannot be forged.
// proof
// =====
// 1. compromise of payload2 can only mean that the responder WAS being impersonated
lemma payload2_src_2_proof:
"
All id initiator responder payload2 #t2 . (
// payload2 was received by an honest initiator
Received2(id, initiator, responder, payload2) @ #t2 &
// but was never sent honestly by the responder
not (Ex #t1 . Sent2(id, responder, initiator, payload2) @ #t1 & #t1 < #t2)
// (no need because there's always an honest responder)
// Identity(resp_priv, responder) @ #init
) ==> Ex #t0 . (
// implies that an honest responder leaked its key BEFORE
Reveal(responder) @ #t0 & #t0 < #t2
)
"
// <- e, ee, se 4
// =============================
// Encryption to a known recipient, weak forward secrecy if the sender's private
// key has been compromised. This payload is encrypted based on an ephemeral-ephemeral DH,
// and also based on an ephemeral-static DH involving the recipient's static key pair.
// However, the binding between the recipient's alleged ephemeral public and the
// recipient's static public key has only been verified based on DHs involving both
// those public keys and the sender's static private key. Thus, if the sender's
// static private key was previously compromised, the recipient's alleged ephemeral
// public key may have been forged by an active attacker. In this case, the attacker
// could later compromise the intended recipient's static private key to decrypt the
// payload (this is a variant of a "KCI" attack enabling a "weak forward secrecy" attack).
// Note that a future version of Noise might include signatures,
// which could improve this security property, but brings other trade-offs.
// proof:
// ======
// 1. if two honests participants end up having payload2 leaked,
// it MUST be because responder WAS compromised and initiator GETS compromised
// 2. payload is not replayable
lemma payload2_dst_4_proof:
"
All id initiator init_priv responder resp_priv payload2 #init_responder #init_initiator #t2 #t3 . (
// for all honest responder and initiator
Identity(resp_priv, responder) @ #init_responder &
Identity(init_priv, initiator) @ #init_initiator &
// when responder receives a payload2 to a (maybe fake) initiator
Sent2(id, responder, initiator, payload2) @ #t2 &
Received2(id, initiator, responder, payload2) @ #t3 & #t2 < #t3
) ==> (
// implies payload is never leaked
not (Ex #i . K(payload2) @ #i) |
(
Ex #t1 #i #j . (
// or it is leaked
K(payload2) @ #i &
// because responder was compromised before
K(resp_priv) @ #t1 & #t1 < #t2 &
// and initiator was compromised at some point
K(init_priv) @ #j
)
)
)
"
lemma payload2_replay:
"
All id responder initiator payload2 #i .
// for all payload1 received
Received2(id, initiator, responder, payload2) @ #i ==> not (
// exists the same payload1 received later
Ex #j . Received2(id, initiator, responder, payload2) @ #j & #i < #j
)
"
// -> 2
// ===================
// Sender authentication resistant to key-compromise impersonation (KCI).
// The sender authentication is based on an ephemeral-static DH
// ("es" or "se") between the sender's static key pair and the recipient's
// ephemeral key pair. Assuming the corresponding private keys are secure,
// this authentication cannot be forged.
// proof:
// ======
// 1. if two honests participants end up having app_data1 leaked,
// it MUST be because responder AND initiator ltk was leaked BEFORE
lemma initiatorAppData_src_2:
"
All id initiator responder plaintext #t1 #t2 #i. (
// for all correct sending of appdata
SentAppData('initiator', id, initiator, responder, plaintext) @ #t1 &
ReceivedAppData('responder', id, responder, initiator, plaintext) @ #t2 &
// and the data leaked before or later
K(plaintext) @ #i
) ==> (
// it implies that the responder or initiator were leaked BEFORE
(Ex #before . Reveal(responder) @ #before & #before < #t1) |
(Ex #before . Reveal(initiator) @ #before & #before < #t1)
)
"
///////////////////////////////////////
// Lemmas: Identity Hiding
///////////////////////////////////////
//
// see the Noise Protocol Framework specification
// section 7.8. Identity hiding
//
// initiator responder
// IK 4 3
//
// initiator 4:
// ============
// Encrypted to responder's static public key, without
// forward secrecy. If an attacker learns the responder's
// private key they can decrypt the initiator's public key.
lemma identity_initiator_4:
"
All initiator #t99 . (
// for all (honest) initiator that exist
(Ex id responder payload1 #i . Sent1(id, initiator, responder, payload1) @ #i) &
// and adversaries that know about this initiator's public key
K(initiator) @ #t99
) ==> (
// either reveal was called before
(Ex #k . Reveal(initiator) @ #k & #k < #t99) |
// or a responder (who had a session with the initiator) was breached
(Ex id responder payload1 #i #j . (
Received1(id, responder, initiator, payload1) @ #i & #i < #t99 &
Reveal(responder) @ #j & #j < #t99 &
not (responder = initiator)
)
)
)
"
// responder 3:
// ============
// Not transmitted, but a passive attacker can check candidates
// for the responder's private key and determine whether the
// candidate is correct. An attacker could also replay a
// previously-recorded message to a new responder and determine
// whether the two responders are the "same" (i.e. are using
// the same static key pair) by whether the recipient accepts
// the message.
// It looks like there is nothing we can prove here.
///////////////////////////////////////
end
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.