Un système mobile est un ensemble de composants qui peuvent interagir entre eux, tout en modifiant dynamiquement le système lui-même. Ces interactions contrôlent ainsi la création et la destruction des liaisons entre les composants, mais aussi la création dynamique de nouveaux composants au sein du système. La taille d'un tel système varie au cours du temps, elle n'est pas bornée en général. Un système mobile peut représenter des réseaux de télécommunication, des systèmes reconfigurables, des applications client-serveur sur la toile, des protocoles cryptographiques, ou des systèmes biologiques. Plusieurs modèles sont disponibles selon le domaine d'application et la granularité du niveau d'observation. Dans cette thèse, nous proposons un cadre de travail unifiant pour découvrir et prouver statiquement (avant leur exécution) et automatiquement les propriétés des systèmes mobiles. Nous proposons un méta-langage dans lequel nous encodons les modèles les plus couramment utilisés dans la littérature (le p-calcul, le calcul des ambients, le join-calcul, le spi-calcul, les BIO-ambients, etc). Pour chaque modèle encodé, le méta-langage calcule une sémantique enrichie dans laquelle à la fois les composants et les objets qu'ils manipulent (adresses mémoires, noms de canaux, clefs secrètes ou partagées, etc) sont identifiés par l'historique de leur création. Ainsi, nous n'utilisons pas de relation de congruence (ni de renommage), ce qui rend l'analyse plus facile. Le cadre général de l'Interprétation Abstraite nous permet ensuite de dériver des sémantiques abstraites, qui sont décidables, correctes, et approchées. Dans cette thèse, nous donnons trois analyses génériques que nous instancions selon le compromis désiré entre le temps de calcul et la précision de l'analyse. La première analyse se concentre sur les propriétés dynamiques du système. Elle infère des relations entre les historiques des objets qui sont manipulés par les composants du système. Cette analyse distingue les instances récursives d'un même objet, et ce, même lorsque le nombre de ces instances n'est pas borné. à titre d'exemple, cette analyse prouve dans le cas d'une application client-serveur à nombre illimité de clients, que les données de chaque client ne sont pas communiquées aux autres clients. La deuxième analyse se concentre sur des propriétés de concurrence. Cette analyse compte le nombre de composants du système. Elle permet de détecter que certains composants ne peuvent pas interagir, car ils ne coexistent jamais. Elle peut aussi garantir à un système qu'il n'épuisera pas les ressources physiques disponibles. Une troisième analyse mêle concurrence et dynamicité.

L'objectif de ces travaux de thèse consiste à mettre en place des solutions algorithmiques permettant de reconstruire un modèle 3D éditable d'un environnement intérieur à l'aide d'une tablette équipée d'un capteur de profondeur.Ces travaux s'inscrivent dans le contexte de la rénovation d'intérieur. Les normes Européennes poussent à la rénovation énergétique et à la modélisation 3D des bâtiments existants. Des outils professionnels utilisant des capteurs de type LIDAR permettent de reconstruire des nuages de points de très grande qualité, mais sont coûteux et longs à mettre en œuvre. De plus, il est très difficile d'identifier automatiquement les constituants d'un bâtiment pour en exporter un modèle 3D éditable complet.Dans le cadre de la rénovation d’intérieur, il n'est pas nécessaire de disposer des informations sur l'ensemble du bâtiment, seules les principales dimensions et surfaces sont nécessaires. Nous pouvons alors envisager d'automatiser complètement le processus de modélisation 3D.La mise sur le marché de capteurs de profondeur intégrables sur tablettes, et l'augmentation des capacités de calcul de ces dernières nous permet d'envisager l'adaptation d'algorithmes de reconstruction 3D classiques à ces supports.Au cours de ces travaux, nous avons envisagé deux approches de reconstruction 3D différentes. La première approche s'appuie sur des méthodes de l'état de l'art. Elle consiste à générer un maillage 3D d'un environnement intérieur en temps réel sur tablette, puis d'utiliser ce maillage 3D pour identifier la structure globale du bâtiment (murs, portes et fenêtres). La deuxième approche envisagée consiste à générer un modèle 3D éditable en temps réel, sans passer par un maillage intermédiaire. De cette manière beaucoup plus d'informations sont disponibles pour pouvoir détecter les éléments structuraux. Nous avons en effet à chaque instant donné un nuage de points complet ainsi que l'image couleur correspondante. Nous avons dans un premier temps mis en place deux algorithmes de segmentation planaire en temps réel. Puis, nous avons mis en place un algorithme d'analyse de ces plans permettant d'identifier deux plans identiques sur plusieurs prises de vue différentes. Nous sommes alors capables d'identifier les différents murs contenus dans l'environnement capturé, et nous pouvons mettre à jour leurs informations géométriques en temps réel. / This thesis works consisted to implement algorithmic solutions to reconstruct an editable 3D model of an indoor environment using a tablet equipped with a depth sensor.These works are part of the context of interior renovation. European standards push for energy renovation and 3D modeling of existing buildings. Professional tools using LIDAR-type sensors make it possible to reconstruct high-quality point clouds, but are costly and time-consuming to implement. In addition, it is very difficult to automatically identify the constituents of a building to export a complete editable 3D model.As part of the interior renovation, it is not necessary to have information on the whole building, only the main dimensions and surfaces are necessary. We can then consider completely automating the 3D modeling process.The recent development of depth sensors that can be integrated on tablets, and the improvement of the tablets computation capabilities allows us to consider the adaptation of classical 3D reconstruction algorithms to these supports.During this work, we considered two different 3D reconstruction approaches. The first approach is based on state-of-the-art methods. It consists of generating a 3D mesh of an interior environment in real time on a tablet, then using this 3D mesh to identify the overall structure of the building (walls, doors and windows). The second approach envisaged is to generate a 3D editable model in real time, without passing through an intermediate mesh. In this way much more information is available to be able to detect the structural elements. We have in fact at each given time a complete point cloud as well as the corresponding color image. In a first time we have set up two planar segmentation algorithms in real time. Then, we set up an analysis algorithm of these plans to identify two identical planes on different captures. We are then able to identify the different walls contained in the captured environment, and we can update their geometric information in real-time.

Les “smart-devices” tels les smartphones, tablettes et même les montres ont été largement démocratisés au cours de la dernière décennie. Dans nos sociétés occidentales, on ne garde plus seulement son ordinateur personnel chez soi, on le transporte dans la poche arrière de son pantalon ou bien autour de son poignet. Ces outils ne sont d’ailleurs plus limités, en termes d’utilisation, à de la simple communication par SMS ou bien téléphone, on se fie à eux pour stocker nos photos et données personnelles, ces dernières parfois aussi critiques que des données de paiement bancaires, on gère nos contacts et finances, se connecte à notre boite mail ou un site marchand depuis eux. . . Des exemples récents nous fournissent d’ailleurs un aperçu des tâches de plus en plus complexes que l’on confie à ces outils : l’Estonie autorise l’utilisation de smartphones pour participer aux scrutins nationaux et en 2017, la société Transport for London a lancé sa propre application autorisant l’émulation d’une Oyster card et son rechargement pour emprunter son réseau de transports publics. Plus les services se complexifient, plus la confiance qui leur est accordée par les groupes industriels et les utilisateurs grandit. Nous nous intéressons ici aux protocoles cryptographiques qui définissent les échanges entre les outils et entités qui interviennent dans l’utilisation de tels services et aux garanties qu’ils proposent en termes de sécurité (authentification mutuelle des agent, intégrité des messages circulant, secret d’une valeur critique…). Moult exemples de la littérature et de la vie courante ont démontré que leur élaboration était hautement vulnérable à des erreurs de design. Heureusement, des années de recherches nous ont fournis des outils pour rendre cette tâche plus fiable, les méthodes formelles font partie de ceux-là. Il est possible de modeler un protocole cryptographique comme un processus abstrait qui manipule des données et primitives cryptographiques elles aussi modélisées comme des termes et fonctions abstraites. On met le protocole à l’épreuve face à un attaquant actif et on peut spécifier mathématiquement les propriétés de sécurité qu’il est censé garantir. Ces preuves de sécurité peuvent être automatisées grâce à des outils tels que ProVerif ou bien Tamarin. L’une des grandes difficultés lorsque l’on cherche à concevoir et prouver formellement la sécurité d’un protocole de niveau industriel réside dans le fait que ce genre de protocole est généralement très long et doit satisfaire des propriétés de sécurité plus complexes que certains protocoles universitaires. Au cours de cette thèse, nous avons souhaité étudier deux cas d’usage : le vote électronique et le paiement mobile. Dans les deux cas, nous avons conçu et prouvé la sécurité d’un protocole répondant aux problématiques spécifiques à chacun des cas d’usage. Dans le cadre du vote électronique, nous proposons le protocole Belenios VS, une variante de Belenios RF. Nous définissons l’écosystème dans lequel le protocole est exécuté et prouvons sa sécurité grâce à ProVerif. Belenios VS garantit la confidentialité du vote et le fait qu’un utilisateur puisse vérifier que son vote a bien fait parti du résultat final de l’élection, tout cela même si l’outil utilisé par le votant est sous le contrôle d’un attaquant. Dans le cadre du paiement, nous avons proposé la première spécification ouverte de bout en bout d’une application de paiement mobile. Sa conception a pris en compte le fait qu’elle devait pouvoir s’adapter à l’écosystème de paiement déjà existant pour être largement déployable et que les coûts de gestion, de développement et de maintenance de la sécurité devait être optimisés / The last decade has seen the massive democratization of smart devices such as phones, tablets, even watches. In the wealthiest societies of the world, not only do people have their personal computer at home, they now carry one in their pocket or around their wrist on a day to day basis. And those devices are no more used simply for communication through messaging or phone calls, they are now used to store personal photos or critical payment data, manage contacts and finances, connect to an e-mail box or a merchant website... Recent examples call for more complex tasks we ask to such devices: Estonia voting policy allows the use of smart ID cards and smartphones to participate to national elections. In 2017, Transport for London launched the TfL Oyster app to allow tube users to top up and manage their Oyster card from their smartphone. As services grow with more complexity, so do the trust users and businesses put in them. We focus our interest into cryptographic protocols which define the exchanges between devices and entities so that such interaction ensure some security guarantees such as authentication, integrity of messages, secrecy… Their design is known to be an error prone task. Thankfully, years of research gave us some tools to improve the design of security protocols, among them are the formal methods: we can model a cryptographic protocol as an abstract process that manipulates data and cryptographic function, also modeled as abstract terms and functions. The protocol is tested against an active adversary and the guarantees we would like a protocol to satisfy are modeled as security properties. The security of the protocol can then be mathematically proven. Such proofs can be automated with tools like ProVerif or Tamarin. One of the big challenge when it comes to designing and formally proving the security an “industrial- level” protocol lies in the fact that such protocols are usually heavier than academic protocols and that they aim at more complex security properties than the classical ones. With this thesis, we wanted to focus on two use cases: electronic voting and mobile payment. We designed two protocols, one for each respective use case and proved their security using automated prover tools. The first one, Belenios VS, is a variant of an existing voting scheme, Belenios RF. It specifies a voting ecosystem allowing a user to cast a ballot from a voting sheet by flashing a code. The protocol’s security has been proven using the ProVerif tool. It guarantees that the vote confidentiality cannot be broken and that the user is capable of verifying their vote is part of the final result by performing a simple task that requires no technical skills all of this even if the user’s device is compromised – by a malware for instance. The second protocol is a payment one that has been conceived in order to be fully scalable with the existing payment ecosystem while improving the security management and cost on the smartphone. Its security has been proven using the Tamarin prover and holds even if the user’s device is under an attacker’s control

Les nouvelles technologies en matière d'accès à l'information, de communication sans-fil et de localisation d'informations ouvrent la voie à des innovations majeures dans l'utilisation des systèmes informatiques. Ces avancées permettent d'imaginer de nouveaux usages informatiques dont la mise en œuvre motive le développement de méthodes de conception appropriées. Plus particulièrement, l'informatique mobile combine désormais des enjeux conceptuels tels que l'accès à des services par un utilisateur en mobilité, la généralisation d'outils de localisation, la compréhension de systèmes complexes par un public non-expert ou l'importante variabilité des situations d'exécution. Cette thèse propose un cadre de conception qui adresse certains des enjeux pour la mobilité des systèmes d'information. Dans cette perspective, les attentes des utilisateurs et les contraintes technologiques inhérentes à la mobilité des constituants du système définissent un espace contextuel dont les dimensions sont prises en compte dès les premières étapes de la conception. Le modèle proposé établit comme point d'entrée une description de l'espace géographique du système pour différencier un ensemble de contextes d'exécution. L'énoncé de ces contextes permet de corréler les attentes des utilisateurs avec les capacités techniques de la plate-forme et d'offrir le niveau fonctionnel le plus acceptable dans une situation donnée. Dans un second temps, les différentes fonctionnalités et les données mises en œuvre dans chaque contexte d'exécution peuvent être ordonnées ou filtrées afin d'optimiser la présentation des informations aux utilisateurs. Ces recommandations sont produites par l'analyse conjointe des préférences d'utilisateurs selon leurs interactions et leurs comportements spatiaux. Deux cadres expérimentaux viennent illustrer les propositions du modèle. La conception d'un système mobile de suivi de compétition nautique prend en compte différents contextes d'exécution et adapte un niveau de service à des situations dégradées. Un système de documentation et de visite de campus illustre les algorithmes de recommandation et affine la présentation d'informations localement à chaque contexte d'exécution.

Les travaux résumés dans ce mémoire ont pour cadre la sûreté de fonctionnement des systèmes informatiques. Ils portent sur l'élimination des fautes, en s'intéressant plus particulièrement au test du logiciel. Les contributions sont regroupées en quatre chapitres. Le premier chapitre rassemble des travaux pour adapter la conception du test aux technologies de développement logicielles. Deux technologies sont considérées : la technologie orientée-­‐objet et la méthode formelle B. Le deuxième chapitre porte sur des associations test et vérification formelle. Il s'agit selon les cas de consolider la vérification d'algorithmes partiellement prouvés, ou de faciliter l'analyse de contrexemples retournés par un model checker. Le troisième chapitre traite de la génération de test par des procédés métaheuristiques, en prenant l'exemple du recuit simulé. L'accent est mis sur l'utilisation de mesures pour guider le paramétrage de la métaheuristique. Enfin, le quatrième chapitre aborde le test de systèmes mobiles. Lestraces d'exécutions sont vérifiées par rapport à un ensemble de propriétés décrites par des scénarios graphiques, en combinant des algorithmes d'appariement de graphes et de calcul d'ordres partiels d'événements.

Les nouvelles technologies en matière d'accès à l'information, de communication sans-fil et de localisation d'informations ouvrent la voie à des innovations majeures dans l'utilisation des systèmes informatiques. Ces avancées permettent d'imaginer de nouveaux usages informatiques dont la mise en œuvre motive le développement de méthodes de conception appropriées. Plus particulièrement, l'informatique mobile combine désormais des enjeux conceptuels tels que l'accès à des services par un utilisateur en mobilité, la généralisation d'outils de localisation, la compréhension de systèmes complexes par un public non-expert ou l'importante variabilité des situations d'exécution. Cette thèse propose un cadre de conception qui adresse certains des enjeux pour la mobilité des systèmes d'information. Dans cette perspective, les attentes des utilisateurs et les contraintes technologiques inhérentes à la mobilité des constituants du système définissent un espace contextuel dont les dimensions sont prises en compte dès les premières étapes de la conception. Le modèle proposé établit comme point d'entrée une description de l'espace géographique du système pour différencier un ensemble de contextes d'exécution. L'énoncé de ces contextes permet de corréler les attentes des utilisateurs avec les capacités techniques de la plate-forme et d'offrir le niveau fonctionnel le plus acceptable dans une situation donnée. Dans un second temps, les différentes fonctionnalités et les données mises en œuvre dans chaque contexte d'exécution peuvent être ordonnées ou filtrées afin d'optimiser la présentation des informations aux utilisateurs. Ces recommandations sont produites par l'analyse conjointe des préférences d'utilisateurs selon leurs interactions et leurs comportements spatiaux. Deux cadres expérimentaux viennent illustrer les propositions du modèle. La conception d'un système mobile de suivi de compétition nautique prend en compte différents contextes d'exécution et adapte un niveau de service à des situations dégradées. Un système de documentation et de visite de campus illustre les algorithmes de recommandation et affine la présentation d'informations localement à chaque contexte d'exécution.

Cette thèse a été effectuée en collaboration entre le Centre de Robotique CAOR de MINES ParisTech et MENSI-Trimble sous convention CIFRE (Convention Industrielle de Formation par la Recherche), afin de concevoir un nouveau système de scanner laser innovant dédié aux systèmes mobiles de cartographie. Pour cela, nous avons développé une méthode d'analyse qualitative des relevés laser et une démarche de conception par simulation d'un système mobile de cartographie. Nous avons ensuite élaboré plusieurs concepts de scanners laser mobiles. A l'aide du simulateur, nous avons virtuellement réalisé ces concepts et avons fait des acquisitions simulées afin d'analyser les données. Après avoir obtenu les résultats de l'analyse, nous avons choisi un concept, réalisé son prototypage et effectué son évaluation en situation réelle.

Les travaux présentés dans ce mémoire résument l'ensemble de mes activités dans le domaine de la résilience et du respect de la vie privée dans les systèmes ubiquitaires mobiles. Ils s'orientent sur trois axes principaux : l'utilisation de la réfléxivité pour la construction d'architectures sûres, la résilience des systèmes mobiquitaires (architectures, algorithmes et leur évalution), et la geoprivacy. Le premier axe concerne la tolérance aux fautes pour les systèmes distribués, sous un angle architecture et langage. Dans ces travaux, j' ai étudié l'utilisation de la réflexivité à la compilation et à l'exécution afin de faciliter l'implémentation de mécanismes de tolérance aux fautes indépendemment de l'application. L'utilisation de la réflexivité a été étudiée dans le cadre de travaux théoriques, concernant la réflexivité multi-niveaux, ou plus pratiques, comme la mise en oeuvre de la réflexivité sur des composants sur étagères, dans une architecture logicielle embarquée, ou pour permettre l'adaptation de mécanismes de tolérance aux fautes à l'exécution. Le chapitre 1 présente ces différents travaux. Le deuxième axe concerne la tolérance aux fautes dans les systèmes mobiles. Mon approche a été d'aborder la mobilité comme un atout et non pas comme une difficulté. Cette approche m'a mené à étudier la notion de communication de groupes géographiques : comment définir un groupe d'entités communicantes en fonction de leur localisation respective ou en fonction de leur proximité. J'ai ensuite, sous l'angle du pair-à-pair, proposé un système de sauvegarde coopérative de données, où les noeuds mobiles participants offrent un service de stockage sécurisé qu'ils peuvent utiliser afin de sauvegarder leurs données critiques. Cette solution a été également déclinée pour offrir un système de boîte noire virtuelle pour l'automobile. Ces travaux ont été traités sous des angles algorithmique et architecturaux, mais également sous l'angle de l'évaluation de la sûreté de fonctionnement, à la fois analytique et expérimentale. Ces travaux font l'objet du chapitre 2. Dans le cadre de mes recherches sur la résilience des systèmes mobiquitaires, des questions d'ordre déontologique ont été soulevées : comment exploiter des données de mobilité individuelles tout en préservant la vie privée des individus ? C'est à cette occasion que je me suis intéressé à ce que l'on peut nommer la geoprivacy. Ce domaine représente maintenant la majeure partie de mes travaux, tant sous l'angle des attaques que sous celui de la protection. Nous proposons un modèle Markovien de mobilité individuelle, outil à la fois compact, précis, intelligible et facilement adaptable pour représenter la mobilité d'un individu. Sur la base de ce modèle de mobilité, nous proposons plusieurs attaques qui ciblent par exemple la prédiction des déplacements futurs, ou encore la des-anonymisation. En ce qui concerne la protection de la geoprivacy, nous travaillons actuellement sur des abstractions de niveau intergiciel, tel les locanymes ou les localisation vérifiées, afin de proposer une architecture sûre et respectueuse de la vie privée pour les systèmes géolocalisés. Le chapitre 3 aborde ces aspects de ma recherche. Ces différents travaux se sont enchaînés dans un mélange de hasard, de sérendipité et de poursuite d'un objectif commun : fournir des moyens algorithmiques et architecturaux pour la résilience des systèmes informatiques actuels, à savoir distribués, mobiles, ubiquitaires. Les techniques et outils que j'utilise pour aborder cette problématique large auront été divers et variés, cela participe à mon expérience, sans cesse renouvelée. De nombreuses pistes de recherche sont encore ouvertes et sont exposées dans le chapitre 4.

De nos jours, l’omniprésence des systèmes mobiles ne fait qu’accroitre et ces derniers deviennent indispensables pour nombreux d’entre nous. Les constructeurs de ces plateformes mobiles inondent le marché avec des produits de plus en plus performants et contenant un grand nombre d’applications énergivores. Le revers de la médaille de cette popularité est la consommation d’énergie. En effet, les caractéristiques des systèmes mobiles actuels ne font qu’accentuer le besoin d’une refonte des techniques d’optimisations de la consommation d’énergie. Dans une époque où les consciences s’élèvent pour un monde plus «green», de nombreuses solutions sont proposées pour répondre à la problématique de la consommation d’énergie des systèmes mobiles. Cependant, dans les solutions existantes, le comportement de l’utilisateur et ses besoins sont rarement considérés. Cette omission est paradoxale car c’est le comportement de l’utilisateur final qui détermine la consommation d’énergie du système. D’autre part, l’utilisation des données qui émanent des différents capteurs embarqués et du système d’exploitation peut être bénéfique pour mettre en place des politiques efficientes de gestion de puissance. Exploité à bon escient, l’important flux d’informations disponible est susceptible de servir à la caractérisation du comportement de l’utilisateur, ses habitudes et ses besoins en matière de configuration hardware. En assimilant ces informations et en les traitant, nous pouvons proposer des optimisations d’énergie sans altérer la satisfaction de l’utilisateur. Dans cette thèse nous proposons le modèle CPA pour Collect – Process – Adjust. Ce modèle permet de collecter des données émanant de différentes sources, les traiter et en générer des politiques d’optimisations d’énergie. Les travaux de cette thèse ont été réalisés en coopération avec Intel. L’objectif de cette collaboration est la conception et la réalisation de solutions permettant d’améliorer la gestion d’énergie proposée par le système d’exploitation. / Optimizing energy consumption in modern mobile handled devices plays a crucial role as lowering the power consumption impacts battery life and systemreliability. Recent mobile platforms have an increasing number of sensors and processing components. Added to the popularity of power-hungry applications, battery life in mobile devices is an important issue. However, the utilization pattern of large amount of data from the various sensors can be beneficial to detect the changing device context, the user needs and the running application requirements in terms of hardware resources. When these information are used properly, an efficient control of power knobs can be implemented to reduce the energy consumption. This thesis has been achieved in collaboration with Intel Portland.

La diffusion massive de dispositifs portables, de plus en plus utilisés pour le traitement et la communication de l'information, permet la collecte d'importantes masses de données liées à l'activité des utilisateurs sur des applications mobiles. Nous nous intéressons aux données de localisation (les traces de mobilité) qui sont issues de systèmes mobiles formés par un groupe d'utilisateurs. Les données de mobilité produites dans un système mobile sont étudiées suivant deux axes : - L'utilisation des modèles de mobilité est à la base du développement d'algorithmes de communication dédiés au systèmes mobiles. Les données de mobilité réelles concernant les utilisateurs vont nous permettre de comparer les données de mobilité synthétiques utilisées dans la simulation avec la réalité qu'ils sont censés décrire. - La manipulation des données de mobilité réelles implique une réflexion sur les conséquences que les informations extraites de ces données ont relativement à la protection de la vie privée des utilisateurs. Les contributions sur ces deux fronts sont les suivantes : - Une analyse fine des propriétés spatiales et sociales d'un ensemble de traces de mobilité réelles collecté expérimentalement à l'aide d'une plateforme à haute precision. - Une comparaison exploratoire entre des traces de mobilité réelles et des traces de mobilité synthétiques générées à partir de sept différents modèle de mobilité. - La conception et l'analyse d'un algorithme d'inférence par co-localisation décorrélée des informations sur la localisation des utilisateurs ciblés. - La quantification du potentiel des données de co-localisation non-déterministes sur la perte de protection de la vie privée d'un ensemble d'utilisateurs. / The wide diffusion of smart portable devices allows the collection of a big amount of data concerning the activities of users from mobile apps. We focus our attention on location data, i.e. mobility traces, of a set of users in a crowd. Data collected from these mobile systems are studied following two axies: - Mobility models are used to simulate the behavior of users to develop opportunistic forwarding algorithms. We compare real and synthetic mobility traces to show the distance between the reality and the models. - Information on mobility may endanger the privacy of users. We analyze the impact of such information on privacy of users. The main contributions are: - We analyze the spatial and social properties of human motion from real traces collected by a highly accurate experimental localization system. - We compare the real traces with synthetic mobility traces generated from seven popular mobility models - We provide an inference algorithm based on co-location of users and we show its efficiency on different datasets. - We quantify the effect of probabilistic co-location information by means of a novel co-location attack.