Alexis Paljic
email: alexis.paljic@mines-paristech.fr

Ecological Validity of Virtual Reality : Three Use Cases

Keywords: Virtual Reality, Ecological Valididy, Comparative Approach, Real vs. Virtual Comparison, Perception of Complex Materials, Manipulation Gestures, Human Robot Cooperation

This paper is a discussion on the question of ecological validity of virtual reality in the light of three studies that we have done in previous works. These works are chosen as a basis for the discussion because they are all designed to assess validity using one method : the comparison of user perception and behavior between real and virtual environements. The first study explores visual perception of complex materials, the second studies the role of visual feedback on user gestures and object manipulation, the third is a study of virtual reality as a tool for assessing the acceptability of human robot collaboration in a car factory. We discuss our methodology, the limits of validity of VR in our three use cases and suggest future developments in VR to provide design tools for more valid VR environments.

Introduction

Ecological validity of Virtual Reality is a central question when VR is used as a predictive tool. This is typically the case in the context of industrial product design, where human in the loop simulations of products are a part of the design process, to avoid the cost of real prototypes. It is also the case in therapy applications where VR is used to assess human behavior. Indeed, in such predictive uses, the proximity of human response within the virtual environment to the equivalent real situation is necessary.

I here define my use of two terms in this paper, Immersion, and Ecological Validity. I will use the term immersion as encompassing two things : 1) sensorimotor interfaces i.e. what a virtual reality system provides from the technical point of view to address visual, haptic, audidory or other modalities 2) the cognitive interfaces, describing the way activities are performed in the virtual environment. I consider as ecological validity the fact that the user's behavioral response is realistic.

In the specific case of VR as a predictive tool, the role of the designer of the VR simulation is to choose the immersion for each use case and human activity that he or she wants to simulate, with the objective of maximizing the ecological validity.

The research field of ecological validity in VR is very large since sensorimotor and cognitive resources are different for each activity, and may be even so between different users. Thus each activity requires an adaptation of the levels of immersion VR and an assessment of its validity.

We can consider that ecological validity in VR is a specific case of a more general question, that is the relation between immersion and presence. The specificity of ecological validity in VR being that the definition of presence that is considered is "response as if real", one of the definitions proposed by Slater [START_REF] Slater | A note on presence terminology[END_REF].

On the general problem, which is the relation between immersion and presence, there is a large number of user studies in VR that focus on the role of specific level of immersion, visual, haptic, auditory, on activities in virtual reality. Part of those activities are not considered in relation to an equivalent real activity, and thus cannot be considered as within the ecological validity scope of research. As examples, research on immersion in VR to help scientific data visualization (fluid dynamics, molecular visualization), or studies on levels of immersion for application control using menus, are not representative of real activities. There are activities that cannot be performed in real life. Some activities in VR are of ecological nature such as navigation or object manipulation, but there is not a large amount of litterature that actually objectively looks at how close those are to the real thing. The VRKnowledge database1 is a curated repository of research findings in the field of virtual reality, and is potentially very useful to the research community. It aims at bringing together research results on the relation between levels of immersion, and performance metrics on various tasks in VR. The ecological validity, as defined in this paper is not directly considered though. Some works have considered comparing behavioral metrics, between a virtual activity and its real counterpart, to assess ecological validity. Various tasks have been considered. We would be tempted here to present a list sorted by a (tentative) level of complexity of tasks. However sorting tasks by complexity is a difficult and open problem. We will just list a series of tasks, and will start with the ones that require only a perceptive component, requiring no active and concious reaction by the user, then considering more interactive ones2 . Note that this list is not exhaustive, and is meant to show the variety of tasks being considered in the literature. There have been real/virtual comparisons on Visual Perception of Distances [START_REF] Rebekka | The Perception of Egocentric Distances in Virtual Environments -A Review[END_REF], Heights [START_REF] Peter | Height effects in real and virtual environments[END_REF], or perception of materials [START_REF] Da Graãğa | Evaluating Stereoscopic Visualization for Predictive Rendering[END_REF]. On more interactive tasks, we can note : the hoop and wire game [START_REF] Arnold | Performance of a skilled motor task in virtual and real environments[END_REF], playing with Lego Bricks [START_REF] Baradaran | A Comparison of Real and Virtual 3D Construction Tools with Novice Users[END_REF], peg insertion [START_REF] Yoshikawa | Toward Observation of Human Assembly Skill Using Virtual Task Space[END_REF], aiming movements [START_REF] Liu | Comparing aimed movements in the real world and in virtual reality[END_REF], reaching [START_REF] Viau | Reaching in reality and virtual reality: a comparison of movement kinematics in healthy subjects and in adults with hemiparesis[END_REF]. We could consider that the next tasks require a supplemementary level of cognitive involement : navigation and spatial knowledge [START_REF] Mania | Fidelity Metrics for Virtual Environment Simulations Based on Spatial Memory Awareness States[END_REF], car driving [START_REF] Milleville | Driving for Real or on a Fixed-Base Simulator: Is It so Different? An Explorative Study[END_REF], wheelchair driving [START_REF] Cooper | Comparison of virtual and real electric powered wheelchair driving using a position sensing joystick and an isometric joystick[END_REF]. As a last group we propose works that tackle activities that have an emotional or social component : collaboratively solving puzzle with other people [START_REF] Axelsson | Cubes in the cube: a comparison of a puzzle-solving task in a virtual and a real environment[END_REF], social behavior in small groups [START_REF] Slater | Small-Group Behavior in a Virtual and Real Environment: A Comparative Study[END_REF], or cooperation with robots [START_REF] Weistroffer | Assessing the acceptability of co-presence on assembly lines: A comparison between actual situations and their virtual reality counterparts[END_REF]. This list is not exhaustive at all, as this paper's focus is not to do a review of the literature on ecological validity. The intent of the author is to present different ways of tackling the question. I will do so by reporting on three studies that were previously done by the author and his colleagues [START_REF] Victor | Physically based image synthesis of materials: a methodology towards the visual comparison of physical vs. virtual samples[END_REF] [START_REF] Weistroffer | Assessing the Acceptability of Human-Robot Co-Presence on Assembly Lines: A Comparison Between Actual Situations and their Virtual Reality Counterparts[END_REF] that are at located at 3 different points in the continuum of tasks proposed in the previous paragraph : perception only, perception and action, emotional and/or interaction with other entities.

[19][7][6][9]

Complex Material Observation

In the domains of Cinema or video Games, an esthetically driven, or simply plausible visual appearance of objects can be acceptable. It not the case for the use of VR for the design of visual appearance of materials, where object's visual aspects needs to be physically realistic. The industrial need is a virtual material design workshop, in which the user virtually specifies a material composition, then he is able to visualize its resulting visual aspect in a VR environment. In this virtual material workshop, we determine the composition of a future real material whose appearance is supposedly predicted by the virtual one. The realistic nature of the image is thus paramount. In order to set up such a workshop, a research project3 is built on a 4 step methodology : 1) optical measures to characterize the composition of the chosen material samples, 2) light-matter interaction models, 3) Rendering in a VR system, 4) Perceptive validations with the human in the loop by comparing real and virtual samples. The results of this resarch are described, for the case of homogeneous coloured materials in Medina et al.'s works [START_REF] Victor | Physically based image synthesis of materials: a methodology towards the visual comparison of physical vs. virtual samples[END_REF][19] and as for complex materials (such as car paints with effects) in [START_REF] Da Graça | Stereoscopy for visual simulation of materials of complex appearance[END_REF] [START_REF] Da Graça | Evaluating Stereoscopic Visualization for Predictive Rendering[END_REF].

The first step in order to obtain a realistic appearance in VR is to ensure a proper calibration of the display chain (including display and stereoscopic glasses characteristics), given that the rendering models and engine provide the spectrum of the light being emitted by the virtual materials. We have set up such a process, in the case of homogeneous materials [START_REF] Victor | Physically based image synthesis of materials: a methodology towards the visual comparison of physical vs. virtual samples[END_REF] [START_REF] Victor | A study of image exposure for the stereoscopic visualization of sparkling materials[END_REF].

We will focus in this paper on another material type, which is complex materials with visual effects, such as car paints which have metallic flakes embedded in the base coat and produce sparkling effects. Statistical models describing such materials have been set up in the project [START_REF] Couka | A mixed Boolean and deposit model for the modeling of metal pigments in paint layers[END_REF], based on optical measurements. The Fig. 1. In order to simulate car paints that have have metallic flakes embedded in the base coat and produce sparkling effects, statistical models describing such materials have been set up [START_REF] Couka | A mixed Boolean and deposit model for the modeling of metal pigments in paint layers[END_REF], based on optical measurements. The models create virtual microstructures, that are fed into a rendering engine for stereoscopic visualization. Then, in a perceptive study, users were asked to compare pictures of real car paints and simulated ones models create virtual microstructures, that are fed into a rendering engine (see Figure 3). To sum up the general results for that case, the above methodology allowed to show two results. Firstly, the use of stereoscopy decreases perception thresholds of specific properties of the material (size and density of aluminium particles) [START_REF] Da Graça | Stereoscopy for visual simulation of materials of complex appearance[END_REF]. Secondly, we have validated that our VR visualization system allows to make a correspondence, for a given visual aspect, between the descriptive metrics of the virtual material to the ones of the real material, through user perceptive studies [START_REF] Da Graça | Evaluating Stereoscopic Visualization for Predictive Rendering[END_REF], see Figure 2.

Both these results have a consequence on ecological validity of VR for the observation of materials : 1) we show that stereoscopy has an impact on perception thresholds and that we are able to quantify it. This quantification can be used as a guideline for the design of VR systems for ecological validity as is can drive immersion choices (given a threshold need, should we use stereo or not?).

2) we show that ecological validity can be achieved in VR at the level of material composition. In the experimental setup, a simple stereoscopic display was used, without dynamic perspective (no head tracking).

Gestures in Object Manipulation

Gestures that are performed in a virtual reality system are likely to be different than gestures from everyday life tasks. The quality of virtual reality systems can modify the way gestures are performed. As examples, we can point out the visual latency of the system, being the delay between movement capture and the resulting visual feedback on the avatar of one's hand. High latencies are known to decrease performance. The number of degrees of freedom that are captured, between a simple hand pose measurement, or a full hand joints configuration acquisition using gloves or vision based cameras, achieve very different levels of ecology of prehension. The use of props, reproducing the shape of the manipulated object can improve user experience and gesture validity.

Here the question we asked ourselves is how much can we play (reduce, distort) with visual feedback and still get stable, close to normal results?

We looked into the role of visual feedback and visual appearance of objects on manipulation gestures in VR. In a previous work [START_REF] Jégo | User-Defined Gestural Interaction: a Study on Gesture Memorization[END_REF] we have studied the role of visual feedback and visual appearance of objects on manipulation gestures (gestures performed while manipulating objects).

A variety of feedbacks where implemented, on a box opening task. The user performed the gesture to open the box, and depending on the progression of his gesture (depending on its position along a prerecorded gesture) a visual feedback on the opening of the box was provided. The visual feebacks (see figure 3) where ranging from boolean (box would visually open only at the end of the gesture), textual (a percentage of the opening was displayed), discrete (only a few steps were displayed), normal, enhanced (with a >1 gain between motion capture and visual displacement) and non coupled (or open loop : meaning that an automatic animation of the box would start at contact user movements having no effect on it). We compared descriptors of gestures between an initially recorded natural gesture (done with no feedback constraints), and the gestures performed with the feedbacks. Results showed firstly that the non coupled feedback is immediatly recognized as such, and gesture descriptors greatly differ from initial gesture (small movements, shorter time). Mechanical work and completion time are also different for all feedbacks. Finally the subjective preferences of users went to enhanced feedback, and diminish with for lower levels of information. In a second experiment, we studied the role of affordances on gesture memorization. We have shown that affordances, which is the visual appearence of objects that shows how it is operated, increase user recall of gestures. The outcome of this study was mainly to set up a method to explore immersion and its effects : a systematic approach of gradually simplifying feedback in order to determine what is necessary in the stimuli in virtual environements to perform valid/representative actions.

Human Robot Cooperation

The introduction of robots as coworking or collaborative units with humans would help reducing physical strain for difficult tasks. However it opens a lot of questions on their social and practical acceptability. We looked into the validity of virtual reality as a tool to assess the acceptability, from the human point of view, to work with a robot. To do so, we set up two use cases in both a real setup and a virtual environment (CAVE), and compared what is representative in VR and what is not [START_REF] Weistroffer | Assessing the Acceptability of Human-Robot Co-Presence on Assembly Lines: A Comparison Between Actual Situations and their Virtual Reality Counterparts[END_REF]. The two use cases were, Human Robot (HR) Copresence and HR Cooperation. Both are studied in the context of car parts mounting tasks in a factory. In the case of HR Copresence, a worker and a robot are working side by side on mounting parts of a car door (see figures 4 and5). The studied variables were environement type (Real/Virtual) and the distance between the operator and the robot (Close, Far).

In the case of HR Cooperation the worker and the robot are facing each other, and the robot can give various parts to the worker (see figures 6 and7). Here the variables that were studied were environement type (Real/Virtual) and different levels of assistance of the robot. In the copresence scenario users preference (questionnaires) went to the 'far' condition, and this result was consistent between real and virtual environments. A increase in heart rate was found when the robot was close, in both real and virtual conditions. Finally, a skin conductance raise (that may be representative of user stress) when the robot was close, in the real conditions, was not found in the virtual condition. In the cooperation scenario, the main result is again that the questionnaires get close responses between real and virtual conditions (acceptability, perceived security, usability). And we observe the same trends on physiological measures as for the copresence use case. We can hypothesize that more complete feedbacks (such as haptics providing contact information with the environment, or auditory feedback for factory or simulated robot sounds) may increase ecological validity, but these require specific studies.

Discussion

Virtual reality shows ecological validity for each of the tasks that we have studied. However, this validity is only proven to a certain extent. Some of the descriptors of human behavior do not match between VR and real (physiological measures for example). The results that we have presented, on comparing behavior descriptors between same activities performed in real and virtual situations, are specific to the use cases an considered tasks. Especially, for each use case, many additional studies can and should be performed to assess the influence of other levels of immersion. We propose below a few examples of characteristics of immersion that could change user response towards higher ecological validity. Here, we argue that the three use cases that we have presented have also a methodological interest. They showed that, for each use case, we can make real / virtual comparisons at very different levels : global subjective appearance of materials, or, at a totally different level, validate underlying physics models. For the Gestures case, two different methods were used. The first is spatial and temporal gesure comparison. For the second, we have tried to develop a method that not only seeks to assertain real/virtual coherence, but also to find out what is the minimal relevant information in the feedback. We did so by stripping down feedback with the goal of finding the minimal information that is needed to have a valid gesture. In this case, the method showed that the maximum info is needed, it is the opinion of the author that this method can be used in different contexts. Finally, for HR copresence and cooperation : we have used subjective questionnaires (Acceptability, Security) or more objective physiological measures 4 .

An important question that is open is how can designers of VR systems re-use such results? Indeed, if one has to set up an activity that is close to ones that appear in the real/virtual comparison literature, a transposition of the results should lead her or him to choose similar levels of immersion.

Here the difficulty resides in deciding what close means. For example, in our material observation use case, we have proven ecological validity for a specific type of metallic flakes. Do these results hold if we change average flake size, or flake shape, or size/shape of the sample on which the material is presented? And what to do if the use case one is setting up does not appear at all in the literature? No guidelines at all in that case. A dream tool answering the question of reusability would be a dictionnary of core activities, and the associated immersion needed for ecological validity. Those core activities, simple in nature, would be the building blocks of any more complex activity. Thus the dictionnary would provide building blocks to infer immersion for any given task. Today this dream tool is purely conceptual.

Conclusion

We have shown that in our three use cases, ecological validity can be proven through a real / virtual comparison method. They work for some of descriptors : questionnaires, movement measures, visual perception of specific properties, and for some not, such as physiological measures. Virtual reality communities have to continue exploring the question of ecological validity and adding up results for the reuse in future designs. But it is a long work. VR and Cognitives Sciences have started to interact, and share their results on the role of immersion on presence. Would this be the beginning of a dictionnary of (micro level) tasks that could be combineable to describe any (macro level) task? In that case a dream tool adding up immersion for ecological validity at the micro level, to construct the immersion at a macro level would be a little bit closer to a reality.

Fig. 2 .

 2 Fig. 2. Car paint models are fed into a rendering engine for stereoscopic visualization.Then, in a perceptive study, users were asked to compare pictures of real car paints and simulated ones

Fig. 3 .

 3 Fig. 3. Study of gesture feedback : on a box opening task, the gesture is measured and several visual feedbacks are proposed to the user (from left to right : boolean, textual, steps, normal, enhanced, openloop) and compared in terms of gesture completion and proximity to an initially recorded natural gesture

Fig. 4 .

 4 Fig. 4. Human Robot Copresence Study. Real Environment.

Fig. 5 .

 5 Fig. 5. Human Robot Copresence Study. Virtual Environment.

Fig. 6 .

 6 Fig. 6. Human Robot Cooperation Study. Real Environment.

Fig. 7 .

 7 Fig. 7. Human Robot Cooperation Study. Virtual Environment

1 . 2 .

 12 Material Observation : Resolution of displays, gamut of displays, high dynamic range displays, use of head tracking and dynamic perspective. Gestures in Object Manipulation : Use of finger tracking, Use of physics engine, Haptic feedback 3. Human Robot Cooperation : Hapic Feedback, Auditory Feedback.

http://knowledgebase.cs.vt.edu/

although this also can be discussed : tasks that appear to be of only of perceptive nature, are likely to include human actions, even non concious, as Varela et al. suggest in their work on Enaction[START_REF] Varela | LâĂŹinscription corporelle de lâĂŹesprit[END_REF]

see acknowledgements

although physiological measures require careful use because of practical reasons : sensors on the skin can move, and add strong variability in data.

Acknowledgments. A part this work (material perception) was funded by French National Research Agency project funded LIMA (Light Interaction Matter Aspect, 2012-2016) under grant number ANR2011RMNP01401. The work on Human Robot cooperation was funded by PSA Group through a research Chair (Chaire Robotique et Realite Virtuelle).


Véronique Cortier
email: veronique.cortier@loria.fr

Niklas Grimm
email: niklas.grimm@tuwien.ac.at

Joseph Lallemand
email: joseph.lallemand@loria.fr

Matteo Maffei
email: matteo.maffei@tuwien.ac.at

A Type System for Privacy Properties

Keywords: Security and privacy → Formal security models, Logic and verification, Protocols, privacy, symbolic models, type systems

Mature push button tools have emerged for checking trace properties (e.g. secrecy or authentication) of security protocols. The case of indistinguishability-based privacy properties (e.g. ballot privacy or anonymity) is more complex and constitutes an active research topic with several recent propositions of techniques and tools.

We explore a novel approach based on type systems and provide a (sound) type system for proving equivalence of protocols, for a bounded or an unbounded number of sessions. The resulting prototype implementation has been tested on various protocols of the literature. It provides a significant speed-up (by orders of magnitude) compared to tools for a bounded number of sessions and complements in terms of expressiveness other state-of-the-art tools, such as ProVerif and Tamarin: e.g., we show that our analysis technique is the first one to handle a faithful encoding of the Helios e-voting protocol in the context of an untrusted ballot box.

INTRODUCTION

Formal methods proved to be indispensable tools for the analysis of advanced cryptographic protocols such as those for key distribution [START_REF] Schmidt | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties[END_REF], mobile payments [START_REF] Cortier | Designing and Proving an EMV-compliant Payment Protocol for Mobile Devices[END_REF], e-voting [START_REF] Backes | Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus[END_REF][START_REF] Cortier | Type-Based Verification of Electronic Voting Protocols[END_REF][START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF], and e-health [START_REF] Maffei | Security and Privacy by Declarative Design[END_REF]. In the last years, mature push-button analysis tools have emerged and have been successfully applied to many protocols from the literature in the context of trace properties such as authentication or confidentiality. These tools employ a variety of analysis techniques, such as model checking (e.g., Avispa [START_REF] Armando | The AVISPA Tool for the automated validation of internet security protocols and applications[END_REF] and Scyther [START_REF] Cas | The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols[END_REF]), Horn clause resolution (e.g., ProVerif [START_REF] Blanchet | An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[END_REF]), term rewriting (e.g., Scyther [START_REF] Cas | The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols[END_REF] and Tamarin [START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF]), and type systems [12, 17, 23-28, 46, 47].

A current and very active topic is the adaptation of these techniques to the more involved case of trace equivalence properties. These are the natural symbolic counterpart of cryptographic indistinguishability properties, and they are at the heart of privacy properties such as ballot privacy [START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF], untraceability [START_REF] Arapinis | Untraceability in the Applied Pi Calculus[END_REF], differential privacy [START_REF] Eigner | Differential Privacy by Typing in Security Protocols[END_REF], or anonymity [START_REF] Abadi | Private Authentication[END_REF][START_REF] Arapinis | Analysing Unlinkability and Anonymity Using the Applied Pi Calculus[END_REF]. They are also used to express stronger forms of confidentiality, such as strong secrecy [START_REF] Cortier | Relating Two Standard Notions of Secrecy[END_REF] or game-based like properties [START_REF] Comon | Computational Soundness of Observational Equivalence[END_REF].

Related Work. Numerous model checking-based tools have recently been proposed for the case of a bounded number of sessions, i.e., when protocols are executed a bounded number of times. These tools encompass SPEC [START_REF] Dawson | Automating Open Bisimulation Checking for the Spi Calculus[END_REF], APTE [START_REF] Baelde | Partial Order Reduction for Security Protocols[END_REF][START_REF] Cheval | APTE: an Algorithm for Proving Trace Equivalence[END_REF], Akiss [START_REF] Chadha | Automated Verification of Equivalence Properties of Cryptographic Protocols[END_REF], or SAT-Equiv [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF]. These tools vary in the class of cryptographic primitives and the class of protocols they can consider. However, due to the complexity of the problem, they all suffer from the state explosion problem and most of them can typically analyse no more than 3-4 sessions of (relatively small) protocols, with the exception of SAT-Equiv which can more easily reach about 10 sessions. The only tools that can verify equivalence properties for an unbounded number of sessions are ProVerif [START_REF] Blanchet | Automated Verification of Selected Equivalences for Security Protocols[END_REF]. Maude-NPA [START_REF] Santiago | A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA[END_REF], and Tamarin [START_REF] Basin | Automated Symbolic Proofs of Observational Equivalence[END_REF]. ProVerif checks a property that is stronger than trace equivalence, namely diff equivalence, which works well in practice provided that protocols have a similar structure. However, as for trace properties, the internal design of ProVerif renders the tool unable to distinguish between exactly one session and infinitely many: this over-approximation often yields false attacks, in particular when the security of a protocol relies on the fact that some action is only performed once. Maude-NPA also checks diff-equivalence but often does not terminate. Tamarin can handle an unbounded number of sessions and is very flexible in terms of supported protocol classes but it often requires human interactions. Finally, some recent work has started to leverage type systems to enforce relational properties for programs, exploring this approach also in the context of cryptographic protocol implementations [START_REF] Barthe | Probabilistic Relational Verification for Cryptographic Implementations[END_REF]: like ProVerif, the resulting tool is unable to distinguish between exactly one session and infinitely many, and furthermore it is only semi-automated, in that it often requires non-trivial lemmas to guide the tool and a specific programming discipline.

Many recent results have been obtained in the area of relational verification of programs [START_REF] Antonopoulos | Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels[END_REF][START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF][START_REF] Benton | Simple Relational Correctness Proofs for Static Analyses and Program Transformations[END_REF][START_REF] Ciobâcă | A languageindependent proof system for full program equivalence[END_REF][START_REF] Grimm | A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations[END_REF][START_REF] Lucanu | Program equivalence by circular reasoning[END_REF][START_REF] Sousa | Cartesian Hoare Logic for Verifying k-Safety Properties[END_REF][START_REF] Yang | Relational Separation Logic[END_REF]. While these results do not target cryptographic protocols and, in particular, do not handle the semantics of cryptographic primitives or an active adversary interference with the program execution, exploring the suitability of the underlying ideas in the context of cryptographic protocols is an interesting subject of future work.

Our contribution. In this paper, we consider a novel type checkingbased approach. Intuitively, a type system over-approximates protocol behavior. Due to this over-approximation, it is no longer possible to decide security properties but the types typically convey sufficient information to prove security. Extending this approach to equivalence properties is a delicate task. Indeed, two protocols P and Q are in equivalence if (roughly) any trace of P has an equivalent trace in Q (and conversely). Over-approximating behavior may not preserve equivalence.

Instead, we develop a somewhat hybrid approach: we design a type system to over-approximate the set of possible traces and we collect the set of sent messages into constraints. We then propose a procedure for proving (static) equivalence of the constraints. These do not only contain sent messages but also reflect internal checks made by the protocols, which is crucial to guarantee that whenever a message is accepted by P, it is also accepted by Q (and conversely).

As a result, we provide a sound type system for proving equivalence of protocols for both a bounded and an unbounded number of sessions, or a mix of both. This is particularly convenient to analyse systems where some actions are limited (e.g., no revote, or limited access to some resource). More specifically, we show that whenever two protocols P and Q are type-checked to be equivalent, then they are in trace equivalence, for the standard notion of trace equivalence [START_REF] Boreale | Proof Techniques for Cryptographic Processes[END_REF], against a full Dolev-Yao attacker. In particular, one advantage of our approach is that it proves security directly in a security model that is similar to the ones used by the other popular tools, in contrast to many other security proofs based on type systems. Our result holds for protocols with all standard primitives (symmetric and asymetric encryption, signatures, pairs, hash), with atomic long-term keys (no fresh keys) and no private channels. Similarly to ProVerif, we need the two protocols P and Q to have a rather similar structure.

We provide a prototype implementation of our type system, that we evaluate on several protocols of the literature. In the case of a bounded number of sessions, our tool provides a significant speed-up (less than one second to analyse a dozen of sessions while other tools typically do not answer within 12 hours, with a few exceptions). To be fair, let us emphasize that these tools can decide equivalence while our tool checks sufficient conditions by the means of our type system. In the case of an unbounded number of sessions, the performance of our prototype tool is comparable to ProVerif. In contrast to ProVerif, our tool can consider a mix of bounded and unbounded number of sessions. As an application, we can prove for the first time ballot privacy of the well-known Helios e-voting protocol [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF], without assuming a reliable channel between honest voters and the ballot box. ProVerif fails in this case as ballot privacy only holds under the assumption that honest voters vote at most once, otherwise the protocol is subject to a copy attack [53]. For similar reasons, also Tamarin fails to verify this protocol. In most of our example, only a few straightforward type annotations were needed, such as indicated which keys are supposed to be secret or public. The case of the helios protocol is more involved and requires to describe the form of encrypted ballots that can be sent by a voter.

Our prototype, the protocol models, as well as a technical report are available online [START_REF] Cortier | A Type System for Privacy Properties[END_REF][START_REF] Cortier | TypeEQ. Source Code[END_REF].

OVERVIEW OF OUR APPROACH

In this section, we introduce the key ideas underlying our approach on a simplified version of the Helios voting protocol. Helios [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF] is a verifiable voting protocol that has been used in various elections, including the election of the rector of the University of Louvain-la-Neuve. Its behavior is depicted below:

S → V i : r i V i → S : [{v i } r i ,r ′ i pk(k s ) ] k i S → V 1 , . . . , V n : v 1 , . . . , v n
where {m} r pk(k ) denotes the asymmetric encryption of message m with the key pk(k ) randomized with the nonce r , and [m] k denotes the signature of m with key k. v i is a value in the set {0, 1}, which represents the candidate V i votes for. In the first step, the voter casts her vote, encrypted with the election's public key pk(k s ) and then signed. Since generating a good random number is difficult for the voter's client (typically a JavaScript run in a browser), a typical trick is to input some randomness (r i ) from the server and to add it to its own randomness (r ′ i ). In the second step the server outputs the tally (i.e., a randomized permutation of the valid votes received in the voting phase). Note that the original Helios protocol does not assume signed ballots. Instead, voters authenticate themselves through a login mechanism. For simplicity, we abstract this authenticated channel by a signature.

A voting protocol provides vote privacy [START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF] if an attacker is not able to know which voter voted for which candidate. Intuitively, this can be modeled as the following trace equivalence property, which requires the attacker not to be able to distinguish A voting 0 and B voting 1 from A voting 1 and B voting 0. Notice that the attacker may control an unbounded number of voters:

V oter (k a , 0) | V oter (k b , 1) | CompromisedV oters | S ≈ t V oter (k a , 1) | V oter (k b , 0) | CompromisedV oters | S
Despite its simplicity, this protocol has a few interesting features that make its analysis particularly challenging. First of all, the server is supposed to discard ciphertext duplicates, otherwise a malicious eligible voter E could intercept A's ciphertext, sign it, and send it to the server [START_REF] Cortier | Attacking and Fixing Helios: An Analysis of Ballot Secrecy[END_REF], as exemplified below:

A → S : [{v a } r a ,r ′ a pk(k s ) ] k a E → S : [{v a } r a ,r ′ a pk(k s ) ] k e B → S : [{v b } r b ,r ′ b pk(k s ) ] k b S → A, B : v a , v b , v a
This would make the two tallied results distinguishable, thereby breaking trace equivalence since

v a , v b , v a ̸ ≈ t v b , v a , v b
Even more interestingly, each voter is supposed to be able to vote only once, otherwise the same attack would apply [53] even if the server discards ciphertext duplicates (as the randomness used by the voter in the two ballots would be different). This makes the analysis particularly challenging, and in particular out of scope of existing cryptographic protocol analyzers like ProVerif, which abstract away from the number of protocol sessions.

With our type system, we can successfully verify the aforementioned privacy property using the following types:

r a : τ LL,1 r a , r b : τ LL,1 r b , r ′ a : τ HH,1 r ′ a , r ′ b : τ HH,1 r ′ b k a : key HH ({ τ LL,1 0 ; τ LL,1 1 * HL * τ HH,1 r ′ a } k s ) k b : key HH ({ τ LL,1 1 ; τ LL,1 0 * HL * τ HH,1 r ′ b } k s ) k s : key HH ( τ LL,1 0 ; τ LL,1 1 * HL * τ HH,1 r ′ a ) ∨ ( τ LL,1 1 ; τ LL,1 0 * HL * τ HH,1 r ′ b )
We assume standard security labels: HH stands for high confidentiality and high integrity, HL for high confidentiality and low integrity, and LL for low confidentiality and low integrity (for simplicity, we omit the low confidentiality and high integrity type, since we do not need it in our examples). The type τ l,1 i describes randomness of security label l produced by the randomness generator at position i in the program, which can be invoked at most once. τ l,∞ i is similar, with the difference that the randomness generator can be invoked an unbounded number of times. These types induce a partition on random values, in which each set contains at most one element or an unbounded number of elements, respectively. This turns out to be useful, as explained below, to type-check protocols, like Helios, in which the number of times messages of a certain shape are produced is relevant for the security of the protocol.

The type of k a (resp. k b ) says that this key is supposed to encrypt 0 and 1 (resp. 1 and 0) on the left-and right-hand side of the equivalence relation, further describing the type of the randomness. The type of k s inherits the two payload types, which are combined in disjunctive form. In fact, public key types implicitly convey an additional payload type, the one characterizing messages encrypted by the attacker: these are of low confidentiality and turn out to be the same on the left-and right-hand side. Key types are crucial to type-check the server code: we verify the signatures produced by A and B and can then use the ciphertext type derived from the type of k a and k b to infer after decryption the vote cast by A and B, respectively. While processing the other ballots, the server discards the ciphertexts produced with randomness matching the one used by A or B: given that these random values are used only once, we know that the remaining ciphertexts must come from the attacker and thus convey the same vote on the left-and on the right-hand side. This suffices to type-check the final output, since the two tallied results on the left-and right-hand side are the same, and thus fulfill trace equivalence.

The type system generates a set of constraints, which, if "consistent", suffice to prove that the protocol is trace equivalent. Intuitively, these constraints characterize the indistinguishability of the messages output by the process. The constraints generated for this simplified version of Helios are reported below:

C = {({sign(aenc(⟨0, ⟨x, r ′ a ⟩⟩, pk(k S )), k a ) ∼ sign(aenc(⟨1, ⟨x, r ′ a ⟩⟩, pk(k S )), k a ), aenc(⟨0, ⟨x, r ′ a ⟩⟩, pk(k S )) ∼ aenc(⟨1, ⟨x, r ′ a ⟩⟩, pk(k S )), sign(aenc(⟨1, ⟨y, r ′ b ⟩⟩, pk(k S )), k b ) ∼ sign(aenc(⟨0, ⟨y, r ′ b ⟩⟩, pk(k S )), k b ), aenc(⟨1, ⟨y, r ′ b ⟩⟩, pk(k S )) ∼ aenc(⟨0, ⟨y, r ′ b ⟩⟩, pk(k S ))}, [x : LL, y : LL])}
These constraints are consistent if the set of left messages of the constraints is in (static) equivalence with the set of the right messages of the constraints. This is clearly the case here, since encryption hides the content of the plaintext. Just to give an example of nonconsistent constraints, consider the following ones:

C ′ = {{h(n 1 ) ∼ h(n 2 ), h(n 1 ) ∼ h(n 1 )}}
where n 1 , n 2 are two confidential nonces. While the first constraint alone is consistent, since n 1 and n 2 are of high confidentiality and the attacker cannot thus distinguish between h(n 1 ) and h(n 2 ), the two constraints all together are not consistent, since the attacker can clearly notice if the two terms output by the process are the same or not. We developed a dedicated procedure to check the consistency of such constraints.

FRAMEWORK

In symbolic models, security protocols are typically modeled as processes of a process algebra, such as the applied pi-calculus [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF].

We present here a calculus close to [START_REF] Cheval | Lengths May Break Privacy -or How to Check for Equivalences With Length[END_REF] inspired from the calculus underlying the ProVerif tool [START_REF] Blanchet | Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif[END_REF].

Terms

Messages are modeled as terms. We assume an infinite set of names N for nonces, further partitioned into the set F N of free nonces (created by the attacker) and the set BN of bound nonces (created by the protocol parties), an infinite set of names K for keys, ranged over by k, and an infinite set of variables V. Cryptographic primitives are modeled through a signature F , that is a set of function symbols, given with their arity (that is, the number of arguments).

Here, we will consider the following signature:

F c = {pk, vk, enc, aenc, sign, ⟨•, •⟩, h}
that models respectively public and verification key, symmetric and asymmetric encryption, concatenation and hash. The companion primitives (symmetric and asymmetric decryption, signature check, and projections) are represented by the following signature:

F d = {dec, adec, checksign, π 1 , π 2 }
We also consider a set C of (public) constants (used as agents names for instance). Given a signature F , a set of names N and a set of variables V, the set of terms T (F , V, N ) is the set inductively defined by applying functions to variables in V and names in N . We denote by names(t ) (resp. vars(t )) the set of names (resp. variables) occurring in t. A term is ground if it does not contain variables.

Here, we will consider the set T (F c ∪ F d ∪ C, V, N ∪ K ) of cryptographic terms, simply called terms. Messages are terms from

T (F c ∪ C, V, N ∪ K ) with atomic keys, that is, a term t ∈ T (F c ∪ C, V, N ∪ K ) is a message if any subterm of t of the form pk(t ′ ), vk(t ′ ), enc(t 1 , t ′ ), aenc(t 1 , t 2 ), or sign(t 1 , t ′ ) is such that t ′ ∈ K and t 2 = pk(t ′
2 ) with t ′ 2 ∈ K . We assume the set of variables to be split into two subsets V = X ⊎ AX where X are variables used in processes while AX are variables used to store messages. An attacker term is a term from T (F c ∪ F d ∪ C, AX, F N ).

A substitution σ = {M 1 /x 1 , . . . , M k /x k } is a mapping from variables x 1 , . . . , x k ∈ V to messages M 1 , . . . , M k . We let dom(σ ) = {x 1 , . . . , x k }. We say that σ is ground if all messages M 1 , . . . , M k are ground. We let names(σ ) = 1≤i ≤k names(M i ). The application of a substitution σ to a term t is denoted tσ and is defined as usual.

The evaluation of a term t, denoted t ↓, corresponds to the application of the cryptographic primitives. For example, the decryption succeeds only if the right decryption key is used. Formally, t ↓ is recursively defined as follows.

u

↓ = u if u ∈ N ∪ V ∪ K ∪ C pk(t ) ↓ = pk(t ↓) if t ↓∈ K vk(t ) ↓ = vk(t ↓) if t ↓∈ K h(t ) ↓ = h(t ↓) if t ↓ ⊥ ⟨t 1 , t 2 ⟩ ↓ = ⟨t 1 ↓, t 2 ↓⟩ if t 1 ↓ ⊥ and t 2 ↓ ⊥ enc(t 1 , t 2 ) ↓ = enc(t 1 ↓, t 2 ↓) if t 1 ↓ ⊥ and t 2 ↓∈ K sign(t 1 , t 2 ) ↓ = sign(t 1 ↓, t 2 ↓) if t 1 ↓ ⊥ and t 2 ↓∈ K aenc(t 1 , t 2 ) ↓ = aenc(t 1 ↓, t 2 ↓) if t 1 ↓ ⊥ and t 2 ↓= pk(k ) for some k ∈ K π 1 (t ) ↓ = t 1 if t ↓= ⟨t 1 , t 2 ⟩ π 2 (t ) ↓ = t 2 if t ↓= ⟨t 1 , t 2 ⟩ dec(t 1 , t 2 ) ↓ = t 3 if t 1 ↓= enc(t 3 , t 4 ) and t 4 = t 2 ↓ adec(t 1 , t 2 ) ↓ = t 3 if t 1 ↓= aenc(t 3 , pk(t 4 )) and t 4 = t 2 ↓ checksign(t 1 , t 2 ) ↓ = t 3 if t 1 ↓= sign(t 3 , t 4 ) and t 2 ↓= vk(t 4 ) t ↓ = ⊥ otherwise
Note that the evaluation of term t succeeds only if the underlying keys are atomic and always returns a message or ⊥. We write t = ↓ t ′ if t ↓= t ′ ↓.

Processes

Security protocols describe how messages should be exchanged between participants. We model them through a process algebra, whose syntax is displayed in Figure 1. We identify processes up to α-renaming, i.e., capture avoiding substitution of bound names and variables, which are defined as usual. Furthermore, we assume that all bound names and variables in the process are distinct.

A configuration of the system is a quadruple (E; P; ϕ; σ ) where:

• P is a multiset of processes that represents the current active processes; • E is a set of names, which represents the private names of the processes; • ϕ is a substitution with dom(ϕ) ⊆ AX and for any x ∈ dom(ϕ), ϕ (x ) (also denoted xϕ) is a message that only contains variables in dom(σ ). ϕ represents the terms already output. • σ is a ground substitution;

The semantics of processes is given through a transition relation α --→ on the quadruples provided in Figure 2 (τ denotes a silent Destructors used in processes:

d ::= dec(•, k ) | adec(•, k ) | checksign(•, vk(k )) | π 1 (•) | π 2 (•) Processes: P, Q ::= 0 | new n.P for n ∈ BN (n bound in P ) | out(M ).P | in(x ).P for x ∈ X(x bound in P ) | P | Q | let x = d (y) in P else Q for x, y ∈ X(x bound in P ) | if M = N then P else Q | !P
where M, N are messages. Intuitively, process new n.P creates a fresh nonce, stored in E, and behaves like P. Process out(M ).P emits M and behaves like P. Process in(x ).P inputs any term computed by the attacker provided it evaluates as a message and then behaves like P. Process P | Q corresponds to the parallel composition of P and Q. Process let x = d (y) in P else Q behaves like P in which x is replaced by d (y) if d (y) can be successfully evaluated and behaves like Q otherwise.

Process if M = N then P else Q behaves like P if M and N correspond to two equal messages and behaves like Q otherwise. The replicated process !P behaves as an unbounded number of copies of P.

A trace of a process P is any possible sequence of transitions in the presence of an attacker that may read, forge, and send messages. Formally, the set of traces trace(P ) is defined as follows.

trace(P ) = {(w, new E.ϕ, σ )|(∅; {P }; ∅; ∅) w ---→ * (E; P; ϕ; σ )} Example 3.1.
Consider the Helios protocol presented in Section 2. For simplicity, we describe here a simplified version with only two (honest) voters A and B and a voting server S. This (simplified) protocol can be modeled by the process:

new r a .V oter (k a , v a , r a ) | new r b .V oter (k b , v b , r b ) | P S
where V oter (k, v, r ) represents voter k willing to vote for v using randomness r while P S represents the voting server. V oter (k, v, r ) simply outputs a signed encrypted vote.

V oter (k, v, r ) = out(sign(aenc(⟨v, r ⟩, pk(k S )), k )) (E; {P 1 | P 2 } ∪ P; ϕ; σ ) τ --→ (E; {P 1 , P 2 } ∪ P; ϕ; σ ) Par (E; {0} ∪ P; ϕ; σ ) τ --→ (E; P; ϕ; σ ) Zero (E; {new n.P } ∪ P; ϕ; σ ) τ --→ (E ∪ {n}; {P } ∪ P; ϕ; σ ) New (E; {out(t ).P } ∪ P; ϕ; σ ) new ax n .out(ax n ) -----------------→ (E; {P } ∪ P; ϕ ∪ {t/ax n }; σ ) Out if tσ is a ground term, ax n ∈ AX and n = |ϕ | + 1 (E; {in(x ).P } ∪ P; ϕ; σ ) in(R) ------→ (E; {P } ∪ P; ϕ; σ ∪ {(Rϕσ ) ↓ /x }) In if R is an attacker term such that vars(R) ⊆ dom(ϕ),
and The voting server receives ballots from A and B and then outputs the decrypted ballots, after some mixing.

(Rϕσ ) ↓ ⊥ (E; {let x = d (M ) in P else Q } ∪ P; ϕ; σ ) τ --→ (E; {P } ∪ P; ϕ; σ ∪ {d (Mσ ) ↓ /x }) Let-In if Mσ is ground and d (Mσ ) ↓ ⊥ (E; {let x = d (M ) in P else Q } ∪ P; ϕ; σ ) τ --→ (E; {Q } ∪ P; ϕ; σ ) Let-Else if Mσ is ground and d (Mσ ) ↓= ⊥, i.e. d cannot be applied to Mσ (E; {if M = N then P else Q } ∪ P; ϕ; σ ) τ --→ (E; {P } ∪ P; ϕ; σ ) If-Then if M, N are messages such that Mσ , N σ are ground and Mσ = N σ (E; {if M = N then P else Q } ∪ P; ϕ; σ ) τ --→ (E; {Q } ∪ P; ϕ; σ ) If-Else if M, N are messages such that Mσ , N σ are ground and Mσ N σ (E; {!P } ∪ P; ϕ; σ ) τ --→ (E; {P, !P } ∪ P; ϕ; σ ) Repl
P S =in(x 1 ).in(x 2 ). let y 1 = checksign(x 1 , vk(k a )) in let y 2 = checksign(x 2 , vk(k b )) in let z 1 = adec(y 1 , k s ) in let z ′ 1 = π 1 (z 1 ) in let z 2 = adec(y 2 , k s ) in let z ′ 2 = π 1 (z 2 ) in (out(z ′ 1 ) | out(z ′ 2 ))

Equivalence

When processes evolve, sent messages are stored in a substitution ϕ while private names are stored in E. A frame is simply an expression of the form new E.ϕ where dom(ϕ) ⊆ AX. We define dom(new E.ϕ) as dom(ϕ). Intuitively, a frame represents the knowledge of an attacker. Intuitively, two sequences of messages are indistinguishable to an attacker if he cannot perform any test that could distinguish them. This is typically modeled as static equivalence [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF]. Here, we consider of variant of [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF] where the attacker is also given the ability to observe when the evaluation of a term fails, as defined for example in [START_REF] Cheval | Lengths May Break Privacy -or How to Check for Equivalences With Length[END_REF]. Definition 3.2 (Static Equivalence). Two ground frames new E.ϕ and new E ′ .ϕ ′ are statically equivalent if and only if they have the same domain, and for all attacker terms R, S with variables in dom(ϕ) = dom(ϕ ′ ), we have

(Rϕ = ↓ Sϕ) ⇐⇒ (Rϕ ′ = ↓ Sϕ ′ )
Then two processes P and Q are in equivalence if no matter how the adversary interacts with P, a similar interaction may happen with Q, with equivalent resulting frames. Let P, Q be two processes. We write P ⊑ t Q if for all (s,ψ , σ ) ∈ trace(P ), there exists (s ′ ,ψ ′ , σ ′ ) ∈ trace(Q ) such that s = τ s ′ and ψ σ and ψ ′ σ ′ are statically equivalent. We say that P and Q are trace equivalent, and we write

l ::= LL | HL | HH T ::= l | T * T | key l (T ) | (T ) k | {T } k | τ l,a n ; τ l ′ ,a m with a ∈ {1, ∞} | T ∨ T
P ≈ t Q, if P ⊑ t Q and Q ⊑ t P.
Note that this definition already includes the attacker's behavior, since processes may input any message forged by the attacker.

Example 3.4. As explained in Section 2, ballot privacy is typically modeled as an equivalence property [START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF] that requires that an attacker cannot distinguish when Alice is voting 0 and Bob is voting 1 from the scenario where the two votes are swapped.

Continuing Example 3.1, ballot privacy of Helios can be expressed as follows:

new r a .V oter (k a , 0, r a ) | new r b .V oter (k b , 1, r b ) | P S ≈ t new r a .V oter (k a , 1, r a ) | new r b .V oter (k b , 0, r b ) | P S

TYPING

We now introduce a type system to statically check trace equivalence between processes. Our typing judgements thus capture properties of pairs of terms or processes, which we will refer to as left and right term or process, respectively.

Types

A selection of the types for messages are defined in Figure 3 and explained below. We assume three security labels (namely, HH, HL, LL), ranged over by l, whose first (resp. second) component denotes the confidentiality (resp. integrity) level. Intuitively, messages of high confidentiality cannot be learned by the attacker, while messages of high integrity cannot originate from the attacker. Pair types describe the type of their components, as usual. Type key l (T ) describes keys of security level l used to encrypt (or sign) messages of type T . The type (T ) k (resp. {T } k ) describes symmetric (resp. asymmetric) encryptions with key k of a message of type T . The type τ l,a i describes nonces and constants of security level l: the label a ranges over {∞, 1}, denoting whether the nonce is bound within a replication or not (constants are always typed with a = 1). We assume a different identifier i for each constant and restriction in the process. The type τ l,1 i is populated by a single name, (i.e., i describes a constant or a non-replicated nonce) and τ l,∞ i is a special type, that is instantiated to τ l,1 i j in the jth replication of the process. Type τ l,a n ; τ l ′ ,a m is a refinement type that restricts the set of values which can be taken by a message to values of type τ l,a n on the left and type τ l ′ ,a m on the right. For a refinement type τ l,a n ; τ l,a n with equal types on both sides we simply write τ l,a n . Messages of type T ∨ T ′ are messages that can have type T or type T ′ .

Constraints

When typing messages, we generate constraints of the form (M ∼ N ), meaning that the attacker sees M and N in the left and right process, respectively, and these two messages are thus required to be indistinguishable.

Typing Messages

Typing judgments are parametrized over a typing environment Γ, which is a list of mappings from names and variables to types. The typing judgement for messages is of the form the form Γ ⊢ M ∼ N : T → c which reads as follows: under the environment Γ, M and N are of type T and either this is a high confidentiality type (i.e., M and N are not disclosed to the attacker) or M and N are indistinguishable for the attacker assuming the set of constraints c holds true. We present an excerpt of the typing rules for messages in Figure 4 and comment on them in the following.

Confidential nonces (i.e. nonces with label l = HH or l = HL) are typed with their label from the typing environment. As the attacker may not observer them, they may be different in the left and the right message and we do not add any constraints (TNonce). Public terms are given type LL if they are the same in the left and the right message (TNonceL, TCstFN, TPubKey, TVKey). We require keys and variables to be the same in the two processes, deriving their type from the environment (TKey and TVar). The rule for pairs operates recursively component-wise (TPair).

For symmetric key encryptions (TEnc), we have to make sure that the payload type matches the key type (which is achieved by rule TEncH). We add the generated ciphertext to the set of constraints, because even though the attacker cannot read the plaintext, he can perform an equality check on the ciphertext that he observed. If we type an encryption with a key that is of low confidentiality

T <: T (SRefl) T <: HL (SHigh) T <: T ′ T ′ <: T ′′ T <: T ′′ (STrans) LL * LL <: LL (SPairL) T 1 <: T ′ 1 T 2 <: T ′ 2 T 1 * T 2 <: T ′ 1 * T ′ 2 (SPair) HH * T <: HH (SPairS)
T * HH <: HH (SPairS') key l (T ) <: l (SKey)

T <: T ′ (T ) k <: (T ′ ) k (SEnc) T <: T ′ {T } k <: {T ′ } k (SAenc)
Figure 5: Subtyping Rules (i.e., the attacker has access to it), then we need to make sure the payload is of type LL, because the attacker can simply decrypt the message and recover the plaintext (TEncL). The rules for asymmetric encryption are the same, with the only difference that we can always chose to ignore the key type and use type LL to check the payload. This allows us to type messages produced by the attacker, which has access to the public key but does not need to respect its type. Signatures are also handled similarly, the difference here is that we need to type the payload with LL even if an honest key is used, as the signature does not hide the content. The first typing rule for hashes (THash) gives them type LL and adds the term to the constraints, without looking at the arguments of the hash function: intuitively this is justified, because the hash function makes it impossible to recover the argument. The second rule (THashL) gives type LL only if we can also give type LL to the argument of the hash function, but does not add any constraints on its own, it is just passing on the constraints created for the arguments. This means we are typing the message as if the hash function would not have been applied and use the message without the hash, which is a strictly stronger result. Both rules have their applications: while the former has to be used whenever we hash a secret, the latter may be useful to avoid the creation of unnecessary constraints when hashing terms like constants or public nonces. Rule THigh states that we can give type HL to every message, which intuitively means that we can treat every message as if it were confidential. Rule TSub allows us to type messages according to the subtyping relation, which is standard and defined in Figure 5. Rule TOr allows us to give a union type to messages, if they are typable with at least one of the two types. TLR 1 and TLR ∞ are the introduction rules for refinement types, while TLR' and TLRL' are the corresponding elimination rules. Finally, TLRVar allows to derive a new refinement type for two variables for which we have singleton refinement types, by taking the left refinement of the left variable and the right refinement of the right variable. We will see application of this rule in the e-voting protocol, where we use it to combine A's vote (0 on the left, 1 on the right) and B's vote (1 on the left, 0 on the right), into a message that is the same on both sides.

Γ(n) = τ l,a n Γ(m) = τ l,a m l ∈ {HH, HL} Γ ⊢ n ∼ m : l → ∅ (TNonce) Γ(n) = τ LL,a n Γ ⊢ n ∼ n : LL → ∅ (TNonceL) a ∈ C ∪ F N Γ ⊢ a ∼ a : LL → ∅ (TCstFN) k ∈ dom(Γ) Γ ⊢ pk(k ) ∼ pk(k ) : LL → ∅ (TPubKey) k ∈ dom(Γ) Γ ⊢ M ∼ N : T → c (TSub) Γ ⊢ M ∼ N : T → c Γ ⊢ M ∼ N : T ∨ T ′ → c (TOr) Γ(m) = τ l,1 m or m ∈ F N ∪ C ∧ l = LL Γ(n) = τ l ′ ,1 n or n ∈ F N ∪ C ∧ l ′ = LL Γ ⊢ m ∼ n : τ l,1 m ; τ l ′ ,1 n → ∅ (TLR 1 ) Γ(m) = τ l,∞ m Γ(n) = τ l ′ ,∞ n Γ ⊢ m ∼ n : τ l,∞ m ; τ l ′ ,∞ n → ∅ (TLR ∞ ) Γ ⊢ M ∼ N : τ l,a m ; τ l,a n → c l ∈ {HL, HH} Γ ⊢ M ∼ N : l → c (TLR') Γ ⊢ M ∼ N : τ LL,a n ; τ LL,a n → c Γ ⊢ M ∼ N : LL → c (TLRL') Γ ⊢ x ∼ x : τ l,1 m ; τ l ′ ,1 n → ∅ Γ ⊢ y ∼ y : τ l ′′ ,1 m ′ ; τ l ′′′ ,1 n ′ → ∅ Γ ⊢ x ∼ y : τ l,1 m ; τ l ′′′ ,1 n ′ → ∅ (TLRVar)

Typing Processes

The typing judgement for processes is of the form Γ ⊢ P ∼ Q → C and can be interpreted as follows: If two processes P and Q can be typed in Γ and if the generated constraint set C is consistent, then P and Q are trace equivalent. We assume in this section that P and Q do not contain replication and that variables and names are renamed to avoid any capture. We also assume processes to be given with type annotations for nonces. When typing processes, the typing environment Γ is passed down and extended from the root towards the leafs of the syntax tree of the process, i.e., following the execution semantics. The generated constraints C however, are passed up from the leafs towards the root, so that at the root we get all generated constraints, modeling the attacker's global view on the process execution.

More precisely, each possible execution path of the processthere may be multiple paths because of conditionals -creates its own set of constraints c together with the typing environment Γ that contains types for all names and variables appearing in c.

Hence a constraint set C is a set elements of the form (c, Γ) for a set of constraints c. The typing environments are required in the constraint checking procedure, as they helps us to be more precise when checking the consistency of constraints.

An excerpt of our typing rules for processes is presented in Figure 6 and explained in the following. Rule PZero copies the current typing environment in the constraints and checks the wellformedness of the environment (Γ ⊢ ⋄), which is defined as expected. Messages output on the network are possibly learned by the attacker, so they have to be of type LL (POut). The generated

Γ ⊢ ⋄ Γ does not contain union types Γ ⊢ 0 ∼ 0 → (∅, Γ) (PZero) Γ ⊢ P ∼ Q → C Γ ⊢ M ∼ N : LL → c Γ ⊢ out(M ).P ∼ out(N ).Q → C∪ ∀ c (POut) Γ, x : LL ⊢ P ∼ Q → C Γ ⊢ in(x ).P ∼ in(x ).Q → C (PIn) Γ, n : τ l,a n ⊢ P ∼ Q → C Γ ⊢ new n : τ l,a n .P ∼ new n : τ l,a n .Q → C (PNew) Γ ⊢ P ∼ Q → C Γ ⊢ P ′ ∼ Q ′ → C ′ Γ ⊢ P ∼ Q → C Γ ⊢ P ′ ∼ Q ′ → C ′ Γ ⊢ M ∼ N : LL → c Γ ⊢ M ′ ∼ N ′ : LL → c ′ Γ ⊢ if M = M ′ then P else P ′ ∼ if N = N ′ then Q else Q ′ → C ∪ C ′ ∪ ∀ (c ∪ c ′ ) (PIfL) Γ ⊢ M 1 ∼ N 1 : τ l,1 m ; τ l ′ ,1 n → ∅ Γ ⊢ M 2 ∼ N 2 : τ l ′′ ,1 m ′ ; τ l ′′′ ,1 n ′ → ∅ b = (τ l,1 m ? = τ l ′′ ,1 m ′ ) b ′ = (τ l ′ ,1 → ∅ Γ ⊢ P ∼ Q → C Γ ⊢ P ′ ∼ Q ′ → C ′ Γ ⊢ if M 1 = M 2 then P else P ′ ∼ if N 1 = N 2 then Q else Q ′ → C ∪ C ′ (PIfLR*)
Figure 6: Rules for processes constraints are added to each element of the constraint set for the continuation process, using the operator ∪ ∀ defined as

C∪ ∀ c ′ := (c ∪ c ′ , Γ) | (c, Γ) ∈ C .
Conversely, messages input from the network are given type LL (PIn). Rule PNew introduces a new nonce, which may be used in the continuation processes. While typing parallel composition (PPar), we type the individual subprocesses and take the product union of the generated constraint sets as the new constraint set. The product union of constraint sets is defined as

C∪ × C ′ := {(c ∪ c ′ , Γ ∪ Γ ′ ) | (c, Γ) ∈ C ∧ (c ′ , Γ ′ ) ∈ C ′ ∧ Γ, Γ ′ are compatible}
where compatible environments are those that agree on the type of all arguments of the shared domain. This operation models the fact that a process P | P ′ can have every trace that is a combination of any trace of P with any trace of P ′ . The branches that are discarded due to incompatible environments correspond to impossible executions (e.g., taking the left branch in P and the right branch in P ′ in two conditionals with the same guard). POr is the elimination rule for union types, which requires the continuation process to be welltyped with both types.

To ensure that the destructor application fails or succeeds equally in the two processes, we allow only the same destructor to be applied to the same variable in both processes (PLet). As usual, we then type-check the then as well as the else branch and then take the union of the corresponding constraints. The typing rules for destructors are presented in Figure 7. These are mostly standard: for instance, after decryption, the type of the payload is determined by the one of the decryption key, as long as this is of high integrity (DDecH). We can as well exploit strong types for ciphertexts, typically introduced by verifying a surrounding signature (see, e.g., the types for Helios) to derive the type of the payload (DDecT). In the case of public key encryption, we have to be careful, since the public encryption key is accessible to the attacker: we thus give the payload type T ∨ LL (rule DAdecH). For operations involving corrupted keys (label LL) we know that the payload is public and hence give the derived message type LL.

In the special case in which we know that the concrete value of the argument of the destructor application is a nonce or constant due to a refinement type, and we know statically that any destructor application will fail, we only need to type-check the else branch (PLetLR). As for destructor applications, the difficulty while typing conditionals is to make sure that the same branch is taken in both processes (PIfL). To ensure this we use a trick: We type both the left and the right operands of the conditional with type LL and add both generated sets of constraints to the constraint set. Intuitively, this means that the attacker could perform the equality test himself, since the guard is of type LL, which means that the conditional must take the same branch on the left and on the right. In the special case in which we can statically determine the concrete value of the terms in the conditional (because the corresponding type is populated by a singleton), we have to typecheck only the single combination of branches that will be executed (PIfLR). Another special case is if the messages on the right are of type HH and the ones on the left of type LL. As a secret of high integrity can never be equal to a public value of low integrity, we know that both processes will take the else branch (PIfS). This rule is crucial, since it may allow us to prune the low typing branch of asymmetric decryption. The last special case for conditionals is when we have a refinement type with replication for both operands of the equality check (PIfLR*). Although we know that the nonces on both sides are of the same type and hence both are elements of the same set, we cannot assume that they are equal, as the sets are infinite, unlike in rule PIfLR. Yet, concrete instantiations of nonces will have the same index for the left and the right process. This is because we check for a variant of diff-equivalence. This ensures that the equality check always yields the same result in the two processes. All these special cases highlight how a careful treatment of names in terms of equivalence classes (statically captured by types) is a powerful device to enhance the expressiveness of the analysis.

Finally, notice that we do not have any typing rule for replication: this is in line with our general idea of typing a bounded number of sessions and then extending this result to the unbounded case in the constraint checking phase, as detailed in Section 6.

CONSISTENCY OF CONSTRAINTS

Our type system guarantees trace equivalence of two processes only if the generated constraints are consistent. In this section we give a slightly simplified definition of consistency of constraints and explain how it captures the attacker's capability to distinguish processes based on their outputs.

To define consistency, we need the following ingredients:

• ϕ l (c) and ϕ r (c) denote the frames that are composed of the left and the right terms of the constraints respectively (in the same order).

• ϕ Γ

LL denotes the frame that is composed of all low confidentiality nonces and keys in Γ, as well as all public encryption keys and verification keys in Γ. This intuitively corresponds to the initial knowledge of the attacker.

• Let E Γ be the set of all nonces occurring in Γ.

• Two ground substitutions σ , σ ′ are well-formed in Γ if they preserve the types for variables in Γ (i.e., Γ ⊢ σ (x ) ∼ σ ′ (x ) : Γ(x ) → c x ).

Definition 5.1 (Consistency).

A set of constraints c is consistent in an environment Γ if for all substitutions σ ,σ ′ well-typed in Γ the frames new We define consistency of constraints in terms of static equivalence, as this notion exactly captures all capabilities of our attacker: to distinguish two processes, he can arbitrarily apply constructors and destructors on observed messages to create new terms, on which he can then perform equality tests or check the applicability of destructors. We require that this property holds for any welltyped substitutions, to soundly cover that fact that we do not know the content of variables statically, except for the information we get by typing. In Section 6.3 we introduce an algorithm to check consistency of constraints.

E Γ .(ϕ Γ LL ∪ ϕ l (c)σ ) and new E Γ .(ϕ Γ LL ∪ ϕ r (c)σ ′ ) are statically equivalent. We say that (c, Γ) is consistent if c is consistent Γ(k ) = key HH (T ) Γ(x ) = LL Γ ⊢ dec(x, k ) : T (DDecH) Γ(k ) = key LL (T ) Γ(x ) = LL Γ ⊢ dec(x, k ) : LL (DDecL) Γ(x ) = (T ) k Γ ⊢ dec(x, k ) : T (DDecT) Γ(k ) = key HH (T ) Γ(x ) = LL Γ ⊢ adec(x, k ) : T ∨ LL (DAdecH) Γ(k ) = key LL (T ) Γ(x ) = LL Γ ⊢ adec(x, k ) : LL (DAdecL) Γ(x ) = {T } k Γ ⊢ adec(x, k ) : T (DAdecT) Γ(k ) = key HH (T ) Γ(x ) = LL Γ ⊢ checksign(x, vk(k )) : T (DCheckH) Γ(k ) = key LL (T ) Γ(x ) = LL Γ ⊢ checksign(x, vk(k )) : LL (DCheckL) Γ(x ) = T * T ′ Γ ⊢ π 1 (x ) : T (DFst) Γ(x ) = T * T ′ Γ ⊢ π 2 (x ) : T ′ (DSnd) Γ(x ) = LL Γ ⊢ π 1 (x ) : LL (DFstL) Γ(x ) = LL Γ ⊢ π 2 (x ) : LL (DSndL)

MAIN RESULTS

In this section, we state our two main soundness theorems, entailing trace equivalence by typing for the bounded and unbounded case, and we explain how to automatically check consistency.

Soundness of the type system

Our type system soundly enforces trace equivalence: if we can typecheck P and Q then P and Q are equivalent, provided that the corresponding constraint set is consistent. Theorem 6.1 (Typing implies trace eqivalence). For all P, Q, and C, for all Γ containing only keys, if Γ ⊢ P ∼ Q → C and C is consistent, then P ≈ t Q.

To prove this theorem, we first show that typing is preserved by reduction, and guarantees that the same actions can be observed on both sides. More precisely, we show that if P and Q are multisets of processes that are pairwise typably equivalent (with consistent constraints), and if a reduction step with action α can be performed to reduce P into P ′ , then Q can be reduced in one or several steps, with the same action α, to some multiset Q ′ such that the processes in P ′ and Q ′ are still typably equivalent (with consistent constraints). This is done by carefully examining all the possible typing rules used to type the processes in P and Q. In addition we show that the frames of messages output when reducing P and Q are typably equivalent with consistent constraints; and that this entails their static equivalence.

This implies that if P and Q are typable with a consistent constraint, then for each trace of P, by induction on the length of the trace, there exists a trace of Q with the same sequence of actions, and with a statically equivalent frame. That is to say P ⊑ t Q. Similarly we show Q ⊑ t P, and we thus have P ≈ t Q.

Since we do not have typing rules for replication, Theorem 6.1 only allows us to prove equivalence of protocols for a finite number of sessions. An arguably surprising result, however, is that, thanks to our infinite nonce types, we can prove equivalence for an unbounded number of sessions, as detailed in the next section.

Typing replicated processes

For more clarity, in this section, without loss of generality we consider that for each infinite nonce type τ l,∞ m appearing in the processes, the set of names BN contains an infinite number of fresh names {m i | i ∈ N} which do not appear in the processes or environments. We similarly assume that for all the variables x appearing in the processes, the set X of all variables also contains fresh variables {x i | i ∈ N} which do not appear in the processes or environments.

Intuitively, whenever we can typecheck a process of the form new n : τ l,1 n . new m : τ l,∞ m . P, we can actually typecheck

new n : τ l,1 n . (new m 1 : τ l,1 m 1 .P 1 | . . . | new m k : τ l,1 m k .P k )
where in P i , the nonce m has been replaced by m i and variables x have been renamed to x i . Formally, we denote by [ t ] Γ i , the term t in which names n such that Γ(n) = τ l,∞ n for some l are replaced by n i , and variables x are replaced by x i .

Similarly, when a term is of type τ l,∞ m ; τ l ′ ,∞ p , it can be of type τ l,1 m i ; τ l ′ ,1 p i for any i. The nonce type τ l,∞ m represents infinitely many nonces (one for each session). That is, for n sessions, the type τ l,∞ m ; τ l ′ ,∞ p represents all τ l,1 m i ; τ l ′ ,1 p i . Formally, given a type T , we define its expansion to n sessions, denoted [ T ] n , as follows.

[

l ] n = l [ T * T ′ ] n = [ T ] n * [ T ′ ] n [ T + T ′ ] n = [ T ] n + [ T ′ ] n key l (T ) n = key l ([ T ] n ) (T ) k n = ([ T ] n ) k [ {T } k ] n = {[ T ] n } k [ T ∨ T ′ ] n = [ T ] n ∨ [ T ′ ] n τ l,1 m ; τ l ′ ,1 p n = τ l,1 m ; τ l ′ ,1 p τ l,∞ m ; τ l ′ ,∞ p n = n j=1 τ l,1 m j ; τ l ′ ,1 p j
where l, l ′ ∈ {LL, HH, HL}, k ∈ K . Note that the size of the expanded type [ T ] n depends on n.

We need to adapt typing environments accordingly. For any typing environment Γ, we define its renaming for session i as:

[ Γ ] i = {x i : T | Γ(x ) = T } ∪ {k : T | Γ(k ) = T } ∪ {m : τ l,1 m | Γ(m) = τ l,1 m } ∪ {m i : τ l,1 m i | Γ(m) = τ l,∞ m }.
and then its expansion to n sessions as

[ Γ ] n i = {x i : [ T ] n | [ Γ ] i (x i ) = T } ∪ {k : [ T ] n | [ Γ ] i (k ) = T } ∪ {m : τ l,1 m | [ Γ ] i (m) = τ l,1 m }.
Note that in [ Γ ] n i , due to the expansion, the size of the types depends on n.

By construction, the environments contained in the constraints generated by typing do not contain union types. However, refinement types with infinite nonce types introduce union types when expanded. In order to recover environments without union types after expanding, which, as we will explain in the next subsection, is needed for our consistency checking procedure, we define branches([ Γ ] n i ) as the set of all Γ ′ , with the same domain as [ Γ ] n i , such that for all x, Γ ′ (x ) is not a union type, and either

• [ Γ ] n i (x ) = Γ ′ (x ); • or there exist types T 1 ,. . . ,T k ,T ′ 1 ,. . . ,T ′ k ′ such that [ Γ ] n i (x ) = T 1 ∨ . . . ∨ T k ∨ Γ ′ (x ) ∨ T ′ 1 ∨ . . . ∨ T ′ k ′
Finally, when typechecking two processes containing nonces with infinite nonce types, we collect constraints that represent families of constraints.

Given a set of constraints c, and an environment Γ, we define the renaming of c for session

i in Γ as [ c ] Γ i = {[ u ] Γ i ∼ [ v ] Γ i | u ∼ v ∈ c}. This is propagated to constraint sets as follows: the renaming of C for session i is [ C ] i = {([ c ] Γ i , [ Γ ] i ) | (c, Γ) ∈ C} and its expansion to n sessions is [ C ] n i = {([ c ] Γ i , Γ ′ ) | ∃Γ. (c, Γ) ∈ C ∧ Γ ′ ∈ branches([ Γ ] n i )}.
Again, note that the size of [ C ] i does not depend on the number of sessions considered, while the size of the types present in [ C ] n i does. For example, for

C = {({h(x ) ∼ h(x )}, [x : τ HH,∞ m ; τ HH,∞ p ])}, we have [ C ] i = {({h(x i ) ∼ h(x i )}, [x i : τ HH,∞ m ; τ HH,∞ p ])} and [ C ] n i = {({h(x i ) ∼ h(x i )}, [x i : n j=1 τ HH,1 m j ; τ HH,1
p j ])}. Our type system is sound for replicated processes provided that the collected constraint sets are consistent, when instantiated with all possible instantiations of the nonces and keys. Theorem 6.2. Consider P, Q, P ′ ,Q ′ , C, C ′ , such that P, Q and P ′ , Q ′ do not share any variable. Consider Γ, containing only keys and nonces with types of the form τ l,1 n . Assume that P and Q only bind nonces with infinite nonce types, i.e. using new m : τ l,∞ m for some label l; while P ′ and Q ′ only bind nonces with finite types, i.e. using new m : τ l,1 m . Let us abbreviate by new n the sequence of declarations of each nonce m ∈ dom(Γ). If

• Γ ⊢ P ∼ Q → C, • Γ ⊢ P ′ ∼ Q ′ → C ′ , • C ′ ∪ × (∪ ×1≤i ≤n [ C ] n i ) is consistent for all n, then new n. ((!P ) | P ′ ) ≈ t new n. ((!Q ) | Q ′ ).
Theorem 6.1 requires to check consistency of one constraint set. Theorem 6.2 now requires to check consistency of an infinite family of contraint sets. Instead of deciding consistency, we provide a procedure that checks a slightly stronger condition.

Procedure for consistency

Checking consistency of a set of constraints amounts to checking static equivalence of the corresponding frames. Our procedure follows the spirit of [START_REF] Abadi | Reconciling Two Views of Cryptography[END_REF] for checking computational indistinguishability: we first open encryption, signatures and pairs as much as possible. Note that the type of a key indicates whether it is public or secret. The two resulting frames should have the same shape. Then, for unopened components, we simply need to check that they satisfy the same equalities.

From now on, we only consider constraint sets that can actually be generated when typing processes, as these are the only ones for which we need to check consistency.

Formally, the procedure check_const is described in Figure 8. It consists of four steps. First, we replace variables with refinements of finite nonce types by their left and right values. In particular a variable with a union type is not associated with a single value and thus cannot be replaced. This is why the branching operation needs to be performed when expanding environments containing refinements with types of the form τ l,∞ n . Second, we recursively open the constraints as much as possible. Third, we check that the resulting constraints have the same shape. Finally, as soon as two constraints M ∼ M ′ and N ∼ N ′ are such that M, N are unifiable, we must have M ′ = N ′ , and conversely. The condition is slightly more involved, especially when the constraints contain variables of refined types with infinite nonce types. Example 6.3. Continuing Example 3.1, when typechecked with appropriate key types, the simplified model of Helios yields constraint sets containing notably the following two constraints.

{ aenc(⟨0, r a ⟩, pk(k s )) ∼ aenc(⟨1, r a ⟩, pk(k s )), aenc(⟨1, r b ⟩, pk(k s )) ∼ aenc(⟨0, r b ⟩, pk(k s )) }
For simplicity, consider the set c containing only these two constraints, together with a typing environment Γ where r a and r b are respectively given types τ HH,1 r a and τ HH,1 r b , and k s is given type key HH (T ) for some T .

step1 Γ (c ) := c σ F , σ ′ F , with F := {x ∈ dom(Γ) | ∃m, n, l, l ′ . Γ(x ) = τ l, 1 m ; τ l ′ , 1 n } and σ F , σ ′ F defined by          • dom(σ F ) = dom(σ ′ F ) = F • ∀x ∈ F . ∀m, n, l, l ′ . τ l, 1 m ; τ l ′ , 1 n ⇒ σ F (x ) = m ∧ σ ′ F (x ) = n step2 Γ (c ) is recursively defined by, for all M , N , M ′ , N ′ : • step2 Γ ( {⟨M, N ⟩ ∼ ⟨M ′ , N ′ ⟩} ∪ c ′ ) := step2 Γ ( {M ∼ M ′ , N ∼ N ′ } ∪ c ′ ) • For all k ∈ K , if ∃T .Γ(k ) = key LL (T ): • step2 Γ ( {enc(M, k ) ∼ enc(M ′ , k ) } ∪ c, c ′ ) := step2 Γ ( {M ∼ M ′ } ∪ c ′ ) • step2 Γ ( {aenc(M, pk(k )) ∼ aenc(M ′ , pk(k )) } ∪ c, c ′ ) := step2 Γ ( {M ∼ M ′ } ∪ c ′ ) • step2 Γ ( {sign(M, k ) ∼ sign(M ′ , k ) } ∪ c ′ ) := step2 Γ ( {M ∼ M ′ } ∪ c ′ )
• For all k ∈ K , if ∃T .Γ(k ) = key HH (T ):

step2 Γ ( {sign(M, k ) ∼ sign(M ′ , k ) } ∪ c ′ ) := {sign(M, k ) ∼ sign(M ′ , k ) } ∪ step2 Γ ( {M ∼ M ′ } ∪ c ′ )
• For all other terms M, N : The procedure check_const({(c, Γ)}) can detect that the constraint c is consistent and returns true. Indeed, as c does not contain variables, step1 Γ (c) simply returns (c, Γ). Since c only contains messages encrypted with secret keys, step2 Γ (c) also leaves c unmodified. step3 Γ (c) then returns true, since the messages appearing in c are messages asymmetrically encrypted with secret keys, which contain a secret nonce (r a or r b ) directly under pairs. Finally step4 Γ (c) trivially returns true, as the messages aenc(⟨0, r a ⟩, pk(k s )) and aenc(⟨1, r b ⟩, pk(k s )) cannot be unified, as well as the messages aenc(⟨1, r a ⟩, pk(k s )) and aenc(⟨0, r b ⟩, pk(k s )).

step2 Γ ( {M ∼ N } ∪ c ′ ) := {M ∼ N } ∪ step2 Γ (c ′ ).
∀x ∈ dom(µ ). ∃l, l ′ , m, p . (Γ(x ) = τ l, ∞ m ; τ l ′ , ∞ p ) ⇒ (x µ ∈ X ∨ ∃i . x µ = m i ) we have M ′ α θ = N ′ α θ where ∀x ∈ dom(µ ).∀l, l ′ , m, p, i . (Γ(x ) = τ l, ∞ m ; τ l ′ , ∞ p ∧ µ (x ) = m i ) ⇒ θ (x ) = p i
Consider now the following set c ′ , where encryption has not been randomised:

c ′ = { aenc(0, pk(k s )) ∼ aenc(1, pk(k s )), aenc(1, pk(k s )) ∼ aenc(0, pk(k s )) }
The procedure check_const({(c ′ , Γ)}) returns false. Indeed, contrary to the case of c, step3 Γ (c ′ ) fails, as the encrypted message do not contain a secret nonce. Actually, the corresponding frames are indeed not statically equivalent since the adversary can reconstruct the encryption of 0 and 1 with the key pk(k s ) (in his initial knowledge), and check for equality.

For constraint sets without infinite nonce types, check_const entails consistency. Theorem 6.4. Let C be a set of constraints such that

∀(c, Γ) ∈ C. ∀l, l ′ , m, p. Γ(x ) τ l,∞ m ; τ l ′ ,∞ p .
If check_const(C) = true, then C is consistent.

We prove this theorem by showing that, for each of the first two steps of the procedure, if stepi Γ (c) is consistent in Γ, then c is consistent in Γ. It then suffices to check the consistency of the constraint step2 Γ (step1 Γ (c)) in Γ. Provided that step3 Γ holds, we show that this constraint is saturated in the sense that any message obtained by the attacker by decomposing terms in the constraint already occurs in the constraint; and the constraint only contains messages which cannot be reconstructed by the attacker from the rest of the constraint. Using this property, we finally prove that the simple unification tests performed in step4 are sufficient to ensure static equivalence of each side of the constraint for any well-typed instantiation of the variables.

As a direct consequence of Theorems 6.1 and 6.4, we now have a procedure to prove trace equivalence of processes without replication.

For proving trace equivalence of processes with replication, we need to check consistency of an infinite family of constraint sets, as prescribed by Theorem 6.2. As mentioned earlier, not only the number of constraints is unbounded, but the size of the type of some (replicated) variables is also unbounded (i.e. of the form n j=1 τ l,1 m j ; τ l ′ ,1 p j ). We use here two ingredients: we first show that it is sufficient to apply our procedure to two constraints only. Second, we show that our procedure applied to variables with replicated types, i.e. nonce types of the form τ l,∞ n implies consistency of the corresponding constraints with types of unbounded size. C is consistent: since m, p are secret, the attacker cannot distinguish between their hashes. However ∪ ×1≤i ≤n [ C ] n i contains (together with some environment):

Two constraints suffice

{h(m 1 ) ∼ h(p), h(m 2 ) ∼ h(p), . . . , h(m n ) ∼ h(p)}
which is not, since the attacker can notice that the value on the right is always the same, while the value on the left is not.

Note however that the inconsistency of ∪ ×1≤i ≤n [ C ] n i would have been discovered when checking the consistency of two copies of the constraint set only. Indeed,

[ C ] n 1 ∪ × [ C ] n 2
contains (together with some environment):

{h(m 1 ) ∼ h(p), h(m 2 ) ∼ h(p)}
which is already inconsistent, for the same reason.

Actually, checking consistency (with our procedure) of two constraints

[ C ] n 1 and [ C ] n 2 entails consistency of ∪ ×1≤i ≤n [ C ] n i . Note that this does not mean that consistency of [ C ] n 1 and [ C ] n 2 im- plies consistency of ∪ ×1≤i ≤n [ C ] n i .
Instead, our procedure ensures a stronger property, for which two constraints suffice. Theorem 6.5. Let C and C ′ be two constraint sets, which do not contain any common variables. For all n ∈ N,

check_const([ C ] n 1 ∪ × [ C ] n 2 ∪ × [ C ′ ] n 1 ) = true ⇒ check_const((∪ ×1≤i ≤n [ C ] n i )∪ × [ C ′ ] n 1 )
= true. To prove Theorem 6.5, we first (easily) show that if

check_const([ C ] n 1 ∪ × [ C ] n 2 ∪ × C ′ n 1 )
= true, then the first three steps of the procedure check_const can be successfully applied to each element of (∪ ×1≤i ≤n

[ C ] n i )∪ × [ C ′ ] n 1 .
However the case of the fourth step is more intricate. When applying the procedure check_const to an element of the constraint set

(∪ ×1≤i ≤n [ C ] n i )∪ × [ C ′ ] n 1 , if step4
fails, then the constraint contains an inconsistency, i.e. elements M ∼ M ′ and N ∼ N ′ for which the unification condition from step4 does not hold. Then we show that we can find a similar inconsistency when considering only the first two constraint sets, i.e. in

[ C ] n 1 ∪ × [ C ] n 2 ∪ × [ C ′ ] n 1 .
This is done by reindexing the nonces and variables. The proof actually requires a careful examination of the structure of the constraint set

(∪ ×1≤i ≤n [ C ] n i )∪ × [ C ′ ] n 1
, to establish this reindexing.

Reducing the size of types

The procedure check_const applied to replicated types implies consistency of corresponding constraints with unbounded types. Theorem 6.6. Let C be a constraint set. Then for all i,

check_const([ C ] i ) = true ⇒ ∀n ≥ 1.check_const([ C ] n i ) = true
Again here, it is rather easy to show that if check_const([ C ] i ) = true then the first three steps of the procedure check_const can successfully be applied to each element of [ C ] n i . The case of step4 is more involved. The property holds thanks to the condition on the most general unifier expressed in step4. Intuitively, this condition is written in such a way that if, when applying step4 to an element of [ C ] n i , two messages can be unified, then the corresponding messages (with replicated types) in [ C ] i can be unified with a most general unifier µ satisfying the condition. The proof uses this idea to show that if step4 succeeds on all elements of [ C ] i , then it also succeeds on the elements of [ C ] n i .

6.6 Checking the consistency of the infinite constraint Theorems 6.2, 6.5, and 6.6 provide a sound procedure for checking trace equivalence of processes with and without replication. Theorem 6.7. Let C, and C ′ be two constraint sets without any common variable.

check_const

([ C ] 1 ∪ × [ C ] 2 ∪ × [ C ′ ] 1 ) = true ⇒ ∀n. [ C ′ ] n 1 ∪ × (∪ ×1≤i ≤n [ C ] n i ) is consistent.
All detailed proofs are available online [START_REF] Cortier | A Type System for Privacy Properties[END_REF].

EXPERIMENTAL RESULTS

We have implemented a prototype type-checker TypeEq and applied it on various examples briefly described below.

Symmetric key protocols. For the sake of comparison, we consider 5 symmetric key protocols taken from the benchmark of [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF], and described in [START_REF] Clark | A Survey of Authentication Protocol Literature: Version 1[END_REF]: Denning-Sacco, Wide Mouth Frog, Needham-Schroeder, Yahalom-Lowe, and Otway-Rees. All these protocols aim at exchanging a key k. We prove strong secrecy of the key, as defined in [START_REF] Abadi | Security Protocols and their Properties[END_REF], i.e., P (k 1 ) ≈ t P (k 2 ) where k 1 and k 2 are public names. Intuitively, an attacker should not be able to tell which key is used even if he knows the two possible values in advance. For some of the protocols, we truncated the last step, when it consists in using the exchanged key for encryption, since our framework currently covers only encryption with long-term (fixed) keys.

Asymmetric key protocols. In addition to the symmetric key protocols, we consider the well-known Needham-Schroeder-Lowe (NSL) protocol [START_REF] Lowe | Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR[END_REF] and we again prove strong secrecy of the nonce sent by the receiver (Bob).

Helios. We model the Helios protocol for two honest voters and infinitely many dishonest ones, as informally described in Section 2. The corresponding process includes a non trivial else branch, used to express the weeding phase [START_REF] Cortier | Attacking and Fixing Helios: An Analysis of Ballot Secrecy[END_REF], where dishonest ballots equal to some honest one are discarded. As emphasised in Section 2, Helios is secure only if honest voters vote at most once. Therefore the protocol includes non replicated processes (for voters) as well as a replicated process (to handle dishonest ballots).

All our experiments have been run on a single Intel Xeon E5-2687Wv3 3.10GHz core, with 378GB of RAM (shared with the 19 other cores). All corresponding files can be found online at [START_REF] Cortier | TypeEQ. Source Code[END_REF].

Bounded number of sessions

We first compare our tool with tools designed for a bounded number of sessions: SPEC [START_REF] Dawson | Automating Open Bisimulation Checking for the Spi Calculus[END_REF], APTE (and its APTE-POR variant) [START_REF] Baelde | Partial Order Reduction for Security Protocols[END_REF][START_REF] Cheval | APTE: an Algorithm for Proving Trace Equivalence[END_REF], Akiss [START_REF] Chadha | Automated Verification of Equivalence Properties of Cryptographic Protocols[END_REF], or SAT-Equiv [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF]. The protocol models may slightly differ due to the subtleties of each tool. For example, several of these tools require simple processes where each sub-process emits on a distinct channel. We do not need such an assumption. In addition, SAT-Equiv only covers symmetric encryption and therefore could not be applied to Helios or NSL. SAT-Equiv further assumes protocols to be well-typed, which sometimes requires to tag protocols. Since we consider only untagged versions (following the original description of each protocol), SAT-Equiv failed to prove the Otway-Rees protocol. Moreover, Helios involves non-trivial else branches, which are only supported by APTE.

The number of sessions we consider denotes the number of processes in parallel in each scenario. For symmetric key protocols, we start with a simple scenario with only two honest participants A, B and a honest server S (3 sessions). We consider increasingly more complex scenarios (6, 7, 10, 12, and 14 sessions) featuring a dishonest agent C. In the complete scenario (14 sessions) each agent among A, B (and C) runs the protocol once as the initiator, and once as the responder with each other agent (A, B, C). In the case of NSL, we similarly consider a scenario with two honest agents A, B running the protocol once (2 sessions), and two scenarios with an additional dishonest agent C, up to the complete scenario (8 sessions) where each agent runs NSL once as initiator, once as responder, with each agent. For Helios, we consider 2 honest voters, and one dishonest voter only, as well as a ballot box. The corresponding results are reported in Figure 9. We write TO for Time Out (12 hours), MO for Memory Out (more than 64 GB of RAM), SO for Stack Overflow, BUG in the case of APTE, when the proof failed due to bugs in the tool, and x when the tool could not handle the protocol for the reasons discussed previously. In all cases, our tool is almost instantaneous and outperforms by orders of magnitude the competitors.

Unbounded numbers of sessions

We then compare our type-checker with ProVerif [START_REF] Blanchet | Automated Verification of Selected Equivalences for Security Protocols[END_REF], for an unbounded number of sessions, on three examples: Helios, Denning-Sacco, and NSL. As expected, ProVerif cannot prove Helios secure since it cannot express that voters vote only once. This may sound surprising, since proofs of Helios in ProVerif already exist (e.g. [START_REF] Arapinis | When Are Three Voters Enough for Privacy Properties?[END_REF][START_REF] Cortier | Attacking and Fixing Helios: An Analysis of Ballot Secrecy[END_REF]). Interestingly, these models actually implicitly assume a reliable channel between honest voters and the voting server: whenever a voter votes, she first sends her vote to the voting server on a secure channel, before letting the attacker see it. This model prevents an attacker from reading and blocking a message, while this can be easily done in practice (by breaking the connection). We also failed to prove (automatically) Helios in Tamarin [START_REF] Basin | Automated Symbolic Proofs of Observational Equivalence[END_REF]. The reason is that the weeding procedure makes Tamarin enter a loop where it cannot detect that, as soon as a ballot is not weed, it has been forged by the adversary.

For the sake of comparison, we run both tools (ProVerif and TypeEq) on a symmetric protocol (Denning-Sacco) and an asymmetric protocol (Needham-Schroeder-Lowe). The execution times are very similar. The corresponding results are reported in Figure 10.

CONCLUSION

We presented a novel type system for verifying trace equivalence in security protocols. It can be applied to various protocols, with support for else branches, standard cryptographic primitives, as well as a bounded and an unbounded number of sessions. We believe that our prototype implementation demonstrates that this approach is promising and opens the way to the development of an efficient technique for proving equivalence properties in even larger classes of protocols. Several interesting problems remain to be studied. For example, a limitation of ProVerif is that it cannot properly handle global states. We plan to explore this case by enriching our types to express the fact that an event is "consumed". Also, for the moment, our type system only applies to protocols P, Q that have the same structure. One advantage of a type system is its modularity: it is relatively easy to add a few rules without redoing the whole proof. We plan to add rules to cover protocols with different structures (e.g. when branches are swapped). Another direction is the treatment of primitives with algebraic properties (e.g. Exclusive Or, or homomorphic encryption). It seems possible to extend the type system and discharge the difficulty to the consistency of the constraints, which seems easier to handle (since this captures the static case). Finally, our type system is sound w.r.t. equivalence in a symbolic model. An interesting question is whether it also entails computational indistinguishability. Again, we expect that an advantage of our type system is the possibility to discharge most of the difficulty to the constraints.

Figure 1 :

 1 Figure 1: Syntax for processes.

Figure 2 :

 2 Figure 2: Semantics

Figure 3 :

 3 Figure 3: Types for terms (selected)

Figure 4 :

 4 Figure 4: Rules for Messages

Figure 7 :

 7 Figure 7: Destructor Rules

,•

  step3 Γ (c ) := check that for all M ∼ N ∈ c, M and N are both • a key k ∈ K such that ∃T .Γ(k ) = key LL (T ); • nonces m, n ∈ N such that ∃a ∈ {1, ∞}. Γ(n) = τ LL, a n ∧ Γ(m) = τ LL, a n or public keys, verification keys, or constants; • or enc(M ′ , k ), enc(N ′ , k ) such that ∃T .Γ(k ) = key HH (T ); • or either h(M ′ ), h(N ′ ) or aenc(M ′ , pk(k )), aenc(N ′ , pk(k )), where ∃T .Γ(k ) = key HH (T ); such that M ′ and N ′ contain directly under pairs some n with Γ(n) = HH or k such that ∃T .Γ(k ) = key HH (T ); • or sign(M ′ , k ), sign(N ′ , k ) such that ∃T .Γ(k ) = key HH (T ).

  step4 Γ (c ) := If for all M ∼ M ′ and N ∼ N ′ ∈ c such that M , N are unifiable with a most general unifier µ, and such that

and α is the

  restriction of µ to {x ∈ dom(µ ) | Γ(x ) = LL ∧ µ (x ) ∈ N }; and if the symmetric condition for the case where M ′ , N ′ are unifiable holds as well, then return true. check_const(C ) := for all (c, Γ) ∈ C, let c 1 := step2 Γ (step1 Γ (c )) and check that step3 Γ (c 1 ) = true and step4 Γ (c 1 ) = true.

Figure 8 :

 8 Figure 8: Procedure for checking consistency.

1 p. 1 p.

 11 Consistency of a constraint set C does not guarantee consistency of ∪ ×1≤i ≤n [ C ] n i . For example, consider C = {({h(m) ∼ h(p)}, [m : τ HH,∞ m , p : τ HH,1 p ])} which can be obtained when typing new m : τ HH,∞ m . new p : τ HH,out(h(m)) ∼ new m : τ HH,∞ m . new p : τ HH,out(h(p)).

Figure 9 :Figure 10 :

 910 Figure 9: Experimental results for the bounded case

Γ ⊢ vk(k ) ∼ vk(k ) : LL → ∅ (TVKey) Γ(k ) = T Γ ⊢ k ∼ k : T → ∅ (TKey) Γ(x ) = T Γ ⊢ x ∼ x : T → ∅ (TVar) Γ ⊢ M ∼ N : T → c Γ ⊢ M ′ ∼ N ′ : T ′ → c ′ Γ ⊢ ⟨M, M ′ ⟩ ∼ ⟨N , N ′ ⟩ : T * T ′ → c ∪ c ′ (TPair) Γ ⊢ M ∼ N : T → c Γ ⊢ enc(M, k ) ∼ enc(N , k ) : (T ) k → c (TEnc) Γ ⊢ M ∼ N : (T ) k → c Γ(k ) = key HH (T ) Γ ⊢ M ∼ N : LL → c ∪ {M ∼ N } (TEncH) Γ ⊢ M ∼ N : (LL) k → c Γ(k ) = key LL (T ) Γ ⊢ M ∼ N : LL → c (TEncL) Γ ⊢ M ∼ N : T → c Γ ⊢ aenc(M, pk(k )) ∼ aenc(N , pk(k )) : {T } k → c (TAenc) Γ ⊢ M ∼ N : {T } k → c Γ(k ) = key HH (T ) Γ ⊢ M ∼ N : LL → c ∪ {M ∼ N } (TAencH) Γ ⊢ M ∼ N : {LL} k → c k ∈ dom(Γ) Γ ⊢ M ∼ N : LL → c (TAencL) Γ ⊢ M ∼ N : T → c Γ ⊢ M ∼ N : LL → c ′ Γ(k ) = key HH (T ) Γ ⊢ sign(M, k ) ∼ sign(N , k ) : LL → c ∪ c ′ ∪ {sign(M, k ) ∼ sign(N , k )} (TSignH) Γ ⊢ M ∼ N : LL → c Γ(k ) = key LL (T ) Γ ⊢ sign(M, k ) ∼ sign(N , k ) : LL → c (TSignL) names(M ) ∪ names(N ) ∪ vars(M ) ∪ vars(N ) ⊆ dom(Γ) ∪ F N Γ ⊢ h(M ) ∼ h(N ) : LL → {h(M ) ∼ h(N )} (THash) Γ ⊢ M ∼ N : LL → c Γ ⊢ h(M ) ∼ h(N ) : LL → c (THashL) names(M ) ∪ names(N ) ∪ vars(M ) ∪ vars(N ) ⊆ dom(Γ) ∪ F N Γ ⊢ M ∼ N : HL → ∅(THigh)Γ ⊢ M ∼ N : T ′ → c T ′ <: T

Γ ⊢ P | P ′ ∼ Q | Q ′ → C∪ × C ′ (PPar) Γ, x : T ⊢ P ∼ Q → C Γ, x : T ′ ⊢ P ∼ Q → C ′ Γ, x : T ∨ T ′ ⊢ P ∼ Q → C ∪ C ′ (POr) Γ ⊢ d (y) : T Γ, x : T ⊢ P ∼ Q → C Γ ⊢ P ′ ∼ Q ′ → C ′ Γ ⊢ let x = d (y) in P else P ′ ∼ let x = d (y) in Q else Q ′ → C ∪ C ′ (PLet) Γ(y) = τ l,a n ; τ l ′ ,a m Γ ⊢ P ′ ∼ Q ′ → C ′ Γ ⊢ let x = d (y) in P else P ′ ∼ let x = d (y) in Q else Q ′ → C ′ (PLetLR)

n ? = τ l ′′′ ,1 n ′ ) Γ ⊢ P b ∼ Q b ′ → C Γ ⊢ if M 1 = M 2 then P ⊤ else P ⊥ ∼ if N 1 = N 2 then Q ⊤ else Q ⊥ → C (PIfLR) Γ ⊢ P ′ ∼ Q ′ → C ′ Γ ⊢ M ∼ N : → c Γ ⊢ M ′ ∼ N ′ : HH → c ′ Γ ⊢ if M = M ′ then P else P ′ ∼ if N = N ′ then Q else Q ′ → C ′ (PIfS) Γ ⊢ M 1 ∼ N 1 : τ l,∞ m ; τ l ′ ,∞ n → ∅ Γ ⊢ M 2 ∼ N 2 : τ l,∞ m ; τ l ′ ,∞ n

Acknowledgments

This work has been partially supported by the European Research Council (ERC) under the European Union's Horizon 2020 research (grant agreement No 645865-SPOOC).