Simple end-to-end encrypted voice calls. https://pages.codeberg.org/tok/talk
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 

178 lines
4.9 KiB

theory SPEKE
begin
//builtins: hashing, diffie-hellman, bilinear-pairing, symmetric-encryption
builtins: hashing, diffie-hellman, symmetric-encryption
// Chose a password that is shared by the two parties.
// The adversary does not yet know the password but
// could guess it because the password space is small.
rule choose_password:
[ Fr(~password) ]
--[ ChoosePassword(~password) ]->
[ !Password(~password) ]
//[ !Password(diff($passwordA, $passwordB)) ]
rule reveal_password:
[ !Password(pw) ]
--[ RevealPassword(pw) ]->
[ Out(pw) ]
// Generate key pair and send public key.
rule Initiator_1:
let
p = h(password)
//P = pmult(p, $BasePoint) // Compute another base point based on password.
//P = $BasePoint^p // Compute another base point based on password.
//pk_i = pmult(~sk_i, P) // Compute public key.
pk_i = p^~sk_i // Compute public key.
in
// Generate a fresh private key.
[ !Password(password), Fr(~sk_i) ]
--[ Initialize($I, ~sk_i) ]->
[ HandshakeI_1($I, ~sk_i), // Store key for next step.
Out(pk_i) // Send public key.
]
// Receive public key, generate key pair and send own public key.
// Compute shared secret.
rule Responder_1:
let
p = h(password)
//P = pmult(p, $BasePoint)
//P = $BasePoint^p
//pk_r = pmult(~sk_r, P) // Compute public key.
pk_r = p^~sk_r // Compute public key.
//s = pmult(~sk_r, pk_i) // Compute shared secret.
s = pk_i^~sk_r // Compute shared secret.
in
// Receive public key from network and generate a fresh key pair.
[ !Password(password), In(pk_i), Fr(~sk_r) ]
-->
// Send the public key and confirmation message.
[ Out(<pk_r, senc('ok', s)>), HandshakeR_1($R, s) ]
// Receive public key and compute shared secret.
// Send a confirmation message to the responder encrypted with the shared secret.
rule Initiator_2:
let
//s = pmult(sk_i, pk_r) // Shared secret.
s = pk_r^sk_i // Shared secret.
in
[ HandshakeI_1($I, sk_i), // Retreive initiator and secret key from previous step.
In(<pk_r, senc('ok', s)>) // Get public key and confirmation message from the network.
]
--[ SharedI($I, s) ]->
[ !SessionKey($I, s), Out(senc('ok', s)) ]
// Accept confirmation message.
// This completes the handshake.
rule Responder_2:
[ HandshakeR_1($R, s), In(senc('ok', s)) ]
--[ SharedR($R, s) ]->
[ !SessionKey($R, s) ]
// Send a data message encrypted with the session key.
rule SendMessage:
[ Fr(~msg), !SessionKey($I, key) ]
--[ SendMessage($I, ~msg, key) ]->
[ Out(senc(~msg, key)) ]
// Receive a data message encrypted with the session key.
rule ReceiveMessage:
[ In(senc(msg_plain, key)), !SessionKey($R, key) ]
--[ Received(msg_plain) ]->
[ ]
lemma Password_secrecy:
"
// It cannot be that
not(
Ex pw #i #j.
ChoosePassword(pw) @ #i & K(pw) @ #j // the adversary knows the shared password
& not (Ex #r. RevealPassword(pw) @ #r) // without the password having been revealed before.
)
"
// It is possible that initiator and responder end up
// with the same shared value. While initiator and
// responder are not the same entity.
lemma SPEKE_reachability_key_exchange:
exists-trace
" Ex I R s #i #j.
SharedR(R, s) @ #i
& SharedI(I, s) @ #j
& not(I = R)
"
lemma SPEKE_reachability_send_message:
exists-trace
" Ex msg #i.
Received(msg) @i
"
lemma SPEKE_shared_key_secrecy:
"
// It cannot be that
not(
Ex I R s #i #j #k.
// responder and initator share a key 's'
SharedR(R, s) @ #i
& SharedI(I, s) @ #j
// and the adversary knows 's'.
& K(s) @ #k
)
"
lemma SPEKE_initiator_shared_key_secrecy:
"
// It cannot be
not(
Ex I s #j #k.
// that the initator computed a shared key 's'
SharedI(I, s) @ #j
// and the adversary knows 's'
& K(s) @ #k
// without the password having been revealed.
& not (Ex pw #r. RevealPassword(pw) @ #r)
)
"
lemma SPEKE_responder_shared_key_secrecy:
"
// It cannot be
not(
Ex R s #j #k.
// that the responder computed a shared key 's'
SharedR(R, s) @ #j
// and the adversary knows 's'
& K(s) @ #k
// without the password having been revealed.
& not (Ex pw #r. RevealPassword(pw) @ #r)
)
"
lemma SPEKE_message_secrecy:
"
// It cannot be that
not(
Ex I msg key #j #k.
// the initiator sent a message
SendMessage(I, msg, key) @ #j
// and the adversary knows 'msg'
& K(msg) @ #k
// without the password having been leaked
& not (Ex pw #r. RevealPassword(pw) @ #r)
)
"
end