# Forward secrecy via a fresh asymmetric key pair
#
# A -> B : { pub(K) }_LongTerm
# B -> A : { S }_pub{K}
# B -> A : { message }_S
# ...
# A -> * : LongTerm

# Run this as:
#   generate --apoc forward.proc > forward.rules
#   rewrite --batch forward.rules

Arities aenc 2, adec 2, pub 1, pri 1, enc 2, dec 2, cons 2, fst 1, snd 1,
        hash 1,
        message, message2, !OK!expected_hash, !OK!expected_message2 .

Expect 2.

# Asymmetric encryption

adec(aenc(M,pub(K)),pri(K)) => M .

# Symmetric encryption

dec(enc(M,K),K) => M .

# Pairs

fst(cons(X,Y)) => X .
snd(cons(X,Y)) => Y .

# The goal. message should not be disclosed, even after the LongTerm key is
# leaked.

| @_output : hash(M) , M : message => @zzResult : !OK!expected_hash .

| @_output       : message  => @zzResult : !FAIL! .
| @_zapoc_output : message  => @zzResult : !FAIL! .
| @_zapoc_output : message2 => @zzResult : !OK!expected_message2 .

%%

new LongTerm .
  ( # Participant A
    ! . new K .
    out enc(pub(K), LongTerm) .
    in KsessEnc . let Ksess = adec(KsessEnc,pri(K)) .
    in Message . let Message = dec(Message, Ksess) .
    out hash(Message) . ()
  | # Participant B
    ! .
    in PubKEnc . let PubK = dec(PubKEnc, LongTerm) .
    new Ksess .
    out aenc(Ksess, PubK) .
    out enc(message, Ksess) . ()
  | # Adversary
    ( ! . new Nonce . out Nonce . ()
    | ! . in X . in Y . out X . out Y .
             out aenc(X,Y) . out adec(X,Y) . 
             out enc(X,Y) . out dec(X,Y) . 
             out cons(X,Y) . out fst(X) . out snd(X) .
             out val(X) . out next(X) . ()
    ) 
  | # LongTerm key leak
    in Know . chk .
    ( # Reveal secret
      out LongTerm . out Know . ()
    | # Participant A
      ! . new K2 .
      out enc(pub(K2), LongTerm) .
      in KsessEnc2 . let Ksess2 = adec(KsessEnc2,pri(K2)) .
      in Message2 . let Message2 = dec(Message2, Ksess2) .
      out hash(Message2) . ()
    | # Participant B
      ! .
      in PubKEnc2 . let PubK2 = dec(PubKEnc2, LongTerm) .
      new Ksess2 .
      out aenc(Ksess2, PubK2) .
      out enc(message2, Ksess2) . ()
    | # Adversary
      ( ! . new Nonce . out Nonce . ()
      | ! . in X . in Y . out X . out Y .
            out aenc(X,Y) . out adec(X,Y) . 
	    out pri(X) . out pub(X) .
            out enc(X,Y) . out dec(X,Y) . 
            out cons(X,Y) . out fst(X) . out snd(X) . 
            out val(X) . out next(X) . ()
      )
    )
  )