Public-Key Encryption: El Gamal

The El Gamal protocol is a CPA-secure public-key encryption schema based on the Diffie-Hellman Key Exchange. As in our previous case studies, Alice wants to communicate q messages to Bob using an authenticated channel. In the symmetric-key setting, the two parties had to agree on a secret shared key that was used both for encryption and decryption. In the public-key setting of El Gamal, Bob generates two keys: the public key is used for encryption and is known to both Alice and the adversary, whereas the secret key is used for decryption and known only to Bob.

protocol real
protocol ideal + sim
INIT
family Send[i < q] : msg * msg
family Recv[i < q] : msg * msg
new PublicKey : msg
new SecretKey : key
family SessionKey[i < q] : msg
family SecretEphemeralKey[i < q] : key
family LeakMsgRcvdIdAdv[i < q] : unit
family OkMsgAdvId[i < q] : msg
new PublicKey : msg
new SecretKey : key
family SecretEphemeralKey[i < q] : key
ideal
sim
Alice
(family SecretEphemeralKey[i < q] ::= 
    samp unif_key (()))
N/A
(family SecretEphemeralKey[i < q] ::= 
    samp unif_key (()))
(family PublicEphemeralKey[i < q] ::=
    ka : key <- read SecretEphemeralKey[i] ;
    return exp( (g(()), ka) ))
N/A
(family PublicEphemeralKey[i < q] ::=
    ka : key <- read SecretEphemeralKey[i] ;
    return exp( (g(()), ka) ))
(family SessionKey[i < q] ::=
    pb : msg <- read PublicKey ;
    ka : key <- read SecretEphemeralKey[i] ;
    return exp( (pb, ka) ))
N/A
N/A
(family Send[i < q] ::=
    m : msg <- read In[i] ;
    k : msg <- read SessionKey[i] ;
    pa : msg <- read PublicEphemeralKey[i] ;
    return ( pa, mul((m, k)) ))
N/A
N/A
Bob
( SecretKey ::= samp unif_key (()) )
N/A
( SecretKey ::= samp unif_key (()) )
(PublicKey ::= 
    kb : key <- read SecretKey ; 
    return exp( (g(()), kb) ))
N/A
(PublicKey ::= 
    kb : key <- read SecretKey ; 
    return exp( (g(()), kb) ))
(LeakPublicKeyRecAdv ::=
    pk : msg <- read PublicKey ;
    return pk)
N/A
(LeakPublicKeyRecAdv ::= read PublicKey)
(family Out[i < q] ::=
    r : msg * msg <- read Recv[i] ;
    kb : key <- read SecretKey ;       
    return mul( (snd r, inv( exp( (fst r, kb) ) )) ))
(family Out[i < q] ::=
    okm : msg <- read OkMsgAdvId[i] ;
    m : msg <- read In[i] ;
    return m)
N/A
Adversary
N/A
(family LeakMsgRcvdIdAdv[i < q] ::=
    m : msg <- read In[i] ;
    return ())
N/A
N/A
N/A
(family OkMsgAdvId[i < q] ::=
    okc : msg <- read OkCtxtAdvNet[i] ;
    return okc )
Auth. channel
(family LeakCtxtAdvNet[i < q] ::=
    s : msg * msg <- read Send[i] ;
    return s)
N/A
(family LeakCtxtAdvNet[i < q] ::=
    lmr : unit <- read LeakMsgRcvdIdAdv[i] ;
    pa : msg <- read PublicEphemeralKey[i] ;
    c : msg <- samp unif_msg (()) ;
    return (pa, c))
(family Recv[i < q] ::=
    okc : msg <- read OkCtxtAdvNet[i] ;
    s : msg * msg <- read Send[i] ;
    return s)
N/A
N/A

begin approx proof

start with real over delta
subst fam Send[bound q] into fam Recv[bound q]
fold fam Send[bound q] into fam LeakCtxtAdvNet[bound q]
fold fam Recv[bound q] into fam Out[bound q]
subst fam SessionKey[bound q] into fam Out[bound q]
subst chn PublicKey into fam Out[bound q]
subst fam PublicEphemeralKey[bound q] into fam Out[bound q]
use expression assumption commute on fam Out[bound q] at 1
drop read chn SecretKey from fam Out[bound q]
drop read fam SecretEphemeralKey[bound q] from fam Out[bound q]
fold chn SecretKey into chn PublicKey
sym from change fam PublicEphemeralKey[bound q] with pb : msg <- read PublicKey ; ka : key <- read SecretEphemeralKey[i] ; return exp((g(()), ka)) in currentProtocol ( drop read chn PublicKey from fam PublicEphemeralKey[bound q] )
add internal family DDH2 indices: i bounds: bound q typed: msg * msg assigned: pb : msg <- read PublicKey ; ka : key <- read SecretEphemeralKey[i] ; return ( exp((g(()), ka)) , exp((pb, ka)) )
sym from change fam PublicEphemeralKey[bound q] with x : msg * msg <- read DDH2[i] ; return fst x in currentProtocol ( subst fam DDH2[bound q] into fam PublicEphemeralKey[bound q] )
sym from change fam SessionKey[bound q] with x : msg * msg <- read DDH2[i] ; return snd x in currentProtocol ( subst fam DDH2[bound q] into fam SessionKey[bound q] )
fold fam SecretEphemeralKey[bound q] into fam DDH2[bound q] then-approx
in the presence of chn PublicKey rewrite family DDH2[bound q] to preNF(nil, ka : key <- samp unif_key(()) ; kr : key <- samp unif_key(()) ; return(exp((g(()), ka)), exp((g(()), kr))) ) by generalization of rewriteDDH2 then-approx
sym from change fam DDH2[bound q] with ka : key <- read SecretEphemeralKey[i] ; kr : key <- read Key[i] ; return(exp((g(()), ka)), exp((g(()), kr))) in extend ( extend currentProtocol with internal family SecretEphemeralKey indices: i bounds: bound q typed: key assigned: samp unif_key(()) ) with internal family Key indices: i bounds: bound q typed: key assigned: samp unif_key(()) ( fold fam Key[bound q] into fam DDH2[bound q] then fold fam SecretEphemeralKey[bound q] into fam DDH2[bound q] )
subst fam DDH2[bound q] into fam PublicEphemeralKey[bound q]
fold fam DDH2[bound q] into fam SessionKey[bound q]
drop read fam Key[bound q] from fam PublicEphemeralKey[bound q]
drop read fam SecretEphemeralKey[bound q] from fam SessionKey[bound q]
sym from change chn PublicKey with kb : key <- read SecretKey ; return exp((g(()), kb)) in extend currentProtocol with internal channel SecretKey typed: key assigned: samp unif_key(()) ( fold chn SecretKey into chn PublicKey )
fold fam Key[bound q] into fam SessionKey[bound q]
use assumption sampExp on fam SessionKey[bound q]
add internal family Enc indices: i bounds: bound q typed: msg assigned: k : msg <- read SessionKey[i] ; m : msg <- read In[i] ; return mul((m, k))
sym from change fam LeakCtxtAdvNet[bound q] with c : msg <- read Enc[i] ; pa : msg <- read PublicEphemeralKey[i] ; return(pa, c) in currentProtocol( subst fam Enc[bound q] into fam LeakCtxtAdvNet[bound q] )
fold fam SessionKey[bound q] into fam Enc[bound q]
use assumption mulFixedMsg on fam Enc[bound q]
fold fam Enc[bound q] into fam LeakCtxtAdvNet[bound q]
sym from idealPlusSim( fold fam OkMsgAdvId[bound q] into fam Out[bound q] then fold fam LeakMsgRcvdIdAdv[bound q] into fam LeakCtxtAdvNet[bound q] )
check-proof idealPlusSim