***( The informal journal-level description of this protocol is as follows: *** Taken from an e-mail by Cathy!!! In this protocol, Alice and Bob each have secret data DA and DB. There is a function f(DA,DB) that they want to have computed, but 1- They cannot compute it themselves 2- Even if they could, they don't want to share their data with each other There is a server that can compute f, but they don't want the server to see DA and DB either. The server is assumed to be "honest but curious", that is, it is trusted to follow the rules of the protocol, but it will try to find out everything it can about DA and DB in the process. The protocol uses three public key algorithms. One, hpke is homomorphic with respect to f. The second, pke, is a regular pubic key encryption algorithm. The third, sign, is a digital signature algorithm. Unlike the three encryption algorithms in the last example, whose choice was completely arbitrary, the use of these three algorithms is motivated by their roles in the protocol. The protocol works as follows. 1. A and B share public and private key pairs for the algorithm hpke. Encryption of message M with hpke is thus modeled as hpke(M,k(A,B)). 2. A,B, and the server s are all able to digitally sign their messages using algorithm sign 3. The server possesses a public and private key pair for algorithm pke The protocol is as follows A -> B : sign( B ; NA ; pke( hpke (DA, k(A,B)), s ),A) B -> A : sign( NA ; NB ; pke( hpke (DB, k(A,B)), s ),B) A -> s : sign( A ; B ; NA ; NB ; pke(hpke(DA,k(A,B)),s) ; pke(hpke(DB,k(A,B)), s), A) s -> A,B : sign( A ; B ; NA ; NB ; f( hpke(DA,k(A,B)) , hpke(DB,k(A,B)) ), s) It has the following flaw when A and B final messages do not ask for f(X3,X4) from the server: A -> I_B : sign( B ; NA ; pke( hpke (DA, k(A,B)), s ),A) I_B -> B : sign( B ; NA ; XE, i) B -> A : sign( NA ; NB ; pke( hpke (DB, k(i,B)), s ),B) A -> s : sign( A ; B ; NA ; NB ; pke(hpke(DA,k(A,B)),s) ; pke(hpke(DB,k(i,B)), s), A) s -> A,B : sign( A ; B ; NA ; NB ; f( hpke(DA,k(A,B)) , hpke(DB,k(i,B)) ), s) The protocol may or may not have other flaws. If it does, it would be interesting to see what happens wrt Maude-NPA. I also think I've got a way to model the "honest-but-curious" behavior of the server in Maude-NPA so that it can be demonstrated that the server doesn't learn the secret data. If this is the case, it would be a new contribution of the paper, because I don't believe anyone has tried to model honest-but curious in a Dolev-Yao based tool before. )*** fmod PROTOCOL-EXAMPLE-SYMBOLS is --- Importing sorts Msg, Fresh, Public, and GhostData protecting DEFINITION-PROTOCOL-RULES . ---------------------------------------------------------- --- Overwrite this module with the syntax of your protocol --- Notes: --- * Sort Msg and Fresh are special and imported --- * Every sort must be a subsort of Msg --- * No sort can be a supersort of Msg ---------------------------------------------------------- --- Sort Information sorts Name Nonce Pkey Data Enc Sign HEnc . subsorts Nonce Pkey Data Name Enc Sign HEnc < Msg . subsort Name < Public . --- Nonce operators op n : Name Fresh -> Nonce [frozen] . op data : Name Fresh -> Data [frozen] . --- Principals op a : -> Name . --- Alice op b : -> Name . --- Bob op s : -> Name . --- Server op i : -> Name . --- Intruder --- Concatenation operator op _;_ : Msg Msg -> Msg [gather (e E) frozen] . --- Public and Private Key operators op pkey : Name Name -> Pkey [frozen] . --- f operator op f : Msg Msg -> HEnc [frozen] . --- Encryption Operators op pke : Msg Name -> Enc [frozen] . op hpke : Msg Pkey -> HEnc [frozen] . op sign : Msg Name -> Sign [frozen] . endfm fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS . ---------------------------------------------------------- --- Overwrite this module with the algebraic properties --- of your protocol ---------------------------------------------------------- vars X Y : Msg . var K : Pkey . ***Homomorphic encryption over f eq hpke(f(X,Y) , K) = f(hpke(X , K) , hpke(Y , K)) [nonexec label homomorphism metadata "builtin-unify"] . endfm fmod PROTOCOL-SPECIFICATION is protecting PROTOCOL-EXAMPLE-SYMBOLS . protecting DEFINITION-PROTOCOL-RULES . protecting DEFINITION-CONSTRAINTS-INPUT . ---------------------------------------------------------- --- Overwrite this module with the strands --- of your protocol ---------------------------------------------------------- vars X Y Z W : Msg . vars X1 X2 X3 X4 : HEnc . vars Y1 Y2 : Enc . vars Z1 Z2 : Sign . vars X' Y' Z' V' W' : Msg . vars r r' r'' r1 r2 r3 r4 : Fresh . vars N N1 N2 : Nonce . vars V P A B : Name . eq STRANDS-DOLEVYAO = :: nil :: [ nil | -(X), -(Y), +(X ; Y), nil ] & :: nil :: [ nil | -(X ; Y), +(X), nil ] & :: nil :: [ nil | -(X ; Y), +(Y), nil ] & :: nil :: [ nil | -(X), -(A), +(pke(X, A)), nil ] & :: nil :: [ nil | -(pke(X,i)), +(X), nil ] & :: nil :: [ nil | -(X), +(sign(X,i)), nil ] & :: nil :: [ nil | -(sign(X,A)), +(X), nil ] & :: nil :: [ nil | -(X), -(A), -(B), +(hpke(X,pkey(A,B))), nil ] & :: nil :: [ nil | -(hpke(X,pkey(A,i))), +(X), nil ] & :: nil :: [ nil | -(hpke(X,pkey(i,B))), +(X), nil ] & :: nil :: [ nil | +(A), nil ] [nonexec] . eq STRANDS-PROTOCOL = :: r, r' :: *** Alice *** [ nil | +(sign( B ; n(A,r) ; pke(hpke(data(A,r'),pkey(A,B)),s),A)), -(sign( n(A,r) ; N ; Y1 , B)), +(sign( A ; B ; n(A,r) ; N ; pke(hpke(data(A,r'),pkey(A,B)),s) ; Y1 , A)), -(sign( A ; B ; n(A,r) ; N ; X1 , s )) , nil ] & :: r, r' :: ***Bob *** [ nil | -(sign( B ; N1 ; Y2, A)), +(sign( N1 ; n(B,r) ; pke(hpke(data(B,r'),pkey(A,B)),s), B)), -(sign( A ; B ; N1 ; n(B,r) ; X2, s )) , nil ] & :: nil :: *** Server *** [ nil | -(sign( A ; B ; N1 ; N2 ; pke(X3 , s) ; pke(X4 , s) , A)), +(sign( A ; B ; N1 ; N2 ; f(X3,X4) , s)) , nil ] [nonexec] . eq ATTACK-STATE(0) = :: r, r' :: *** Alice *** [ nil , +(sign( b ; n(a,r) ; pke(hpke (data(a,r'),pkey(a,b)),s),a)), -(sign( n(a,r) ; N ; Y1 ,b )), +(sign( a ; b ; n(a,r) ; N ; pke(hpke (data(a,r'),pkey(a,b)),s) ; Y1 , a)), -(sign( a ; b ; n(a,r) ; N ; X1 , s )) | nil ] || empty || nil || nil || never( *** Authentication *** :: r1, r2 :: ***Bob *** [ nil | -(sign( b ; n(a,r) ; pke(hpke(data(a,r'),pkey(a,b)),s), a)), +(sign( n(a,r) ; n(b,r1) ; pke(hpke(data(b,r2),pkey(a,b)),s), b)), nil ] & S:StrandSet || IK:IntruderKnowledge) [nonexec] . endfm --- THIS HAS TO BE THE LAST LOADED MODULE !!!! select MAUDE-NPA .