Symmetric-Key Encryption: Authenticated-To-Secure Channel

Alice wants to communicate q messages to Bob using an authenticated channel. The authenticated channel is not secure: it leaks each message to Eve, and waits to receive an ok message back from her before delivering the in-flight message. Thus, Eve cannot modify any of the messages but can read and delay them for any amount of time. To transmit information securely, Alice sends encryptions of her messages, which Bob decrypts using a shared key not known to Eve.

protocol real
protocol ideal + sim
declarations
new Key : key in
newfamily Recv[i < n] in
newfamily Send[i < n] in
newfamily LeakMsgRcvdIdAdv[i < n] in
newfamily OkMsgAdvId[i < n] in
IDEAL
SIM
N/A
new Key : key in
keygen
( Key ::= samp gen_keydistribution gen_key : unit -> key (()) )
( Key ::= samp gen_key (()) )
alice
( family Send[i < n] ::= 
    in : msg <- read In[i] ;
    k : key <- read Key ;
    samp encdistribution enc : msg * key -> ctxt ( (in, k) )
)
Leakage
( family LeakCtxtNetAdv[i < n] ::= 
    send : ctxt <- read Send[i] ; 
    return send
)
( family LeakCtxtNetAdv[i < n] ::= 
    x : unit <- read LeakMsgRcvdIdAdv[i] ;
    k : key <- read Key ;
    samp enc ( (zerosfunction zeros : unit -> msg(()), k) )
)
( family LeakMsgRcvdIdAdv[i < n] ::= 
    in : msg <- read In[i] ; 
    return ()
)
( family OkMsgAdvId[i < n] ::= 
    okCtxt : unit <- read OkCtxtAdvNet[i] ;
    return okCtxt
)
channel
( family Recv[i < n] ::= 
    okCtxt : unit <- read OkCtxtAdvNet[i] ;
    send : ctxt <- read Send[i] ;
    return send
)
bob
( family Out[i < n] ::=
    c : ctxt <- read Recv[i] ;
    k : key <- read Key ;
    return decfunction dec : ctxt * key -> msg((c, k))
)
( family Out[i < n] ::= 
    okMsg : unit <- read OkMsgAdvId[i] ;
    in : msg <- read In[i] ;
    return in
)

begin approx proof

start with real over delta input In[i < n] : msg ;
input OkCtxtAdvNet[i < n] : unit ;
output Out[i < n] : msg ;
output LeakCtxtNetAdv[i < n] : ctxt
subst fam Recv[i < n] into fam Out[i < n]
absorb fam Recv[i < n]
add internal family Dec[i < n] typed: msg assigned: k : key <- read Key ;
send : ctxt <- read Send [i] ;
return dec ( (send, k) )
add internal family Enc[i < n] typed: ctxt assigned: in : msg <- read In[i] ;
k : key <- read Key ;
samp enc ( (in, k) )
sym from change fam Send[i < n] with e : ctxt <- read Enc[i] ; return e
in currentProtocol(
   subst fam Enc[i < n] into fam Send[i < n]
)
sym from change fam Out[i < n] with okCtxt : unit <- read OkCtxtAdvNet[i] ;
d : msg <- read Dec[i] ;
return d
in currentProtocol(
   subst fam Dec[i < n] into fam Out[i < n]
)
subst fam Send[i < n] into fam LeakCtxtNetAdv[i < n]
subst fam Send[i < n] into fam Dec[i < n]
absorb fam Send[i < n]
compose fam Dec[i < n] with fam Enc[i < n] in group
in the presence of chn Key rewrite group Dec[i < n] and Enc[i < n] to (family Dec[i < n] ::= in : msg <- read In[i] ; return in) || (family Enc[i < n] ::= in : msg <- read In[i] ; k : key <- read Key ; samp enc ( (in, k) )) by induction on i bound B ( use assumption enc-dec-correctness(keyN ::= samp gen_key (()) ) ||
(encN ::= m : msg <- read inN ; k : key <- read keyN ; samp enc((m, k))) ||
(decN ::= c : ctxt <- read encN ; k : key <- read keyN ; return dec((c, k)))
=
(keyN ::= samp gen_key (()) ) ||
(encN ::= m : msg <- read inN ; k : key <- read keyN ; samp enc((m, k))) ||
(decN ::= in : msg <- read inN ; return in) on chn Key, chn Dec[B], chn Enc[B] )
decompose fam Dec[i < n] with fam Enc[i < n]
restructure (gather chn Key, fam Enc[i < n] from currentProtocol hiding chn Key)
use approx assumption cpanew Key : key in ((Key ::= samp gen_key (())) || (Enc[i < n] ::= m <- read In[i]; k <- read Key; samp enc((m, k))))
=
new Key : key in ((Key ::= samp gen_key (())) || (Enc[i < n] ::= m <- read In[i]; k <- read Key; samp enc((zeros(()), k))))
bring declarations of hidden channels in front
fold fam Enc[i < n] into fam LeakCtxtNetAdv[i < n]
fold fam Dec[i < n] into fam Out[i < n]
sym from idealPlusSim ( subst fam OkMsgAdvId[i < n] into fam Out[i < n] then
subst fam LeakMsgRcvdIdAdv[i < n] into fam LeakCtxtNetAdv[i < n] then
absorb fam LeakMsgRcvdIdAdv[i < n] then
absorb fam OkMsgAdvId[i < n] )
restructure idealPlusSim
check-proof idealPlusSim
show-bounds