# Common Crypto API Example

Arities enc 2, dec 2, cons 2, fst 1, snd 1, + 2, h 2,
        f1 3, f2 3, f3 3, f4 3, f5 2, f6 2,
        0, kp, km, data, pin, exp, imp, kek, k3, kek2, exp1, p, acc, forbidden.

# Encryption

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

# Rules for XOR

+(X,Y) => +(Y,X) .
+(+(X,Y),Z) => +(X,+(Y,Z)) .
+(0,X) => X .
+(X,X) => 0 .

# Left Associative Hash (no rules required)

# The six CCA operations f1 .. f6

# K_key_part_import_notcompleting
f1(X,Y,enc(Z,h(h(X,kp),km))) => enc(+(Z,Y),h(h(X,kp),km)) .

# K_key_part_import_notcompleting
f2(X,Y,enc(Z,h(h(X,kp),km))) => enc(+(Z,Y),h(X,km)) .

# K_key_import
f3(T,enc(K,h(imp,km)),enc(X,h(T,K))) => enc(X,h(T,km)) .

# K_key_export
f4(T,enc(K,h(exp,km)),enc(X,h(T,km))) => enc(X,h(T,K)) .

# K_key_encrypt_using_data_key
f5(X,enc(K,h(data,km))) => enc(X,K) .

# K_key_decrypt_using_data_key
f6(enc(X,K),enc(K,h(data,km))) => X .

# The goal.

kek        => forbidden .
km         => forbidden .
p          => forbidden .
enc(acc,p) => forbidden .

| @k : forbidden => @zzResult : !FAIL! .

%%

@public : data,pin,imp,k3,acc,kp.

@secret : km,kek,p,kek2,exp1 .

@forbidden : kek,km,p,enc(acc,p).

@k : 0 , 
     @public,
     enc(p,h(pin,kek)) ,
     enc(+(kek,k3),h(h(imp,kp),km)) ,
     enc(kek2, h(h(imp,kp),km)) ,
     enc(kek2, h(h(exp,kp),km)) ,
     enc(exp1, h(exp,km)) .

@k : +(@k,@k) , h(@k,@k) , 
     enc(@k,@k) , dec(@k,@k) ,
     f1(@k,@k,@k) , f2(@k,@k,@k) , 
     f3(@k,@k,@k) , f4(@k,@k,@k) ,
     f5(@k,@k) , f6(@k,@k) .