mpOTR_verif
===========

This is mpOTR protocol analysis wich is connected to another project:

https://github.com/maria-msu-seclab/mpotrDevelopment

mpOTR is a protocol for encrypted group communications with deniability 
feature. Current project aims to verify security properties of the protocol
and\or find the possible attacks.

The tool we use for protocol analysis and verification is Maude-NPA 
developed by University of Illinois at Urbana-Champaign:

http://maude.cs.uiuc.edu/tools/Maude-NPA/

We higly appreciate your ideas, questions and any other comments, see our 
info at AUTHORS


Work in progress:
 * Add initial grammars generated by Maude-NPA for faster search
 * Connection phase -- Done
 * Auth phase -- Done  
 * Need More Auth attacks (like impersonation)
 * Communication phase + OldBlue
 * Finilising phase -- make finalisation checks
 * Protocol as a whole
 * Overall attacks

 Questions: 
 * OldBlue : Do we send request to only one client or we broadcast it?
 * OldBlue : Do we send the response to only one lient or we broadcast it?
 	For both questions it seems like the answer is "broadcast" because that is
	what the channel (underlying protocol) allow us to do. Other ways will 
	require intelligent underlying protocol thus require making our own 
	channel protocol or limiting the usage of existing ones (not really
	desirable).
	* How to distinguish between the message itself and the second message 
	sended as a response for LostMessageRequest for those clients who
	have recieved the original one.
		We need some kind of flag. -- Done
 * What attacks we can do at Communication phase?
 
 * How to describe attack on the deniability feature?
   -- Some kind of that there is no connection between (s_i, S_i) and (x_i, y_i)
      mpCat draft && that paper, depends on the deniability definition.
 * How to describe attack on the PFC feature?
   -- No connection between long-term key and session simm key 
Ideas for previous two is 
      if intruder knows the long-term secret keys she cannot guess the 
	  session key (attack 0) and ephemeral private key (attack 2). Will this be equal to the 
	  abcence of a proof of that the certain long-term private key has 
	  participated in particular conversation?
 *	КАК ОПИСАТЬ, ЕСЛИ НАРУШИТЕЛЬ -- ОДИН ИЗ УЧАСТНИКОВ?? пОПРОБОВАТЬ ТАКИЕ АТАКИ.