- IPDL Protocol Equivalence - Full Content

Diffie-Hellman Key Exchange (DHKE) + One-Time Pad (OTP)

In symmetric-key encryption, the sender (Alice) and the receiver (Bob) need to agree on a shared secret key. One such key-agreement protocol is the Diffie-Hellman Key Exchange (DHKE). We then use the Diffie-Hellman Key Exchange protocol to turn an authenticated channel into a one-time pad that delivers a single secret message from Alice to Bob.

protocol real
protocol ideal + sim
INIT
new SecretKey-Alice : key in
new SecretKey-Bob : key in
new Send-Alice-Bob : msg in
new Send-Bob-Alice : msg in
new Recv-Alice-Bob : msg in
new Recv-Bob-Alice : msg in
new OkKey-AliceAdvId : msg in
new OkKey-BobAdvId : msg in
ideal
sim
new SharedKey : msg in
new SecretKey-Alice : key in
new SecretKey-Bob : key in
new PublicKey-Alice : msg in
new PublicKey-Bob : msg in
Alice
( SecretKey-Alice ::= samp unif_keydistribution unif_key : unit -> key(()) )
N/A
( SecretKey-Alice ::= samp unif_keydistribution unif_key : unit -> key(()) )
( Send-Alice-Bob ::= ka : key <- read SecretKey-Alice ;
     return expfunction exp : msg * key -> msg( (gfunction g : unit -> msg(()), ka) ) )
N/A
N/A
N/A
N/A
( PublicKey-Alice ::= ka : key <- read SecretKey-Alice ;
     return expfunction exp : msg * key -> msg( (gfunction g : unit -> msg(()), ka) ) )
( LeakPublicKey-AliceAdvNet ::= sa : msg <- read Send-Alice-Bob ;
     return sa )
N/A
( LeakPublicKey-AliceAdvNet ::= pka : msg <- read PublicKey-Alice ;
     return pka )
( Key-Alice ::= rb : msg <- read Recv-Bob-Alice ; 
     ka : key <- read SecretKey-Alice ;
     return expfunction exp : msg * key -> msg( (rb, ka) ) )
( Key-Alice ::= oka : msg <- read OkKey-AliceAdvId ;
     sk : msg <- read SharedKey ; return sk )
N/A
N/A
N/A
( OkKey-AliceAdvId ::= ob : msg <- read OkPublicKey-BobAdvNet ;
     return ob )
Bob
( SecretKey-Bob ::= samp unif_keydistribution unif_key : unit -> key(()) )
N/A
( SecretKey-Bob ::= samp unif_keydistribution unif_key : unit -> key(()) )
( Send-Bob-Alice ::= kb : key <- read SecretKey-Bob ;
     return expfunction exp : msg * key -> msg( (gfunction g : unit -> msg(()), kb) ) )
N/A
N/A
N/A
N/A
( PublicKey-Bob ::= kb : key <- read SecretKey-Bob ;
     return expfunction exp : msg * key -> msg( (gfunction g : unit -> msg(()), kb) ) )
( LeakPublicKey-BobAdvNet ::= sb : msg <- read Send-Bob-Alice ;
     return sb )
N/A
( LeakPublicKey-BobAdvNet ::= pkb : msg <- read PublicKey-Bob ;
     return pkb )
( Key-Bob ::= ra : msg <- read Recv-Alice-Bob ; 
     kb : key <- read SecretKey-Bob ;
     return expfunction exp : msg * key -> msg( (ra, kb) ) )
( Key-Bob ::= okb : msg <- read OkKey-BobAdvId ;
     sk : msg <- read SharedKey ; return sk )
N/A
N/A
N/A
( OkKey-BobAdvId ::= oa : msg <- read OkPublicKey-AliceAdvNet ;
     return oa )
Shared
N/A
( SharedKey ::= samp unif_msgdistribution unif_msg : unit -> msg(()) )
N/A

begin approx proof

start with realOTP over deltainput OkCtxtAdvNet : msg ; input In : msg ; input OkPublicKey-AliceAdvNet : msg ; input OkPublicKey-BobAdvNet : msg ; output LeakCtxtNetAdv : msg ; output LeakPublicKey-AliceAdvNet : msg ; output LeakPublicKey-BobAdvNet : msg ; output Out : msg
fold chn Recv into chn Out
subst chn Send into chn Out
fold chn Send into chn LeakCtxtNetAdv
restructure
(gather
chn SecretKey-Alice, chn SecretKey-Bob,
chn Send-Alice-Bob, chn Send-Bob-Alice,
chn Recv-Bob-Alice, chn Recv-Alice-Bob,
chn Key-Alice, chn Key-Bob,
chn LeakPublicKey-AliceAdvNet, chn LeakPublicKey-BobAdvNet
from currentProtocol
hiding
chn SecretKey-Alice, chn SecretKey-Bob,
chn Send-Alice-Bob, chn Send-Bob-Alice,
chn Recv-Bob-Alice, chn Recv-Alice-Bob) then-approx
call-approx dhkeProof then-approx
bring declarations of hidden channels in front
subst chn Key-Alice into chn LeakCtxtNetAdv
fold chn Key-Alice into chn Out
fold chn Key-Bob into chn Out
drop read chn SharedKey from chn Out
fold chn SharedKey into chn LeakCtxtNetAdv
use assumption mulFixedMsgk : msg <- samp unif_msg(()) ;
return mul((m, k))
=
samp unif_msg(()) on chn LeakCtxtNetAdv
sym from idealPlusSimOTP(
fold chn OkMsgAdvId into chn Out then
fold chn LeakMsgRcvdIdAdv into chn LeakCtxtNetAdv
)
restructure idealPlusSimOTP
check-proof idealPlusSimOTP

current-protocol
show-bounds