diff --git a/src/avatartranslator/AvatarPragma.java b/src/avatartranslator/AvatarPragma.java index 5103cdfea6a811a994f7432a732f65ea19962529..773072105df94c56eafb0c6ab1f0c8c2c6db5c88 100644 --- a/src/avatartranslator/AvatarPragma.java +++ b/src/avatartranslator/AvatarPragma.java @@ -51,9 +51,9 @@ import myutil.*; import ui.*; public abstract class AvatarPragma extends AvatarElement { - private final String[] PRAGMAS = {"Confidentiality", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Public", "Constant"}; - private final String[] PRAGMAS_TRANSLATION = {"Secret", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Public", "Constant"}; - private LinkedList<AvatarAttribute> arguments; + private final String[] PRAGMAS = {"Confidentiality", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Public", "PublicConstant", "PrivateConstant"}; + private final String[] PRAGMAS_TRANSLATION = {"Secret", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Public", "PublicConstant", "PrivateConstant"}; + protected LinkedList<AvatarAttribute> arguments; private int proofStatus = 0; @@ -148,12 +148,19 @@ public abstract class AvatarPragma extends AvatarElement { return pragmas; } } - else if (header.equals("Constant")){ + else if (header.equals("PrivateConstant")){ LinkedList<AvatarConstant> constants = new LinkedList<AvatarConstant>(); for (String arg: args){ constants.add(new AvatarConstant(arg, obj)); } - pragmas.add(new AvatarPragmaConstant(str, obj, constants)); + pragmas.add(new AvatarPragmaConstant(str, obj, constants, false)); + } + else if (header.equals("PublicConstant")){ + LinkedList<AvatarConstant> constants = new LinkedList<AvatarConstant>(); + for (String arg: args){ + constants.add(new AvatarConstant(arg, obj)); + } + pragmas.add(new AvatarPragmaConstant(str, obj, constants, true)); } else if (header.equals("PrivatePublicKeys")){ LinkedList<AvatarAttribute> attrs = new LinkedList<AvatarAttribute>(); diff --git a/src/avatartranslator/AvatarPragmaConstant.java b/src/avatartranslator/AvatarPragmaConstant.java index 05230cd307eb8e2959b189996eaa3c143c14519b..e7e3774e79c00d8b2316ba5d6d5de58abd7da803 100644 --- a/src/avatartranslator/AvatarPragmaConstant.java +++ b/src/avatartranslator/AvatarPragmaConstant.java @@ -52,18 +52,32 @@ import myutil.*; public class AvatarPragmaConstant extends AvatarPragma { - private LinkedList<AvatarAttribute> arguments; private LinkedList<AvatarConstant> constants; + private boolean isPublic; - public AvatarPragmaConstant(String _name, Object _referenceObject, LinkedList<AvatarConstant> _consts){ + public AvatarPragmaConstant(String _name, Object _referenceObject, LinkedList<AvatarConstant> _consts, boolean _isPublic){ super(_name, _referenceObject); arguments = new LinkedList<AvatarAttribute>(); constants = _consts; + this.isPublic = _isPublic; } - public LinkedList<AvatarAttribute> getArgs(){ - return arguments; - } + public LinkedList<AvatarConstant> getConstants() { return constants; } + + public AvatarConstant getConstantWithName (String name) { + for (AvatarConstant c: this.constants) + if (c.getName ().equals (name)) + return c; + return null; + } + + public boolean hasConstantWithName (String name) { + return this.getConstantWithName (name) != null; + } + + public boolean isPublic () { + return this.isPublic; + } } diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java index c70f2d38a0ed3e2b7100103c23c01cc191589d10..b4e132c990eb3c2de4d43d3e8ac80b464953464b 100755 --- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java +++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java @@ -57,6 +57,7 @@ import javax.xml.parsers.*; import ui.ConfigurationTTool; import ui.CheckingError; import ui.AvatarDesignPanel; +import ui.window.JDialogProVerifGeneration; import ui.TGComponent; import proverifspec.*; import myutil.*; @@ -111,7 +112,7 @@ public class AVATAR2ProVerif implements AvatarTranslator { private int dummyDataCounter; - private boolean stateReachability; + private int stateReachability; private Vector warnings; @@ -165,7 +166,7 @@ public class AVATAR2ProVerif implements AvatarTranslator { return this.avspec; } - public ProVerifSpec generateProVerif(boolean _debug, boolean _optimize, boolean _stateReachability, boolean _typed) { + public ProVerifSpec generateProVerif(boolean _debug, boolean _optimize, int _stateReachability, boolean _typed) { this.stateReachability = _stateReachability; this.warnings = new Vector(); @@ -474,18 +475,15 @@ public class AVATAR2ProVerif implements AvatarTranslator { this.spec.addDeclaration (new ProVerifVar ("call__" + block.getName() + "__" + simplifiedElements.get (asme), "bitstring", true)); } - this.spec.addDeclaration (new ProVerifComment ("Data")); + this.spec.addDeclaration (new ProVerifComment ("Constants")); TraceManager.addDev("Constants"); - for (AvatarPragma pragma: this.avspec.getPragmas ()) { - TraceManager.addDev("Pragma " + pragma.toString ()); - + for (AvatarPragma pragma: this.avspec.getPragmas ()) if (pragma instanceof AvatarPragmaConstant) for (AvatarConstant constant: ((AvatarPragmaConstant) pragma).getConstants ()) { String constName = constant.getName (); TraceManager.addDev("| " + constName); - this.spec.addDeclaration (new ProVerifConst (constName, "bitstring")); + this.spec.addDeclaration (new ProVerifVar (constName, "bitstring", ! ((AvatarPragmaConstant) pragma).isPublic ())); } - } /* Secrecy Assumptions */ this.secrecyChecked = new HashSet<AvatarAttribute> (); @@ -530,9 +528,9 @@ public class AVATAR2ProVerif implements AvatarTranslator { } // Queries for states - if (this.stateReachability) { + TraceManager.addDev ("Queries Event (" + (this.stateReachability == JDialogProVerifGeneration.REACHABILITY_ALL ? "ALL" : this.stateReachability == JDialogProVerifGeneration.REACHABILITY_SELECTED ? "SELECTED" : "NONE") + ")"); + if (this.stateReachability != JDialogProVerifGeneration.REACHABILITY_NONE) { this.spec.addDeclaration (new ProVerifComment ("Queries Event")); - TraceManager.addDev ("Queries Event"); for (AvatarBlock block: this.avspec.getListOfBlocks ()) { HashSet<AvatarStateMachineElement> visited = new HashSet<AvatarStateMachineElement> (); LinkedList<AvatarStateMachineElement> toVisit = new LinkedList<AvatarStateMachineElement> (); @@ -543,7 +541,7 @@ public class AVATAR2ProVerif implements AvatarTranslator { continue; visited.add (asme); - if (asme instanceof AvatarState) { + if (asme instanceof AvatarState && (this.stateReachability == JDialogProVerifGeneration.REACHABILITY_ALL || ((AvatarState) asme).isCheckable ())) { this.spec.addDeclaration (new ProVerifQueryEv (new ProVerifVar[] {}, "enteringState__" + block.getName() + "__" + asme.getName())); this.spec.addDeclaration (new ProVerifEvDecl ("enteringState__" + block.getName() + "__" + asme.getName(), new String[] {})); TraceManager.addDev("| event (enteringState__" + block.getName() + "__" + asme.getName() + ")"); @@ -604,6 +602,22 @@ public class AVATAR2ProVerif implements AvatarTranslator { this.nameEquivalence = new HashMap<AvatarAttribute, AvatarAttribute> (); + TraceManager.addDev("Finding constants"); + for (AvatarBlock block: blocks) + for (AvatarAttribute attr: block.getAttributes ()) + if (this.avspec.getAvatarConstantWithName (attr.getName ()) != null) { + if (attr.isInt () || attr.isBool ()) { + lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, null), "bitstring")}, attr.getName ())); + systemKnowledge.add (attr); + } else { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Attribute " + attr.getBlock ().getName () + "." + attr.getName () + " should be of type int or bool to be considered as a constant."); + ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarBDPanel()); + ce.setTGComponent((TGComponent)attr.getReferenceObject()); + warnings.add(ce); + continue; + } + } + TraceManager.addDev("Finding system knowledge"); for (AvatarPragma pragma: this.avspec.getPragmas ()) // Check if pragma is system initial knowledge @@ -613,7 +627,7 @@ public class AVATAR2ProVerif implements AvatarTranslator { for (AvatarAttribute arg: pragma.getArgs ()) { // ignore if the attribute was already declared if (systemKnowledge.contains (arg)) { - CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Attribute " + arg.getBlock ().getName () + "." + arg.getName () + " already appears in another initial knowledge pragma (ignored)."); + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Attribute " + arg.getBlock ().getName () + "." + arg.getName () + " already appears in another initial knowledge pragma or is a constant (ignored)."); ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarBDPanel()); ce.setTGComponent((TGComponent)pragma.getReferenceObject()); warnings.add(ce); @@ -1241,7 +1255,8 @@ public class AVATAR2ProVerif implements AvatarTranslator { ProVerifTranslatorParameter arg = (ProVerifTranslatorParameter) _arg; ProVerifProcInstr _lastInstr = arg.lastInstr; - if (this.stateReachability) + if (this.stateReachability == JDialogProVerifGeneration.REACHABILITY_ALL || + (this.stateReachability == JDialogProVerifGeneration.REACHABILITY_SELECTED && _asme.isCheckable ())) // Adding an event for reachability of the state _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("event enteringState__" + arg.block.getName() + "__" + _asme.getName() + "()", true)); diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java index 70f92570dee59c29c8993dcbab03fdde69aa024b..63fe936e165cf622e7bd594e391bb89f1b4d0605 100644 --- a/src/ui/AvatarDesignPanelTranslator.java +++ b/src/ui/AvatarDesignPanelTranslator.java @@ -59,8 +59,8 @@ import ui.window.*; public class AvatarDesignPanelTranslator { - private final String[] PRAGMAS = {"Confidentiality", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Constant"}; - private final String[] PRAGMAS_TRANSLATION = {"Secret", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Constant"}; + private final String[] PRAGMAS = {"Confidentiality", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "PublicConstant", "PrivateConstant"}; + private final String[] PRAGMAS_TRANSLATION = {"Secret", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "PublicConstant", "PrivateConstant"}; protected AvatarDesignPanel adp; protected Vector checkingErrors, warnings; @@ -158,10 +158,9 @@ public class AvatarDesignPanelTranslator { AvatarPragmaConstant apg = (AvatarPragmaConstant) tmpPragma; for (AvatarConstant ac: apg.getConstants()){ _as.addConstant(ac); - } - } else { - _as.addPragma(tmpPragma); - } + } + } + _as.addPragma(tmpPragma); //TraceManager.addDev("Adding pragma:" + tmp); } } diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java index b411b428bbd4818c7c33a837d59a3f6a585ad444..aa5f58b59a07f3c0463ac4c2c488459478e45ac1 100755 --- a/src/ui/GTURTLEModeling.java +++ b/src/ui/GTURTLEModeling.java @@ -632,7 +632,7 @@ public class GTURTLEModeling { return this.avatar2proverif.getOutputAnalyzer (); } - public boolean generateProVerifFromAVATAR(String _path, boolean _stateReachability, boolean _advancedTranslation, boolean _typed) { + public boolean generateProVerifFromAVATAR(String _path, int _stateReachability, boolean _typed) { avatar2proverif = new AVATAR2ProVerif(avatarspec); //tml2uppaal.setChoiceDeterministic(choices); //tml2uppaal.setSizeInfiniteFIFO(_size); diff --git a/src/ui/TDiagramPanel.java b/src/ui/TDiagramPanel.java index fda70e677782829f87aa379bcd0bc2ced310dc4e..eb2520483acdbfb83beab169f619619a8da5a9f1 100755 --- a/src/ui/TDiagramPanel.java +++ b/src/ui/TDiagramPanel.java @@ -1555,7 +1555,7 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree { removeInternalComment = new JMenuItem("Remove internal comment"); removeInternalComment.addActionListener(menuAL); - checkAccessibility = new JMenuItem("Check for accessibility / liveness with UPPAAL"); + checkAccessibility = new JMenuItem("Check for accessibility / liveness"); checkAccessibility.addActionListener(menuAL); checkInvariant = new JMenuItem("Check for mutual exclusion"); diff --git a/src/ui/avatarbd/AvatarBDPragma.java b/src/ui/avatarbd/AvatarBDPragma.java index 70c2293f7469ff065eb0dcb9455970eec6ba52d4..88275c39362ff51feb1f9a7f049a37f202e4f0ef 100755 --- a/src/ui/avatarbd/AvatarBDPragma.java +++ b/src/ui/avatarbd/AvatarBDPragma.java @@ -78,7 +78,7 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent { private int maxFontSize = 30; private int minFontSize = 4; private int currentFontSize = -1; - private final String[] mPragma = {"#Constant", "#InitialSystemKnowledge", "#InitialSessionKnowledge", "#PrivatePublicKeys", "#Public"}; + private final String[] mPragma = {"#PublicConstant", "#PrivateConstant", "#InitialSystemKnowledge", "#InitialSessionKnowledge", "#PrivatePublicKeys", "#Public"}; private final String[] pPragma = {"#Confidentiality", "#Secret", "#SecrecyAssumption", "#Authenticity"}; protected Graphics graphics; public final static int NOT_VERIFIED = 0; diff --git a/src/ui/window/JDialogPragma.java b/src/ui/window/JDialogPragma.java index 2b711804cad2ced78bef19dd0070fe90b6e1fc34..09954772817ec9e3e07f5ea0e1f03552c2b4face 100755 --- a/src/ui/window/JDialogPragma.java +++ b/src/ui/window/JDialogPragma.java @@ -76,7 +76,7 @@ public class JDialogPragma extends javax.swing.JDialog implements ActionListener //Suggestion Panel code from: http://stackoverflow.com/questions/10873748/how-to-show-autocomplete-as-i-type-in-jtextarea public class SuggestionPanel { - private final String[] pragma = {"#Authenticity", "#Confidentiality", "#Constant", "#InitialSessionKnowledge", "#InitialSystemKnowledge", "#PrivatePublicKeys", "#Public", "#SecrecyAssumption", "#Secret"}; + private final String[] pragma = {"#Authenticity", "#Confidentiality", "#PublicConstant", "#PrivateConstant", "#InitialSessionKnowledge", "#InitialSystemKnowledge", "#PrivatePublicKeys", "#Public", "#SecrecyAssumption", "#Secret"}; private JList list; private JPopupMenu popupMenu; private String subWord; @@ -230,7 +230,7 @@ public class JDialogPragma extends javax.swing.JDialog implements ActionListener c.setLayout(new BorderLayout()); //setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE); helpPopup = new JPopupMenu(); - JTextArea jft = new JTextArea("Pragma Guidelines: \n #Authenticity: Compare if two Attributes are equal at given states \n #Confidentiality: Query whether the attacker knows the value of this attribute. \n #Constant: Declare string as possible constant \n #InitialSessionKnowledge: Knowledge at the start of each session\n #InitialSystemKnowledge: Knowledge at the start of the system \n #PrivatePublicKeys: Set two attribute of a block as Private and Public Key respectively \n #Public: Declare variable public \n #SecrecyAssumption: Assume attribute confidential, but query to verify \n #Secret: See #Confidentiality"); + JTextArea jft = new JTextArea("Pragma Guidelines: \n #Authenticity: Compare if two Attributes are equal at given states \n #Confidentiality: Query whether the attacker knows the value of this attribute. \n #PublicConstant: Declare string as public constant \n #PrivateConstant: Declare string as private constant \n #InitialSessionKnowledge: Knowledge at the start of each session\n #InitialSystemKnowledge: Knowledge at the start of the system \n #PrivatePublicKeys: Set two attribute of a block as Private and Public Key respectively \n #Public: Declare variable public \n #SecrecyAssumption: Assume attribute confidential, but query to verify \n #Secret: See #Confidentiality"); helpPopup.add(jft); textarea = new JTextArea(); diff --git a/src/ui/window/JDialogProVerifGeneration.java b/src/ui/window/JDialogProVerifGeneration.java index d3421323337c39a64be70eab48ffa4154bbb4b80..615d627b821475b2cd3cb40dd488bb07e1520267 100644 --- a/src/ui/window/JDialogProVerifGeneration.java +++ b/src/ui/window/JDialogProVerifGeneration.java @@ -78,6 +78,10 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac protected final static int STARTED = 2; protected final static int STOPPED = 3; + public final static int REACHABILITY_ALL = 1; + public final static int REACHABILITY_SELECTED = 2; + public final static int REACHABILITY_NONE = 3; + int mode; //components @@ -92,7 +96,9 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac protected JTextField code1, code2, unitcycle, compiler1, exe1, exe2, exe3, exe2int; protected JTabbedPane jp1; protected JScrollPane jsp; - protected JCheckBox stateReachability, translationOfBooleanFunction, outputOfProVerif, typedLanguage; + protected JCheckBox outputOfProVerif, typedLanguage; + protected JRadioButton stateReachabilityAll, stateReachabilitySelected, stateReachabilityNone; + protected ButtonGroup stateReachabilityGroup; protected JComboBox versionSimulator; private Thread t; @@ -156,7 +162,6 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac jp03.setBorder(new javax.swing.border.TitledBorder("Execution")); - c01.gridheight = 1; c01.weighty = 1.0; c01.weightx = 1.0; c01.gridwidth = GridBagConstraints.REMAINDER; //end row @@ -173,14 +178,34 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac jp01.add(new JLabel(" "), c01); c01.gridwidth = GridBagConstraints.REMAINDER; //end row - stateReachability = new JCheckBox("Compute state reachability"); - stateReachability.setSelected(true); - jp01.add(stateReachability, c01); - translationOfBooleanFunction = new JCheckBox("Advanced translation of boolean functions"); - translationOfBooleanFunction.setSelected(true); - jp01.add(translationOfBooleanFunction, c01); + c01.gridx = 0; + c01.gridy = 3; + c01.gridwidth = 1; + jp01.add(new JLabel("Compute state reachability: "), c01); + + stateReachabilityGroup = new ButtonGroup (); + + c01.gridx = 1; + stateReachabilityAll = new JRadioButton("all"); + jp01.add(stateReachabilityAll, c01); + + c01.gridx = 2; + stateReachabilitySelected = new JRadioButton("selected"); + jp01.add(stateReachabilitySelected, c01); + + c01.gridx = 3; + c01.gridwidth = GridBagConstraints.REMAINDER; //end row + stateReachabilityNone = new JRadioButton("none"); + jp01.add(stateReachabilityNone, c01); + + stateReachabilityGroup.add (stateReachabilityAll); + stateReachabilityGroup.add (stateReachabilitySelected); + stateReachabilityGroup.add (stateReachabilityNone); + stateReachabilityAll.setSelected(true); + c01.gridx = GridBagConstraints.RELATIVE; + c01.gridy = GridBagConstraints.RELATIVE; typedLanguage = new JCheckBox("Generate typed Pi calculus"); typedLanguage.setSelected(true); jp01.add(typedLanguage, c01); @@ -351,7 +376,7 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac System.out.println("FILE EXISTS!!!"); } - if (mgui.gtm.generateProVerifFromAVATAR(pathCode, stateReachability.isSelected(), translationOfBooleanFunction.isSelected(), typedLanguage.isSelected())) { + if (mgui.gtm.generateProVerifFromAVATAR(pathCode, stateReachabilityAll.isSelected () ? REACHABILITY_ALL : stateReachabilitySelected.isSelected () ? REACHABILITY_SELECTED : REACHABILITY_NONE, typedLanguage.isSelected())) { jta.append("ProVerif code generation done\n"); } else { setError();