(* 3 Formalization of LINE encryption (1:n) *) (* overview group members: Client1, Client2, client3 Client1: -- group key geneneraotr upload public key to messaging server -- generate group shared key compute encrypted group shared keys for Client2, Client3 upload these keys to messaging server -- receive, group message decrypt the message Client2: -- group message sender upload public key to messaging server -- download encrypted group shared key decrypt the key encrypt a group mesage with group shared key send encrypted group message to Client1, Client3 Client3: upload public key to messaging server -- receive, group message download encrypted group shared key decrypt the message MessagingServer: manage publc keys manage encrypted group shared keys *) set traceBacktracking = false. (* Rules for ECDH key exchange *) type G. (* type of generator *) type scalar. (* type of scalar *) type basis. (* type of base points *) fun Ggen(basis):G. (* convert base point to generator *) fun sca(scalar,G):G. (* scalar multiplication *) equation forall a:scalar, b:scalar, P:basis; sca(a,sca(b,Ggen(P)))=sca(b,sca(a,Ggen(P))). (* commutativity *) (* Types *) type key. type iv. (* Rules for AES-CBC *) fun senccbc(bitstring,key,iv):bitstring. (* encryption function *) reduc forall m:bitstring, k:key, i:iv; sdeccbc(senccbc(m,k,i),k,i)=m. (* decryption function *) (* Rules for AES-ECB *) fun sencecb(bitstring,key):bitstring. (* encryption function *) reduc forall m:bitstring, k:key; sdececb(sencecb(m,k),k)=m. (* decryption function *) (* Rules for SHA256 *) fun Hash(bitstring):bitstring. (* hash function *) (* Rules for unknown algorithm to encrypt/decrypt group shared key *) fun ENC(scalar, G):bitstring. reduc forall k:G, x:scalar; DEC(ENC(x, k), k) = x. (* Rules for XOR *) fun xor(bitstring,bitstring):bitstring. equation forall x:bitstring, y:bitstring; xor(xor(x,y),y)=x. equation forall x:bitstring; xor(x,xor(x,x))=x. equation forall x:bitstring; xor(xor(x,x),x)=x. equation forall x:bitstring, y:bitstring; xor(y,xor(x,x))=y. equation forall x:bitstring, y:bitstring; xor(xor(x,y),xor(x,x))=xor(x,y). equation forall x:bitstring, y:bitstring; xor(xor(x,y),xor(y,y))=xor(x,y). (* Rules for subbitstring -- not explaned on the paper -- *) fun breakf(bitstring):bitstring. fun breakb(bitstring):bitstring. (* Rules for type conversion *) fun ToKey(bitstring):key. (* convert bitstring type to key type *) fun ToIV(bitstring):iv. (* convert bitstring type to iv type *) (* Types *) type coins. type ID. type version. type ContentType. (* Constants *) const J:basis[data]. const Key:bitstring[data]. const IV:bitstring[data]. const ver:version[data]. const contentType:ContentType[data]. (* Declaration of channel and secret *) free c:channel. (* channel *) free c_pr:channel[private]. (* private channel to share groupKeyID *) free M:bitstring[private]. (* client's secret information *) (* Verification of Secrecy and Authenticity *) (* Secrecy of message *) query attacker(M). (* Events *) event Client1_term1(key, iv, ID, ID). (* msesageSenderID, message, senderID, groupKeyID *) event Client1_term2(key, iv, ID, ID). (* msesageSenderID, message, senderID, groupKeyID *) event Client2_accept(key, iv, ID, ID). (* msesageSenderID, message, senderID, groupKeyID *) event Client3_term(key, iv, ID, ID). (* msesageSenderID, message, senderID, groupKeyID *) (* query k:key, v:iv, senderID:ID, groupKeyID:ID; event(Client1_term1(k, v, senderID, groupKeyID)). query k:key, v:iv, senderID:ID, groupKeyID:ID; event(Client1_term2(k, v, senderID, groupKeyID)). query k:key, v:iv, senderID:ID, groupKeyID:ID; event(Client2_accept(k, v, senderID, groupKeyID)). query k:key, v:iv, senderID:ID, groupKeyID:ID; event(Client3_term(k, v, senderID, groupKeyID)). *) (* Authenticity *) query k:key, v:iv, senderID:ID, groupKeyID:ID; inj-event(Client3_term(k, v, senderID, groupKeyID)) ==> inj-event(Client2_accept(k, v, senderID, groupKeyID)). query k:key, v:iv, senderID:ID, groupKeyID:ID; inj-event(Client1_term1(k, v, senderID, groupKeyID)) ==> inj-event(Client2_accept(k, v, senderID, groupKeyID)). (* Abstract TEP model *) type TEPSessionKey. fun TEPENC(TEPSessionKey, bitstring): bitstring. reduc forall k:TEPSessionKey, x:bitstring; TEPDEC(k, TEPENC(k, x)) = x. const Client1TEPSessionKey: TEPSessionKey[private]. const Client2TEPSessionKey: TEPSessionKey[private]. const Client3TEPSessionKey: TEPSessionKey[private]. const AttackerTEPSessionKey: TEPSessionKey. (* Messaging Server *) type MessagingServerMessageType. const RegisterPublicKey: MessagingServerMessageType. const ResponseRegisterPublicKey: MessagingServerMessageType. const QueryPublicKey: MessagingServerMessageType. const ResponsePublicKey: MessagingServerMessageType. const RegisterGroupKey2: MessagingServerMessageType. const ResponseGroupKeyID: MessagingServerMessageType. const QueryGroupKey: MessagingServerMessageType. const ResponseGroupKey: MessagingServerMessageType. table publickey_table(ID, G). table groupkey_table(ID, ID, bitstring, ID). (* (encryptedFor, encryptedBy, groupKeyEncrypted, groupKeyID) *) let MessagingServer_register(msg:bitstring, sessionKey:TEPSessionKey) = let decrypted: bitstring = TEPDEC(sessionKey, msg) in let (=RegisterPublicKey, id:ID, pubKey:G, nonce:coins) = decrypted in ( get publickey_table(=id, k:G) in 0 (* already registered *) else ( insert publickey_table(id, pubKey); out(c, TEPENC(sessionKey, (ResponseRegisterPublicKey, id, nonce))) ) ) else let (=RegisterGroupKey2, groupKeyID:ID, encryptedBy:ID, (encryptedFor1:ID, groupKeyEncrypted1:bitstring), (encryptedFor2:ID, groupKeyEncrypted2:bitstring), nonce:coins) = decrypted in ( get groupkey_table(=encryptedFor1, =encryptedBy, k1:bitstring, =groupKeyID) in 0 (* already registered *) else get groupkey_table(=encryptedFor2, =encryptedBy, k2:bitstring, =groupKeyID) in 0 (* already registered *) else insert groupkey_table(encryptedFor1, encryptedBy, groupKeyEncrypted1, groupKeyID); insert groupkey_table(encryptedFor2, encryptedBy, groupKeyEncrypted2, groupKeyID); out(c, TEPENC(sessionKey, (ResponseGroupKeyID, groupKeyID, nonce))) ). let MessagingServer_query(msg:bitstring, sessionKey:TEPSessionKey) = let decrypted: bitstring = TEPDEC(sessionKey, msg) in let (=QueryPublicKey, id:ID, nonce:coins) = decrypted in ( get publickey_table(=id, pubKey:G) in out(c, TEPENC(sessionKey, (ResponsePublicKey, id, pubKey, nonce))) ) else let (=QueryGroupKey, groupKeyID:ID, encryptedFor:ID, nonce:coins) = decrypted in ( get groupkey_table(=encryptedFor, encryptedBy:ID, groupKeyEncrypted:bitstring, =groupKeyID) in out(c, TEPENC(sessionKey, (ResponseGroupKey, encryptedFor, encryptedBy, groupKeyEncrypted, groupKeyID, nonce))) ). let MessagingServer() = !( in(c, msg:bitstring); ( MessagingServer_register(msg, Client1TEPSessionKey) | MessagingServer_register(msg, Client2TEPSessionKey) | MessagingServer_register(msg, Client3TEPSessionKey) | (* MessagingServer_register(msg, AttackerTEPSessionKey) | *) MessagingServer_query(msg, Client1TEPSessionKey) | MessagingServer_query(msg, Client2TEPSessionKey) | MessagingServer_query(msg, Client3TEPSessionKey) | MessagingServer_query(msg, AttackerTEPSessionKey) ) ). (* Client1 subprocess *) let Client1(c1id:ID, c2id:ID, c3id:ID) = (* register public key *) new c1cpr:scalar; let c1cpu = sca(c1cpr, Ggen(J)) in new n0: coins; out(c, TEPENC(Client1TEPSessionKey, (RegisterPublicKey, c1id, c1cpu, n0))); in(c, msg0:bitstring); let (=ResponseRegisterPublicKey, =c1id, =n0) = TEPDEC(Client1TEPSessionKey, msg0) in out(c, c1id); (* compute group shared key *) new sharedKey_gr:scalar; (* let sharedKey_gr_pu:G = sca(SharedKey_gr, Ggen(J)) in -- unused -- *) (* get public key of c2 *) new n1: coins; out(c, TEPENC(Client1TEPSessionKey, (QueryPublicKey, c2id, n1))); in(c, msg1:bitstring); let (=ResponsePublicKey, =c2id, c2cpu:G, =n1) = TEPDEC(Client1TEPSessionKey, msg1) in (* get public key of c3 *) new n2:coins; out(c, TEPENC(Client1TEPSessionKey, (QueryPublicKey, c3id, n2))); in(c, msg2:bitstring); let (=ResponsePublicKey, =c3id, c3cpu:G, =n2) = TEPDEC(Client1TEPSessionKey, msg2) in (* register group shared key *) let key12:G = sca(c1cpr, c2cpu) in let key13:G = sca(c1cpr, c3cpu) in let sharedKey_gr_en12:bitstring = ENC(sharedKey_gr, key12) in let sharedKey_gr_en13:bitstring = ENC(sharedKey_gr, key13) in new groupKeyID: ID; new n3:coins; out(c, TEPENC(Client1TEPSessionKey, (RegisterGroupKey2, groupKeyID, c1id, (c2id, sharedKey_gr_en12), (c3id, sharedKey_gr_en13), n3))); in(c, msg3:bitstring); let (=ResponseGroupKeyID, =groupKeyID, =n3) = TEPDEC(Client1TEPSessionKey, msg3) in (* share groupKeyID *) out(c_pr, groupKeyID); !( (* receive group message (from c2) *) in(c, (=ver, =contentType, salt:coins, C:bitstring, mac:bitstring, senderID:ID, groupKeyID':ID)); if (groupKeyID = groupKeyID') then ( (* get public key of user who send message *) new n4: coins; out(c, TEPENC(Client3TEPSessionKey, (QueryPublicKey, senderID, n4))); in(c, msg4:bitstring); let (=ResponsePublicKey, =senderID, cycpu:G, =n4) = TEPDEC(Client3TEPSessionKey, msg4) in let sharedSecret_gr = sca(sharedKey_gr, cycpu) in (* decrypt message *) let Ken:key = ToKey(Hash((sharedSecret_gr, salt, Key))) in let MACp:bitstring = Hash(C) in let MACe:bitstring = sencecb(xor(breakf(MACp), breakb(MACp)), Ken) in if (mac = MACe) then ( let IVpre:bitstring = Hash((sharedSecret_gr, salt, IV)) in let IVen:iv = ToIV(xor(breakf(IVpre), breakb(IVpre))) in let M':bitstring = sdeccbc(C, Ken, IVen) in event Client1_term1(Ken, IVen, senderID, groupKeyID) ) ) else ( (* -- this arm will not be completed in this scenario -- *) (* get encrypted groupKey *) new n4:coins; out(c, TEPENC(Client1TEPSessionKey, (QueryGroupKey, groupKeyID', c1id, n4))); in(c, msg4:bitstring); let (=ResponseGroupKey, =c1id, encryptedBy:ID, sharedKey_gr_en:bitstring, =groupKeyID', =n4) = TEPDEC(Client1TEPSessionKey, msg4) in (* get public key of user who encrypt groupKey *) new n5: coins; out(c, TEPENC(Client1TEPSessionKey, (QueryPublicKey, encryptedBy, n5))); in(c, msg5:bitstring); let (=ResponsePublicKey, =encryptedBy, cxcpu:G, =n5) = TEPDEC(Client1TEPSessionKey, msg5) in (* compute group key *) let key1x:G = sca(c1cpr, cxcpu) in let sharedKey_gr':scalar = DEC(sharedKey_gr_en, key1x) in (* get public key of user who send message *) new n6: coins; out(c, TEPENC(Client1TEPSessionKey, (QueryPublicKey, senderID, n6))); in(c, msg6:bitstring); let (=ResponsePublicKey, =encryptedBy, cycpu:G, =n6) = TEPDEC(Client1TEPSessionKey, msg5) in let sharedSecret_gr = sca(sharedKey_gr', cycpu) in (* decrypt message *) let Ken':key = ToKey(Hash((sharedSecret_gr, salt, Key))) in let MACp':bitstring = Hash(C) in let MACe':bitstring = sencecb(xor(breakf(MACp'), breakb(MACp')), Ken') in if (mac = MACe') then ( let IVpre:bitstring = Hash((sharedSecret_gr, salt, IV)) in let IVen:iv = ToIV(xor(breakf(IVpre), breakb(IVpre))) in let M':bitstring = sdeccbc(C, Ken', IVen) in event Client1_term2(Ken', IVen, senderID, groupKeyID) ) ) ). (* Client2 subprocess *) let Client2(c1id:ID, c2id:ID, c3id:ID) = (* register public key *) new c2cpr:scalar; let c2cpu = sca(c2cpr, Ggen(J)) in new n0: coins; out(c, TEPENC(Client2TEPSessionKey, (RegisterPublicKey, c2id, c2cpu, n0))); in(c, msg0:bitstring); let (=ResponseRegisterPublicKey, =c2id, =n0) = TEPDEC(Client2TEPSessionKey, msg0) in out(c, c2id); (* share groupKeyID *) in(c_pr, groupKeyID:ID); (* get encrypted groupKey *) new n1:coins; out(c, TEPENC(Client2TEPSessionKey, (QueryGroupKey, groupKeyID, c2id, n1))); in(c, msg1:bitstring); let (=ResponseGroupKey, =c2id, encryptedBy:ID, sharedKey_gr_en:bitstring, =groupKeyID, =n1) = TEPDEC(Client2TEPSessionKey, msg1) in (* get public key of user who encrypt groupKey *) new n2:coins; out(c, TEPENC(Client2TEPSessionKey, (QueryPublicKey, encryptedBy, n2))); in(c, msg2:bitstring); let (=ResponsePublicKey, =encryptedBy, cxcpu:G, =n2) = TEPDEC(Client2TEPSessionKey, msg2) in (* compute group key *) let key2x:G = sca(c2cpr, cxcpu) in let sharedKey_gr:scalar = DEC(sharedKey_gr_en, key2x) in !( (* encrypt message *) let sharedSecret_gr = sca(sharedKey_gr, c2cpu) in new salt:coins; let Ken:key = ToKey(Hash((sharedSecret_gr, salt, Key))) in let IVpre:bitstring = Hash((sharedSecret_gr, salt, IV)) in let IVen:iv = ToIV(xor(breakf(IVpre), breakb(IVpre))) in let C:bitstring = senccbc(M, Ken, IVen) in let MACp:bitstring = Hash(C) in let MACe:bitstring = sencecb(xor(breakf(MACp), breakb(MACp)), Ken) in (* send group message *) event Client2_accept(Ken, IVen, c2id, groupKeyID); out(c, (ver, contentType, salt, C, MACe, c2id, groupKeyID)) ). (* Client3 subprocess *) let Client3(c3id:ID) = (* register public key *) new c3cpr:scalar; let c3cpu = sca(c3cpr, Ggen(J)) in new n0: coins; out(c, TEPENC(Client3TEPSessionKey, (RegisterPublicKey, c3id, c3cpu, n0))); in(c, msg0:bitstring); let (=ResponseRegisterPublicKey, =c3id, =n0) = TEPDEC(Client3TEPSessionKey, msg0) in out(c, c3id); (* share groupKeyID *) in(c_pr, groupKeyID:ID); !( (* receive encrypted group message (from c2) *) in(c, (=ver, =contentType, salt:coins, C:bitstring, mac:bitstring, senderID:ID, =groupKeyID)); new n1:coins; out(c, TEPENC(Client3TEPSessionKey, (QueryGroupKey, groupKeyID, c3id, n1))); in(c, msg1:bitstring); let (=ResponseGroupKey, =c3id, encryptedBy:ID, sharedKey_gr_en:bitstring, =groupKeyID, =n1) = TEPDEC(Client3TEPSessionKey, msg1) in (* get public key of user who encrypt groupKey *) new n2:coins; out(c, TEPENC(Client3TEPSessionKey, (QueryPublicKey, encryptedBy, n2))); in(c, msg2:bitstring); let (=ResponsePublicKey, =encryptedBy, cxcpu:G, =n2) = TEPDEC(Client3TEPSessionKey, msg2) in (* compute group key *) let key3x:G = sca(c3cpr, cxcpu) in let sharedKey_gr:scalar = DEC(sharedKey_gr_en, key3x) in (* get public key of user who send message *) new n3: coins; out(c, TEPENC(Client3TEPSessionKey, (QueryPublicKey, senderID, n3))); in(c, msg3:bitstring); let (=ResponsePublicKey, =senderID, cycpu:G, =n3) = TEPDEC(Client3TEPSessionKey, msg3) in let sharedSecret_gr = sca(sharedKey_gr, cycpu) in (* decrypt message *) let Ken:key = ToKey(Hash((sharedSecret_gr, salt, Key))) in let MACp:bitstring = Hash(C) in let MACe:bitstring = sencecb(xor(breakf(MACp), breakb(MACp)), Ken) in if (mac = MACe) then ( let IVpre:bitstring = Hash((sharedSecret_gr, salt, IV)) in let IVen:iv = ToIV(xor(breakf(IVpre), breakb(IVpre))) in let M':bitstring = sdeccbc(C, Ken, IVen) in event Client3_term(Ken, IVen, senderID, groupKeyID) ) ). (* Main process *) process new c1id:ID; new c2id:ID; new c3id:ID; ( Client1(c1id, c2id, c3id) | Client2(c1id, c2id, c3id) | Client3( c3id) | MessagingServer() )