/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
*
* ludovic.apvrille AT enst.fr
*
* This software is a computer program whose purpose is to allow the
* edition of TURTLE analysis, design and deployment diagrams, to
* allow the generation of RT-LOTOS or Java code from this diagram,
* and at last to allow the analysis of formal validation traces
* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
* from INRIA Rhone-Alpes.
*
* This software is governed by the CeCILL license under French law and
* abiding by the rules of distribution of free software. You can use,
* modify and/ or redistribute the software under the terms of the CeCILL
* license as circulated by CEA, CNRS and INRIA at the following URL
* "http://www.cecill.info".
*
* As a counterpart to the access to the source code and rights to copy,
* modify and redistribute granted by the license, users are provided only
* with a limited warranty and the software's author, the holder of the
* economic rights, and the successive licensors have only limited
* liability.
*
* In this respect, the user's attention is drawn to the risks associated
* with loading, using, modifying and/or developing or reproducing the
* software by the user in light of its specific status of free software,
* that may mean that it is complicated to manipulate, and that also
* therefore means that it is reserved for developers and experienced
* professionals having in-depth computer knowledge. Users are therefore
* encouraged to load and test the software's suitability as regards their
* requirements in conditions enabling the security of their systems and/or
* data to be ensured and, more generally, to use and operate it in the
* same conditions as regards security.
*
* The fact that you are presently reading this means that you have had
* knowledge of the CeCILL license and that you accept its terms.
*/
package proverifspec;
import avatartranslator.toproverif.AVATAR2ProVerif;
import myutil.TraceManager;
import ui.AvatarDesignPanel;
import ui.TAttribute;
import ui.avatarbd.AvatarBDBlock;
import java.io.BufferedWriter;
import java.io.IOException;
import java.util.HashMap;
import java.util.LinkedList;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
/**
* Class ProVerifResultTrace
* Creation: 22/05/2017
* @version 1.0 22/05/2017
* @author Florian LUGOU
*/
public class ProVerifResultTrace {
private static Pattern tracePattern;
private static Pattern blockNamePattern;
private static Pattern attrPattern;
private LinkedList<ProVerifResultTraceStep> trace;
private StringBuilder buffer;
private LinkedList<String> proverifProcess;
private HashMap<String, Integer> attackerNamesMap;
static
{
ProVerifResultTrace.attrPattern = Pattern.compile("\\b((\\w+?)" + AVATAR2ProVerif.ATTR_DELIM + ")?(\\w+?)(" + AVATAR2ProVerif.ATTR_DELIM + "[0-9_]+?)?(_\\d+)?\\b(\\[[^\\]]*\\])?");
ProVerifResultTrace.tracePattern = Pattern.compile("^\\d+\\. (.*)$");
ProVerifResultTrace.blockNamePattern = Pattern.compile("let \\(=sessionID,=call" + AVATAR2ProVerif.ATTR_DELIM + "(.+?)" + AVATAR2ProVerif.ATTR_DELIM + ".*");
}
private class OutStep implements ProVerifResultTraceStep {
private String from;
private String to;
private String message;
private String channel;
public OutStep(String from, String to, String message, String channel) {
this.from = from;
this.to = to;
this.message = message;
this.channel = channel;
}
public boolean messageEquals(String message)
{
return this.message.equals(message);
}
public void setTo(String to)
{
this.to = to;
}
public boolean isToAttacker()
{
return this.to.equals("Attacker");
}
@Override
public String describeAsString(AvatarDesignPanel adp)
{
return "MSG " + this.from + " -- " + this.channel + " --> " + this.to + " : " + ProVerifResultTrace.this.replaceAllAttributeNames(adp, this.message).replaceAll(",", ", ");
}
@Override
public void describeAsSDTransaction(AvatarDesignPanel adp, BufferedWriter writer, int step) throws IOException
{
writer.write("#" + step + " time=0.000000000 block=" + this.from + " blockdestination=" + this.to + " type=synchro channel=" + this.channel + " params=\"" + ProVerifResultTrace.this.replaceAllAttributeNames(adp, this.message).replaceAll(",", ", ") + "\"");
writer.newLine();
writer.flush();
}
@Override
public void describeAsTMLSDTransaction(BufferedWriter writer, int step) throws IOException
{
writer.write("#" + step + " time=0.000000000 block=" + this.from + " blockdestination=" + this.to + " type=synchro channel=" + this.channel + " params=\"" + this.message.replaceAll(",", ", ") + "\"");
writer.newLine();
writer.flush();
}
}
private class EventStep implements ProVerifResultTraceStep {
private String block;
private String name;
public EventStep (String block, String name)
{
this.block = block;
this.name = name;
}
@Override
public String describeAsString(AvatarDesignPanel adp)
{
return "EV " + this.block + "." + this.name;
}
@Override
public void describeAsSDTransaction(AvatarDesignPanel adp, BufferedWriter writer, int step) throws IOException
{
writer.write("#" + step + " time=0.000000000 block=" + this.block + " type=state_entering state="+ this.name);
writer.newLine();
writer.flush();
}
@Override
public void describeAsTMLSDTransaction(BufferedWriter writer, int step) throws IOException
{
writer.write("#" + step + " time=0.000000000 block=" + this.block + " type=state_entering state="+ this.name);
writer.newLine();
writer.flush();
}
}
private class NewStep implements ProVerifResultTraceStep {
private String name;
public NewStep(String name)
{
this.name = name;
}
@Override
public String describeAsString(AvatarDesignPanel adp)
{
return "NEW " + ProVerifResultTrace.this.replaceAttributeName(adp, this.name);
}
@Override
public void describeAsSDTransaction(AvatarDesignPanel adp, BufferedWriter writer, int step) throws IOException
{
writer.write("#" + step + " time=0.000000000 block=Attacker type=function_call func=new parameters=" + ProVerifResultTrace.this.replaceAttributeName(adp, this.name));
writer.newLine();
writer.flush();
}
@Override
public void describeAsTMLSDTransaction(BufferedWriter writer, int step) throws IOException
{
writer.write("#" + step + " time=0.000000000 block=Attacker type=function_call func=new parameters=" + this.name);
writer.newLine();
writer.flush();
}
}
public ProVerifResultTrace(LinkedList<String> proverifProcess)
{
this.proverifProcess = proverifProcess;
this.trace = new LinkedList<ProVerifResultTraceStep> ();
this.attackerNamesMap = new HashMap<String, Integer> ();
this.buffer = null;
}
public LinkedList<ProVerifResultTraceStep> getTrace()
{
return this.trace;
}
public void addTraceStep(String str)
{
Matcher m = tracePattern.matcher(str);
if (m.matches())
{
this.finalizeStep();
this.buffer = new StringBuilder();
str = m.group(1);
}
this.buffer.append(str);
}
private String replaceAttributeName(AvatarDesignPanel adp, String str)
{
Matcher m = ProVerifResultTrace.attrPattern.matcher(str);
if (m.matches())
{
String part1 = m.group(2);
String part2 = m.group(3);
Integer s;
if (part1 == null) {
part1 = "Attacker";
s = this.attackerNamesMap.get(part1 + AVATAR2ProVerif.ATTR_DELIM + str);
if (s == null)
return str;
}
else
{
s = this.attackerNamesMap.get(str);
if (s != null)
{
String [] spl = str.split(AVATAR2ProVerif.ATTR_DELIM, 3);
part1 = spl[0];
part2 = spl[1];
}
}
String blockPart = "Attacker";
String attrPart = part2;
if (!part1.equals("Attacker"))
{
// TODO: why is it just name and not FQN ?
AvatarBDBlock block = adp.getAvatarBDPanel().getBlockFromOwnerName(part1.replaceAll("__", "."));
if (block == null)
{
TraceManager.addDev("[ERROR] Unknown block : " + part1);
return null;
}
if (s == null)
blockPart = block.getOwnerName();
String attrName[] = part2.split("__", 2);
if (attrName.length >= 2)
{
TAttribute attr = block.getAttributeByName(attrName[0]);
if (attr == null)
{
// TODO: can happen when library function ?
TraceManager.addDev("[ERROR] Unknown attribute : " + part2 + " for block " + block.getOwnerName());
attrPart = part2.replaceAll("__", ".");
}
else
{
// TODO: is it possible that subtype is itself composed ?
LinkedList<TAttribute> types = adp.getAvatarBDPanel().getAttributesOfDataType(attr.getTypeOther());
if (types.size() > 1)
attrPart = attrName[0] + "." + attrName[1];
else
attrPart = attrName[0];
}
}
}
if (s != null && s.intValue() > 0)
attrPart += "_" + s;
return blockPart + "." + attrPart;
}
return str;
}
private String replaceAllAttributeNames(AvatarDesignPanel adp, String str)
{
Matcher m = ProVerifResultTrace.attrPattern.matcher(str);
String result = "";
int lastEnd = 0;
while (m.find(lastEnd))
{
result += str.substring(lastEnd, m.start());
result += this.replaceAttributeName(adp, m.group(0));
lastEnd = m.end();
}
result += str.substring(lastEnd);
// Replace pk(...)
Pattern p = Pattern.compile("pk\\(([a-zA-Z0-9_.]+)\\)");
m = p.matcher(result);
lastEnd = 0;
str = "";
while (m.find(lastEnd))
{
String replaceBy = m.group(0);
for (String pragma: adp.getModelPragmas())
{
String parts[] = pragma.split("\\s+");
if (!parts[0].equals("#PrivatePublicKeys") || parts.length < 4)
continue;
if (m.group(1).equals(parts[1] + "." + parts[2]))
{
replaceBy = parts[1] + "." + parts[3];
break;
}
}
str += result.substring(lastEnd, m.start());
str += replaceBy;
lastEnd = m.end();
}
str += result.substring(lastEnd);
return str;
}
private String getBlockNameFromLine(int line)
{
for (int i=line; i>=0; i--)
{
Matcher m = blockNamePattern.matcher(this.proverifProcess.get(i));
if (m.matches())
{
return m.group(1).replaceAll("__", ".");
}
}
// This can happen when out(pk(...)) in no process due to pragma PrivatePublicKey
return null;
}
private String consumePrecondition(String str)
{
try {
Pattern p = Pattern.compile("The message (.+?) that the attacker may have by (.+?) may be received at input \\{(.+?)\\}\\.(.*)");
Matcher m = p.matcher(str);
if (m.matches())
{
String msgName = m.group(1);
if (msgName.startsWith("chControlEnc")
|| msgName.startsWith("strong" + AVATAR2ProVerif.ATTR_DELIM)
|| msgName.startsWith("choice" + AVATAR2ProVerif.ATTR_DELIM))
return m.group(4);
String channelName = "";
Matcher m2 = Pattern.compile(AVATAR2ProVerif.CH_ENCRYPT + ".+?__(.+?)\\((.*)\\)").matcher(msgName);
if (m2.matches())
{
channelName = m2.group(1);
msgName = m2.group(2);
}
boolean foundAStep = false;
for (ProVerifResultTraceStep step: this.trace)
{
if (step instanceof OutStep)
{
OutStep out = (OutStep) step;
if (out.messageEquals(msgName) && out.isToAttacker())
{
foundAStep = true;
out.setTo(this.getBlockNameFromLine(Integer.parseInt(m.group(3))));
break;
}
// TODO: ProVerif does not output twice the out in case of weak authenticity violation...
// It can only be seen in the trace reconstruction phase.
}
}
if (!foundAStep)
{
this.trace.add(new OutStep("Attacker", this.getBlockNameFromLine(Integer.parseInt(m.group(3))), msgName, channelName));
}
return m.group(4);
}
p = Pattern.compile("We have (.+?)\\.(.*)");
m = p.matcher(str);
if (m.matches())
{
return m.group(2);
}
p = Pattern.compile("The event (.+?)( \\(with environment .+?)? may be executed at \\{(.+?)\\}\\.(.*)");
m = p.matcher(str);
if (m.matches())
{
return m.group(4);
}
} catch (NumberFormatException e) {
TraceManager.addDev("[ERROR] Parsing int");
}
return null;
}
private void finalizeStep()
{
if (this.buffer == null)
return;
String str = this.buffer.toString();
String newStr = str;
while (newStr != null)
{
str = newStr;
newStr = this.consumePrecondition(newStr);
}
if (str.startsWith("By "))
{
return;
}
try {
Pattern p = Pattern.compile("(So t|T)he message (.*) may be sent (.*) at output \\{(\\d+)\\}.*");
Matcher m = p.matcher(str);
if (m.matches())
{
String msgName = m.group(2);
if (msgName.startsWith("strong" + AVATAR2ProVerif.ATTR_DELIM)
|| msgName.startsWith("choice" + AVATAR2ProVerif.ATTR_DELIM)
|| msgName.startsWith("chControlEnc"))
return;
String blockName = this.getBlockNameFromLine(Integer.parseInt(m.group(4)));
String channelName = "";
m = Pattern.compile(AVATAR2ProVerif.CH_ENCRYPT + ".+?__(.+?)\\((.*)\\)").matcher(msgName);
if (m.matches())
{
channelName = m.group(1);
msgName = m.group(2);
}
if (blockName != null)
this.trace.add(new OutStep(blockName, "Attacker", msgName, channelName));
return;
}
p = Pattern.compile("So event (.*) may be executed at \\{(\\d+)\\}( in session .+)?\\..*");
m = p.matcher(str);
if (m.matches())
{
String line = m.group(2);
p = Pattern.compile("enteringState" + AVATAR2ProVerif.ATTR_DELIM + "[a-zA-Z0-9_]+" + AVATAR2ProVerif.ATTR_DELIM + "([a-zA-Z0-9_]+)");
m = p.matcher(m.group(1));
if (m.matches())
{
this.trace.add(new EventStep(this.getBlockNameFromLine(Integer.parseInt(line)), m.group(1)));
return;
}
return;
}
p = Pattern.compile("The attacker has some term (.*)\\.attacker\\(\\1\\)\\.");
m = p.matcher(str);
p = Pattern.compile("We assume as hypothesis thatattacker\\((\\w*)\\)\\.");
Matcher m2 = p.matcher(str);
if (m.matches() || m2.matches())
{
String attrName;
if (m.matches())
attrName = m.group(1);
else
attrName = m2.group(1);
String attrName2 = attrName;
if (attrName.startsWith("strong" + AVATAR2ProVerif.ATTR_DELIM)
|| attrName.startsWith("choice" + AVATAR2ProVerif.ATTR_DELIM))
return;
m = ProVerifResultTrace.attrPattern.matcher(attrName);
if (m.matches())
{
String newName = m.group(3);
if (!attrName.contains(AVATAR2ProVerif.ATTR_DELIM))
attrName = "Attacker" + AVATAR2ProVerif.ATTR_DELIM + attrName;
int n = 0;
for (String k: this.attackerNamesMap.keySet())
{
if (newName.equals(k.split(AVATAR2ProVerif.ATTR_DELIM, 3)[1]))
{
if (this.attackerNamesMap.get(k) == 0)
{
this.attackerNamesMap.remove(k);
this.attackerNamesMap.put(k, new Integer("1"));
n = 2;
break;
}
else
{
int nn = this.attackerNamesMap.get(k).intValue();
if (nn >= n)
n = nn+1;
}
}
}
this.attackerNamesMap.put(attrName, new Integer(n));
this.trace.add(new NewStep(attrName2));
}
return;
}
} catch (NumberFormatException e) {
TraceManager.addDev("[ERROR] Parsing int");
}
TraceManager.addDev("[DEBUG] unmatch: " + str);
}
public void finalize()
{
this.finalizeStep();
}
}